From 77802cfba08ca7fcb5b830d34119daf561a7ce60 Mon Sep 17 00:00:00 2001
From: Daniel Kroening <dkr@amazon.com>
Date: Sat, 13 Dec 2025 16:51:15 -0800
Subject: [PATCH] ensure reset constraint is Boolean

This addresses the case when the argument given to --reset is not Boolean.
---
 .../test.desc => CLI/reset1.desc}                 |  2 +-
 .../main.sv => CLI/reset1.sv}                     |  0
 regression/ebmc/CLI/reset2.desc                   |  7 +++++++
 regression/ebmc/CLI/reset2.sv                     | 15 +++++++++++++++
 src/ebmc/build_transition_system.cpp              |  4 ++++
 5 files changed, 27 insertions(+), 1 deletion(-)
 rename regression/ebmc/{reset-command-line-option1/test.desc => CLI/reset1.desc} (87%)
 rename regression/ebmc/{reset-command-line-option1/main.sv => CLI/reset1.sv} (100%)
 create mode 100644 regression/ebmc/CLI/reset2.desc
 create mode 100644 regression/ebmc/CLI/reset2.sv

diff --git a/regression/ebmc/reset-command-line-option1/test.desc b/regression/ebmc/CLI/reset1.desc
similarity index 87%
rename from regression/ebmc/reset-command-line-option1/test.desc
rename to regression/ebmc/CLI/reset1.desc
index b56303c9f..f7fd20981 100644
--- a/regression/ebmc/reset-command-line-option1/test.desc
+++ b/regression/ebmc/CLI/reset1.desc
@@ -1,5 +1,5 @@
 CORE
-main.sv
+reset1.sv
 --module top --bound 10 --reset reset_n
 ^EXIT=0$
 ^SIGNAL=0$
diff --git a/regression/ebmc/reset-command-line-option1/main.sv b/regression/ebmc/CLI/reset1.sv
similarity index 100%
rename from regression/ebmc/reset-command-line-option1/main.sv
rename to regression/ebmc/CLI/reset1.sv
diff --git a/regression/ebmc/CLI/reset2.desc b/regression/ebmc/CLI/reset2.desc
new file mode 100644
index 000000000..fd8cd275b
--- /dev/null
+++ b/regression/ebmc/CLI/reset2.desc
@@ -0,0 +1,7 @@
+CORE
+reset2.sv
+--module top --bound 10 --reset ~reset_n
+^\[top\.p1\] always \(disable iff \(!top\.reset_n\) top\.data >= 0 && top\.data <= 10\): PROVED .*$
+^EXIT=0$
+^SIGNAL=0$
+--
diff --git a/regression/ebmc/CLI/reset2.sv b/regression/ebmc/CLI/reset2.sv
new file mode 100644
index 000000000..7b1e27a5e
--- /dev/null
+++ b/regression/ebmc/CLI/reset2.sv
@@ -0,0 +1,15 @@
+module top(input reset_n, clk);
+
+  reg [7:0] data;
+
+  always @(posedge clk) begin
+    if(!reset_n)
+      data = 0;
+    else if(data != 10)
+      data++;
+  end
+
+  // the below holds if the design is reset properly
+  p1: assert property (disable iff (!reset_n) data >=0 && data <= 10);
+
+endmodule
diff --git a/src/ebmc/build_transition_system.cpp b/src/ebmc/build_transition_system.cpp
index f14dc10b6..897803bf4 100644
--- a/src/ebmc/build_transition_system.cpp
+++ b/src/ebmc/build_transition_system.cpp
@@ -276,6 +276,10 @@ int get_transition_system(
     exprt reset_constraint = to_expr(
       ns, transition_system.main_symbol->name, cmdline.get_value("reset"));
 
+    // we want the constraint to be boolean
+    reset_constraint =
+      typecast_exprt::conditional_cast(reset_constraint, bool_typet{});
+
     // true in initial state
     transt new_trans_expr = transition_system.trans_expr;
     new_trans_expr.init() = and_exprt(new_trans_expr.init(), reset_constraint);