From d3c912497d7aea328dc4092d41d66f587f72637f Mon Sep 17 00:00:00 2001
From: Daniel Kroening <dkr@amazon.com>
Date: Tue, 20 May 2025 13:24:56 +0100
Subject: [PATCH] Bugfix: use INVAR for SMV word-level in-state invariants

This fixes the SMV word-level output for in-state invariants.
---
 regression/ebmc/smv-word-level/verilog2.desc | 24 ++++++++++----------
 src/ebmc/output_smv_word_level.cpp           |  2 +-
 2 files changed, 13 insertions(+), 13 deletions(-)

diff --git a/regression/ebmc/smv-word-level/verilog2.desc b/regression/ebmc/smv-word-level/verilog2.desc
index 9d099e002..04df97b3a 100644
--- a/regression/ebmc/smv-word-level/verilog2.desc
+++ b/regression/ebmc/smv-word-level/verilog2.desc
@@ -2,18 +2,18 @@ CORE
 verilog2.sv
 --smv-word-level
 ^MODULE main$
-^INIT main\.sw1 = extend\(signed\(main\.ui\), 24\)$
-^INIT main\.sw2 = extend\(main\.si, 24\)$
-^INIT main\.uw1 = extend\(main\.ui, 24\)$
-^INIT main\.uw2 = unsigned\(extend\(main\.si, 24\)\)$
-^INIT main\.sn1 = signed\(resize\(main\.ui, 4\)\)$
-^INIT main\.sn2 = signed\(resize\(unsigned\(main.si\), 4\)\)$
-^INIT main\.un1 = resize\(main\.ui, 4\)$
-^INIT main\.un2 = resize\(unsigned\(main\.si\), 4\)$
-^INIT main\.sb1 = signed\(main\.ui\)$
-^INIT main\.sb2 = main\.si$
-^INIT main\.ub1 = main\.ui$
-^INIT main\.ub2 = unsigned\(main\.si\)$
+^INVAR main\.sw1 = extend\(signed\(main\.ui\), 24\)$
+^INVAR main\.sw2 = extend\(main\.si, 24\)$
+^INVAR main\.uw1 = extend\(main\.ui, 24\)$
+^INVAR main\.uw2 = unsigned\(extend\(main\.si, 24\)\)$
+^INVAR main\.sn1 = signed\(resize\(main\.ui, 4\)\)$
+^INVAR main\.sn2 = signed\(resize\(unsigned\(main.si\), 4\)\)$
+^INVAR main\.un1 = resize\(main\.ui, 4\)$
+^INVAR main\.un2 = resize\(unsigned\(main\.si\), 4\)$
+^INVAR main\.sb1 = signed\(main\.ui\)$
+^INVAR main\.sb2 = main\.si$
+^INVAR main\.ub1 = main\.ui$
+^INVAR main\.ub2 = unsigned\(main\.si\)$
 ^EXIT=0$
 ^SIGNAL=0$
 --
diff --git a/src/ebmc/output_smv_word_level.cpp b/src/ebmc/output_smv_word_level.cpp
index 9a1b5fb1f..e0565f147 100644
--- a/src/ebmc/output_smv_word_level.cpp
+++ b/src/ebmc/output_smv_word_level.cpp
@@ -119,7 +119,7 @@ smv_invar(const exprt &expr, const namespacet &ns, std::ostream &out)
   if(expr.id() == ID_and)
   {
     for(auto &conjunct : expr.operands())
-      smv_initial_states(conjunct, ns, out);
+      smv_invar(conjunct, ns, out);
   }
   else if(expr.is_true())
   {