ensure reset constraint is Boolean

regression/ebmc/reset-command-line-option1/test.desc → 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$

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$
+--

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

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);