IC3: better error message when given assumption

This improves the error handling when giving an assumption to the IC3 engine.

Author: kroening

regression/ebmc/ic3/not_supported3.desc

@@ -0,0 +1,7 @@
+CORE
+not_supported3.sv
+--ic3
+^no support for assumptions$
+^EXIT=1$
+^SIGNAL=0$
+--

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

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)