Merge pull request #2 from diffblue/fix/named_properties_ebmc_ic3

support named properties in EBMC/ic3

Author: mgudemann

regression/ebmc/ic3/non_inductive1/non_inductive.sv

@@ -0,0 +1,39 @@
+// this example is a representation of the circuit in
+// "SAT-Based Verification without State Space Traversal"
+//   by Per Bjesse & Koen Claessen (FMCAD 2000)
+module main(clock, s3, out);
+   input clock;
+   input s3;
+   output out;
+
+   wire   s5=  s4 | s3;
+   wire   s6= ~s4 |~s3;
+   wire   s9= ~s8 |~s7;
+   wire   s10= s9 |~s3;
+   wire   s11=(~s6 | s10)&( s6 |~s10);
+
+   reg    s4;
+   reg    s7;
+   reg    s8;
+
+   initial s4=0;
+   initial s7=0;
+   initial s8=0;
+
+   always @ (posedge clock) s4 <= ~s5;
+   always @ (posedge clock) s7 <= ~s3;
+   always @ (posedge clock) s8 <= s9;
+   assign out=s11;
+   // not inductive for any k
+   p0: assert property (s11);
+   p1: assert property ((s7 |~s4) & s11);
+   // 3-inductive
+   p2: assert property ((s8 |~s4) & s11);
+   // 2-inductive
+   p3: assert property ((~s8 | ~s7 | s4) & s11);
+   p4: assert property ((s8 |~s4) & (s7 |~s4) & s11);
+   p5: assert property ((s7 |~s4) & (~s8 | ~s7 | s4) & s11);
+   p6: assert property ((s8 |~s4) & (~s8 | ~s7 | s4) & s11);
+   // inductive
+   p7: assert property ((s7 |~s4) & (s8 |~s4) & (~s8 | ~s7 | s4) & s11);
+endmodule

regression/ebmc/ic3/non_inductive1/test.desc

@@ -0,0 +1,6 @@
+CORE
+non_inductive.sv
+--ic3 --prop 0
+^property HOLDS$
+^verification is ok
+--

src/ic3/r6ead_input.cc

@@ -90,20 +90,18 @@ bool ic3_enginet::find_prop(propertyt &Prop)
     std::cout  << properties.size() << " properties\n";
     exit(100);
   }
-  
-  for(const auto &p : properties) {
-    std::string Sn;
-    irep_idt Nm = p.name;
-    short_name(Sn,Nm);
-    int ind = stoi(Sn);
-    if (ind-1 == Ci.prop_ind) {
+
+  size_t idx=0;
+  for(const auto &p : properties)
+  {
+    if(idx == Ci.prop_ind)
+    {
       Prop = p;
       return(true);
     }
+    idx++;
   }
-
-  return(false);
-
+  return false;
 } /* end of function find_prop */
 
 /*==================================