From be27d85ae2267a4dcbc4019854f99922a078adb3 Mon Sep 17 00:00:00 2001
From: Daniel Kroening <dkr@amazon.com>
Date: Wed, 4 Jun 2025 17:27:24 -0700
Subject: [PATCH] SMV: disallow next(...) in INVAR

This errors the use of next(...) in INVAR, which matches NuSMV's behavior.
---
 regression/smv/invar/invar1.desc |  8 ++++++++
 regression/smv/invar/invar1.smv  | 11 +++++++++++
 regression/smv/invar/invar2.desc |  8 ++++++++
 regression/smv/invar/invar2.smv  |  6 ++++++
 src/smvlang/smv_typecheck.cpp    |  5 +++++
 5 files changed, 38 insertions(+)
 create mode 100644 regression/smv/invar/invar1.desc
 create mode 100644 regression/smv/invar/invar1.smv
 create mode 100644 regression/smv/invar/invar2.desc
 create mode 100644 regression/smv/invar/invar2.smv

diff --git a/regression/smv/invar/invar1.desc b/regression/smv/invar/invar1.desc
new file mode 100644
index 00000000..cd2b0d3e
--- /dev/null
+++ b/regression/smv/invar/invar1.desc
@@ -0,0 +1,8 @@
+CORE
+invar1.smv
+--bound 20
+^\[.*\] G x != 10: PROVED up to bound 20$
+^EXIT=0$
+^SIGNAL=0$
+--
+--
diff --git a/regression/smv/invar/invar1.smv b/regression/smv/invar/invar1.smv
new file mode 100644
index 00000000..c8fc124f
--- /dev/null
+++ b/regression/smv/invar/invar1.smv
@@ -0,0 +1,11 @@
+MODULE main
+
+VAR x : 1..10;
+
+ASSIGN init(x) := 1;
+ASSIGN next(x) := x = 10 ? 10 : x + 1;
+
+-- x won't reach 10, since we won't reach 3
+INVAR x != 3
+
+LTLSPEC G x != 10
diff --git a/regression/smv/invar/invar2.desc b/regression/smv/invar/invar2.desc
new file mode 100644
index 00000000..27ee2c9b
--- /dev/null
+++ b/regression/smv/invar/invar2.desc
@@ -0,0 +1,8 @@
+CORE
+invar2.smv
+
+^file .* line 6: next\(...\) is not allowed here$
+^EXIT=2$
+^SIGNAL=0$
+--
+--
diff --git a/regression/smv/invar/invar2.smv b/regression/smv/invar/invar2.smv
new file mode 100644
index 00000000..d5739c7b
--- /dev/null
+++ b/regression/smv/invar/invar2.smv
@@ -0,0 +1,6 @@
+MODULE main
+
+VAR x : 1..10;
+
+-- next(...) is not allowed
+INVAR next(x) != 3
diff --git a/src/smvlang/smv_typecheck.cpp b/src/smvlang/smv_typecheck.cpp
index 009f5e55..9c446d7c 100644
--- a/src/smvlang/smv_typecheck.cpp
+++ b/src/smvlang/smv_typecheck.cpp
@@ -49,6 +49,7 @@ class smv_typecheckt:public typecheckt
   typedef enum
   {
     INIT,
+    INVAR,
     TRANS,
     OTHER,
     LTL,
@@ -1562,6 +1563,10 @@ void smv_typecheckt::typecheck(
     return;
 
   case smv_parse_treet::modulet::itemt::INVAR:
+    typecheck(item.expr, INVAR);
+    convert_expr_to(item.expr, bool_typet{});
+    return;
+
   case smv_parse_treet::modulet::itemt::FAIRNESS:
     typecheck(item.expr, OTHER);
     convert_expr_to(item.expr, bool_typet{});