ebmc: re-enable IC3

This fixes the IC3 to ebmc interface and re-enables the tests.

Author: kroening

regression/ebmc/ic3/bobcount.desc

@@ -1,6 +1,8 @@
-KNOWNBUG
+CORE
 bobcount.sv
 --ic3
+^EXIT=2$
+^SIGNAL=0$
 ^property HOLDS
 ^inductive invariant verification is ok
 --

regression/ebmc/ic3/bobmiterbm1multi.1033.desc

@@ -1,6 +1,8 @@
-KNOWNBUG
+CORE
 bobmiterbm1multi.sv
 --ic3 --property bobmiterbm1multi.property.1033
+^EXIT=2$
+^SIGNAL=0$
 ^property HOLDS
 ^inductive invariant verification is ok
 --

regression/ebmc/ic3/bobmiterbm1multi.1080.desc

@@ -1,6 +1,8 @@
-KNOWNBUG
+CORE
 bobmiterbm1multi.sv
 --ic3 --property bobmiterbm1multi.property.1080
+^EXIT=1$
+^SIGNAL=0$
 ^property FAILED
 ^cex verification is ok
 --

regression/ebmc/ic3/eijks208o.desc

@@ -1,6 +1,8 @@
-KNOWNBUG
+CORE
 eijks208o.sv
 --ic3
+^EXIT=2$
+^SIGNAL=0$
 ^property HOLDS
 ^inductive invariant verification is ok
 --

regression/ebmc/ic3/non_inductive1.desc

@@ -1,6 +1,8 @@
-KNOWNBUG
+CORE
 non_inductive1.sv
 --ic3 --property main.property.p0
+^EXIT=2$
+^SIGNAL=0$
 ^property HOLDS$
 ^inductive invariant verification is ok
 --

regression/ebmc/ic3/pdtvispeterson.desc

@@ -1,6 +1,8 @@
-KNOWNBUG
+CORE
 pdtvispeterson.sv
 --ic3
+^EXIT=2$
+^SIGNAL=0$
 ^property HOLDS
 ^inductive invariant verification is ok
 --

regression/ebmc/ic3/ringp0.desc

@@ -1,6 +1,8 @@
-KNOWNBUG
+CORE
 ringp0.sv
 --ic3
+^EXIT=1$
+^SIGNAL=0$
 ^property FAILED
 ^cex verification is ok
 --

regression/ebmc/ic3/sm98a7multi.desc

@@ -1,6 +1,8 @@
-KNOWNBUG
+CORE
 sm98a7multi.sv
 --ic3 --property sm98a7multi.property.2 --constr
+^EXIT=1$
+^SIGNAL=0$
 ^property FAILED
 ^cex verification is ok
 --

regression/ebmc/ic3/visbakery.desc

@@ -1,6 +1,8 @@
-KNOWNBUG
+CORE
 visbakery.sv
 --ic3
+^EXIT=1$
+^SIGNAL=0$
 ^property FAILED
 ^cex verification is ok
 --

regression/ebmc/ic3/viseisenberg.desc

@@ -1,6 +1,8 @@
-KNOWNBUG
+CORE
 viseisenberg.sv
 --ic3
+^EXIT=1$
+^SIGNAL=0$
 ^property FAILED
 ^cex verification is ok
 --