Merge pull request #1637 from diffblue/p-command-line-option2

ensure that command-line properties are boolean

Author: tautschnig

CHANGELOG

@@ -1,5 +1,7 @@
 # EBMC 5.10
 
+* cast properties given with -p to Boolean if need be
+
 # EBMC 5.9
 
 * Verilog: use top-level module for verification, instead of "main"

regression/ebmc/p-command-line-option/p-command-line-option2.desc

@@ -0,0 +1,8 @@
+CORE
+p-command-line-option2.v
+--bound 1 -p "0"
+^EXIT=10$
+^SIGNAL=0$
+^\[command-line assertion\] always 0: REFUTED$
+--
+^warning: ignoring

regression/ebmc/p-command-line-option/p-command-line-option2.v

@@ -0,0 +1,3 @@
+module main(input clk);
+
+endmodule

src/ebmc/ebmc_properties.cpp

@@ -159,6 +159,9 @@ ebmc_propertiest ebmc_propertiest::from_command_line(
       throw ebmc_errort() << "failed to parse the given property expression";
     }
 
+    // We want the property to be boolean.
+    expr = typecast_exprt::conditional_cast(expr, bool_typet{});
+
     // We give it an implict always, as in SVA
 
     if(expr.id() != ID_sva_always)