Merge pull request #780 from diffblue/assume2

EBMC: retain assumptions when using `--property`

Author: tautschnig

CHANGELOG

@@ -6,6 +6,7 @@
 * Verilog: allow indexed part select
 * word-level BMC: fix for F/s_eventually and U/s_until
 * IC3: liveness to safety translation
+* Assumptions are not disabled when using --property
 
 # EBMC 5.2
 

regression/ebmc/assume1/test.desc renamed to regression/ebmc/assumptions/assume1.desc

@@ -1,5 +1,5 @@
 CORE
-main.v
+assume1.v
 --module main --bound 3 --aig --vl2smv-extensions
 ^\[main\.property\.a1\] assume always 10 <= main\.a && main\.a <= 100: ASSUMED$
 ^\[main\.property\.p1\] always main\.a != 200: PROVED up to bound 3$

regression/ebmc/assume1/main.v renamed to regression/ebmc/assumptions/assume1.v

@@ -0,0 +1,7 @@
+CORE
+assume2.sv
+--bound 0 --property main.p1
+^\[main\.a1\] assume always 10 <= main\.a && main\.a <= 100: ASSUMED$
+^\[main\.p1\] always main\.a != 200: PROVED up to bound 0$
+^EXIT=0$
+^SIGNAL=0$

regression/ebmc/assumptions/assume2.desc

@@ -0,0 +1,10 @@
+module main(input [31:0] a);
+
+  a1: assume final (10<=a && a<=100);
+
+  p1: assert final (a!=200);
+
+  // would fail
+  p2: assert final (a!=20);
+
+endmodule 

regression/ebmc/assumptions/assume2.sv

@@ -110,8 +110,10 @@ bool ebmc_propertiest::select_property(
   {
     std::string property = cmdline.get_value("property");
 
+    // disable all assertions (not: assumptions)
     for(auto &p : properties)
-      p.status = propertyt::statust::DISABLED;
+      if(!p.is_assumed())
+        p.status = propertyt::statust::DISABLED;
 
     bool found = false;