diff --git a/regression/ebmc/ic3/not_supported3.desc b/regression/ebmc/ic3/not_supported3.desc
new file mode 100644
index 000000000..bf68c6f3f
--- /dev/null
+++ b/regression/ebmc/ic3/not_supported3.desc
@@ -0,0 +1,7 @@
+CORE
+not_supported3.sv
+--ic3
+^no support for assumptions$
+^EXIT=1$
+^SIGNAL=0$
+--
diff --git a/regression/ebmc/ic3/not_supported3.sv b/regression/ebmc/ic3/not_supported3.sv
new file mode 100644
index 000000000..4f4eea6d7
--- /dev/null
+++ b/regression/ebmc/ic3/not_supported3.sv
@@ -0,0 +1,13 @@
+module main(input clk);
+
+  reg my_bit;
+
+  initial my_bit=0;
+
+  always @(posedge clk)
+    my_bit = !my_bit;
+
+  // no support for assumptions
+  p0: assume property (my_bit == 0);
+
+endmodule
diff --git a/src/ic3/m1ain.cc b/src/ic3/m1ain.cc
index 41a7753b2..aa32eb183 100644
--- a/src/ic3/m1ain.cc
+++ b/src/ic3/m1ain.cc
@@ -117,6 +117,16 @@ int ic3_enginet::operator()()
       return 1;
     }
 
+    // No support for assumptions
+    for(auto &property : properties.properties)
+    {
+      if(property.is_assumed())
+      {
+        message.error() << "no support for assumptions" << messaget::eom;
+        return 1;
+      }
+    }
+
     std::size_t number_of_properties = 0;
 
     for(auto &property : properties.properties)