From a22bb786e0c59b9ecae7f15221617dd0c0b2aa0c Mon Sep 17 00:00:00 2001
From: Daniel Kroening <dkr@amazon.com>
Date: Sun, 2 Nov 2025 15:14:24 -0800
Subject: [PATCH] SMV: test for precedence of X vs &

This test checks the relative precedence of X vs &.
---
 regression/smv/LTL/smv_ltlspec_X1.desc | 10 ++++++++++
 regression/smv/LTL/smv_ltlspec_X1.smv  | 11 +++++++++++
 2 files changed, 21 insertions(+)
 create mode 100644 regression/smv/LTL/smv_ltlspec_X1.desc
 create mode 100644 regression/smv/LTL/smv_ltlspec_X1.smv

diff --git a/regression/smv/LTL/smv_ltlspec_X1.desc b/regression/smv/LTL/smv_ltlspec_X1.desc
new file mode 100644
index 000000000..fd8f47f86
--- /dev/null
+++ b/regression/smv/LTL/smv_ltlspec_X1.desc
@@ -0,0 +1,10 @@
+CORE
+smv_ltlspec_X1.smv
+
+^\[.*\] X x & x: REFUTED$
+^\[.*\] X x & x: REFUTED$
+^\[.*\] X \(x & x\): PROVED \(CT=1\)$
+^EXIT=10$
+^SIGNAL=0$
+--
+^warning: ignoring
diff --git a/regression/smv/LTL/smv_ltlspec_X1.smv b/regression/smv/LTL/smv_ltlspec_X1.smv
new file mode 100644
index 000000000..b389b86eb
--- /dev/null
+++ b/regression/smv/LTL/smv_ltlspec_X1.smv
@@ -0,0 +1,11 @@
+MODULE main
+
+VAR x : boolean;
+
+ASSIGN next(x) := TRUE;
+       init(x) := FALSE;
+
+-- X binds stronger than &
+LTLSPEC X x & x -- should parse as (X x) & x
+LTLSPEC (X x) & x -- should fail
+LTLSPEC X (x & x) -- should pass