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;