From 2dc3c7d0c32339b587f3bac1e7f50746c99f6a1d Mon Sep 17 00:00:00 2001
From: Daniel Kroening <dkr@amazon.com>
Date: Fri, 18 Oct 2024 06:19:15 -0700
Subject: [PATCH] EBMC: retain assumptions when using --property

When using the --property command-line option, do not disable the
assumptions.
---
 CHANGELOG                                              |  1 +
 .../{assume1/test.desc => assumptions/assume1.desc}    |  2 +-
 .../ebmc/{assume1/main.v => assumptions/assume1.v}     |  0
 regression/ebmc/assumptions/assume2.desc               |  7 +++++++
 regression/ebmc/assumptions/assume2.sv                 | 10 ++++++++++
 src/ebmc/ebmc_properties.cpp                           |  4 +++-
 6 files changed, 22 insertions(+), 2 deletions(-)
 rename regression/ebmc/{assume1/test.desc => assumptions/assume1.desc} (95%)
 rename regression/ebmc/{assume1/main.v => assumptions/assume1.v} (100%)
 create mode 100644 regression/ebmc/assumptions/assume2.desc
 create mode 100644 regression/ebmc/assumptions/assume2.sv

diff --git a/CHANGELOG b/CHANGELOG
index 9cc8eca31..5f17b63bd 100644
--- a/CHANGELOG
+++ b/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
 
diff --git a/regression/ebmc/assume1/test.desc b/regression/ebmc/assumptions/assume1.desc
similarity index 95%
rename from regression/ebmc/assume1/test.desc
rename to regression/ebmc/assumptions/assume1.desc
index 0c1ff980a..bee7188f9 100644
--- a/regression/ebmc/assume1/test.desc
+++ b/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$
diff --git a/regression/ebmc/assume1/main.v b/regression/ebmc/assumptions/assume1.v
similarity index 100%
rename from regression/ebmc/assume1/main.v
rename to regression/ebmc/assumptions/assume1.v
diff --git a/regression/ebmc/assumptions/assume2.desc b/regression/ebmc/assumptions/assume2.desc
new file mode 100644
index 000000000..d2729fec3
--- /dev/null
+++ b/regression/ebmc/assumptions/assume2.desc
@@ -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$
diff --git a/regression/ebmc/assumptions/assume2.sv b/regression/ebmc/assumptions/assume2.sv
new file mode 100644
index 000000000..321751301
--- /dev/null
+++ b/regression/ebmc/assumptions/assume2.sv
@@ -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 
diff --git a/src/ebmc/ebmc_properties.cpp b/src/ebmc/ebmc_properties.cpp
index fb3ee03f7..b1b848595 100644
--- a/src/ebmc/ebmc_properties.cpp
+++ b/src/ebmc/ebmc_properties.cpp
@@ -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;