Merge pull request #904 from diffblue/ic3-interface

IC3: use property_checker interface

Author: tautschnig

regression/ebmc/ic3/bobcount.desc

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

regression/ebmc/ic3/bobmiterbm1multi.1033.desc

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

regression/ebmc/ic3/bobmiterbm1multi.1080.desc

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

regression/ebmc/ic3/eijks208o.desc

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

regression/ebmc/ic3/non_inductive1.desc

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

regression/ebmc/ic3/pdtvispeterson.desc

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

regression/ebmc/ic3/ringp0.desc

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

regression/ebmc/ic3/sm98a7multi.desc

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

regression/ebmc/ic3/unconstrained_initial.desc

@@ -1,7 +1,7 @@
 KNOWNBUG
 unconstrained_initial.sv
 --ic3
-^EXIT=1$
+^EXIT=10$
 ^SIGNAL=0$
 ^property FAILED
 ^cex verification is ok

regression/ebmc/ic3/visbakery.desc

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