Merge pull request #899 from diffblue/ic3-result

IC3: use report_results

regression/ebmc/ic3/bobcount.desc

@@ -1,9 +1,10 @@
 CORE
 bobcount.sv
 --ic3
-^EXIT=2$
-^SIGNAL=0$
+^\[bobcount\.assert\.1\] always !bobcount\.p0: PROVED$
 ^property HOLDS
 ^inductive invariant verification is ok
+^EXIT=2$
+^SIGNAL=0$
 --
 ^inductive invariant verification failed

regression/ebmc/ic3/bobmiterbm1multi.1033.desc

@@ -1,9 +1,10 @@
 CORE
 bobmiterbm1multi.sv
 --ic3 --property bobmiterbm1multi.assert.1033
-^EXIT=2$
-^SIGNAL=0$
+^\[bobmiterbm1multi\.assert\.1033\] always !bobmiterbm1multi\.p1032: PROVED$
 ^property HOLDS
 ^inductive invariant verification is ok
+^EXIT=2$
+^SIGNAL=0$
 --
 ^inductive invariant verification failed

regression/ebmc/ic3/bobmiterbm1multi.1080.desc

@@ -1,9 +1,10 @@
 CORE
 bobmiterbm1multi.sv
 --ic3 --property bobmiterbm1multi.assert.1080
-^EXIT=1$
-^SIGNAL=0$
+^\[bobmiterbm1multi\.assert\.1080\] always !bobmiterbm1multi\.p1079: REFUTED$
 ^property FAILED
 ^cex verification is ok
+^EXIT=1$
+^SIGNAL=0$
 --
 ^cex verification failed

regression/ebmc/ic3/eijks208o.desc

@@ -1,9 +1,10 @@
 CORE
 eijks208o.sv
 --ic3
-^EXIT=2$
-^SIGNAL=0$
+^\[eijks208o\.assert\.1\] always !eijks208o\.p0: PROVED$
 ^property HOLDS
 ^inductive invariant verification is ok
+^EXIT=2$
+^SIGNAL=0$
 --
 ^inductive invariant verification failed

regression/ebmc/ic3/non_inductive1.desc

@@ -1,9 +1,10 @@
 CORE
 non_inductive1.sv
 --ic3 --property main.p0
-^EXIT=2$
-^SIGNAL=0$
+^\[main\.p0\] always main\.s11: PROVED$
 ^property HOLDS$
 ^inductive invariant verification is ok
+^EXIT=2$
+^SIGNAL=0$
 --
 ^inductive invariant verification failed

regression/ebmc/ic3/pdtvispeterson.desc

@@ -1,9 +1,10 @@
 CORE
 pdtvispeterson.sv
 --ic3
-^EXIT=2$
-^SIGNAL=0$
+^\[pdtvispeterson\.assert\.1\] always !pdtvispeterson\.p0: PROVED$
 ^property HOLDS
 ^inductive invariant verification is ok
+^EXIT=2$
+^SIGNAL=0$
 --
 ^inductive invariant verification failed

regression/ebmc/ic3/ringp0.desc

@@ -1,9 +1,10 @@
 CORE
 ringp0.sv
 --ic3
-^EXIT=1$
-^SIGNAL=0$
+^\[ringp0\.assert\.1\] always !ringp0\.p0: REFUTED$
 ^property FAILED
 ^cex verification is ok
+^EXIT=1$
+^SIGNAL=0$
 --
 ^cex verification failed

regression/ebmc/ic3/sm98a7multi.desc

@@ -1,9 +1,10 @@
 CORE
 sm98a7multi.sv
 --ic3 --property sm98a7multi.assert.2 --constr
-^EXIT=1$
-^SIGNAL=0$
+^\[sm98a7multi\.assert\.2\] always !sm98a7multi\.p1: REFUTED$
 ^property FAILED
 ^cex verification is ok
+^EXIT=1$
+^SIGNAL=0$
 --
 ^cex verification failed

regression/ebmc/ic3/visbakery.desc

@@ -1,9 +1,10 @@
 CORE
 visbakery.sv
 --ic3
-^EXIT=1$
-^SIGNAL=0$
+^\[visbakery\.assert\.1\] always !visbakery\.p0: REFUTED$
 ^property FAILED
 ^cex verification is ok
+^EXIT=1$
+^SIGNAL=0$
 --
 ^cex verification failed

regression/ebmc/ic3/viseisenberg.desc

@@ -1,9 +1,10 @@
 CORE
 viseisenberg.sv
 --ic3
-^EXIT=1$
-^SIGNAL=0$
+^\[viseisenberg\.assert\.1\] always !viseisenberg\.p0: REFUTED$
 ^property FAILED
 ^cex verification is ok
+^EXIT=1$
+^SIGNAL=0$
 --
 ^cex verification failed

src/ic3/m1ain.cc

@@ -141,6 +141,46 @@ int ic3_enginet::operator()()
       report_results(cmdline, result, ns, message.get_message_handler());
       return result.exit_code();
     }
+
+    const0 = false;
+    const1 = false;
+    orig_names = false;
+
+    // print_nodes();
+    // print_var_map(std::cout);
+    read_ebmc_input();
+    // print_blif3("tst.blif",Ci.N);
+    if (cmdline.isset("aiger")) {
+      printf("converting to aiger format\n");
+      Ci.print_aiger_format();
+      exit(0);
+    }
+
+    //  printf("Constr_gates.size() = %d\n",Ci.Constr_gates.size()); 
+    int result = Ci.run_ic3();
+
+    // find the first unknown property
+    for(auto &property : properties.properties)
+    {
+      if(property.is_unknown())
+      {
+        switch(result)
+        {
+        case 1: property.refuted(); break;
+        case 2: property.proved(); break;
+        default: property.failure(); break;
+        }
+        break;
+      }
+    }
+
+    {
+      property_checker_resultt result{properties};
+      namespacet ns(transition_system.symbol_table);
+      report_results(cmdline, result, ns, message.get_message_handler());
+    }
+
+    return result;
   }
   catch(const std::string &error_str)
   {
@@ -154,24 +194,6 @@ int ic3_enginet::operator()()
   catch(int)    {
     return 1;
   }
-
-  const0 = false;
-  const1 = false;
-  orig_names = false;
-
-  // print_nodes();
-  // print_var_map(std::cout);
-  read_ebmc_input();
-  // print_blif3("tst.blif",Ci.N);
-  if (cmdline.isset("aiger")) {
-    printf("converting to aiger format\n");
-    Ci.print_aiger_format();
-    exit(0);
-  }
-
-  //  printf("Constr_gates.size() = %d\n",Ci.Constr_gates.size()); 
-  return(Ci.run_ic3());
-
 } /* end of function operator */
 
 /* ======================