ensure reset constraint is Boolean

This addresses the case when the argument given to --reset is not Boolean.

Author: kroening

…bmc/reset-command-line-option1/test.desc regression/ebmc/CLI/reset1.descregression/ebmc/reset-command-line-option1/test.desc renamed to regression/ebmc/CLI/reset1.desc regression/ebmc/reset-command-line-option1/test.desc renamed to 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$

…/ebmc/reset-command-line-option1/main.sv regression/ebmc/CLI/reset1.svregression/ebmc/reset-command-line-option1/main.sv renamed to regression/ebmc/CLI/reset1.sv regression/ebmc/reset-command-line-option1/main.sv renamed to regression/ebmc/CLI/reset1.sv

@@ -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.desc

@@ -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

regression/ebmc/CLI/reset2.sv

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