diff --git a/regression/ebmc/ic3/bobcount.desc b/regression/ebmc/ic3/bobcount.desc
index cada27143..a8320587a 100644
--- a/regression/ebmc/ic3/bobcount.desc
+++ b/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
diff --git a/regression/ebmc/ic3/bobmiterbm1multi.1033.desc b/regression/ebmc/ic3/bobmiterbm1multi.1033.desc
index 4a46e6e95..7639c6df6 100644
--- a/regression/ebmc/ic3/bobmiterbm1multi.1033.desc
+++ b/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
diff --git a/regression/ebmc/ic3/bobmiterbm1multi.1080.desc b/regression/ebmc/ic3/bobmiterbm1multi.1080.desc
index d531e7011..7959f5e1a 100644
--- a/regression/ebmc/ic3/bobmiterbm1multi.1080.desc
+++ b/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
diff --git a/regression/ebmc/ic3/eijks208o.desc b/regression/ebmc/ic3/eijks208o.desc
index c77824181..11a612206 100644
--- a/regression/ebmc/ic3/eijks208o.desc
+++ b/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
diff --git a/regression/ebmc/ic3/non_inductive1.desc b/regression/ebmc/ic3/non_inductive1.desc
index 2c33d649d..fcbc5ef45 100644
--- a/regression/ebmc/ic3/non_inductive1.desc
+++ b/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
diff --git a/regression/ebmc/ic3/pdtvispeterson.desc b/regression/ebmc/ic3/pdtvispeterson.desc
index d8c011a16..63b814c25 100644
--- a/regression/ebmc/ic3/pdtvispeterson.desc
+++ b/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
diff --git a/regression/ebmc/ic3/ringp0.desc b/regression/ebmc/ic3/ringp0.desc
index 0f1790625..b6f812632 100644
--- a/regression/ebmc/ic3/ringp0.desc
+++ b/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
diff --git a/regression/ebmc/ic3/sm98a7multi.desc b/regression/ebmc/ic3/sm98a7multi.desc
index 3139728a8..6cd7a3c9c 100644
--- a/regression/ebmc/ic3/sm98a7multi.desc
+++ b/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
diff --git a/regression/ebmc/ic3/visbakery.desc b/regression/ebmc/ic3/visbakery.desc
index 32ffdb41c..57312d05e 100644
--- a/regression/ebmc/ic3/visbakery.desc
+++ b/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
diff --git a/regression/ebmc/ic3/viseisenberg.desc b/regression/ebmc/ic3/viseisenberg.desc
index c771a4867..98deeca79 100644
--- a/regression/ebmc/ic3/viseisenberg.desc
+++ b/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
diff --git a/src/ic3/m1ain.cc b/src/ic3/m1ain.cc
index 41a7753b2..fe9304a71 100644
--- a/src/ic3/m1ain.cc
+++ b/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 */
 
 /* ======================