ebmc: re-enable IC3

kroening · kroening · commit 9125a0655aa9 · 2023-12-10T11:49:55.000-08:00
This fixes the IC3 to ebmc interface and re-enables the tests.
diff --git a/regression/ebmc/ic3/bobcount.desc b/regression/ebmc/ic3/bobcount.desc
@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 bobcount.sv
 --ic3
 ^property HOLDS
diff --git a/regression/ebmc/ic3/bobmiterbm1multi.1033.desc b/regression/ebmc/ic3/bobmiterbm1multi.1033.desc
@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 bobmiterbm1multi.sv
 --ic3 --property bobmiterbm1multi.property.1033
 ^property HOLDS
diff --git a/regression/ebmc/ic3/bobmiterbm1multi.1080.desc b/regression/ebmc/ic3/bobmiterbm1multi.1080.desc
@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 bobmiterbm1multi.sv
 --ic3 --property bobmiterbm1multi.property.1080
 ^property FAILED
diff --git a/regression/ebmc/ic3/eijks208o.desc b/regression/ebmc/ic3/eijks208o.desc
@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 eijks208o.sv
 --ic3
 ^property HOLDS
diff --git a/regression/ebmc/ic3/non_inductive1.desc b/regression/ebmc/ic3/non_inductive1.desc
@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 non_inductive1.sv
 --ic3 --property main.property.p0
 ^property HOLDS$
diff --git a/regression/ebmc/ic3/pdtvispeterson.desc b/regression/ebmc/ic3/pdtvispeterson.desc
@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 pdtvispeterson.sv
 --ic3
 ^property HOLDS
diff --git a/regression/ebmc/ic3/ringp0.desc b/regression/ebmc/ic3/ringp0.desc
@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 ringp0.sv
 --ic3
 ^property FAILED
diff --git a/regression/ebmc/ic3/sm98a7multi.desc b/regression/ebmc/ic3/sm98a7multi.desc
@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 sm98a7multi.sv
 --ic3 --property sm98a7multi.property.2 --constr
 ^property FAILED
diff --git a/regression/ebmc/ic3/visbakery.desc b/regression/ebmc/ic3/visbakery.desc
@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 visbakery.sv
 --ic3
 ^property FAILED
diff --git a/regression/ebmc/ic3/viseisenberg.desc b/regression/ebmc/ic3/viseisenberg.desc
@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 viseisenberg.sv
 --ic3
 ^property FAILED
diff --git a/src/ic3/m1ain.cc b/src/ic3/m1ain.cc
@@ -61,6 +61,9 @@ int ic3_enginet::operator()()
       return 2;
     }
 
+    properties = ebmc_propertiest::from_command_line(
+      cmdline, transition_system, message.get_message_handler());
+
     if(properties.properties.empty())
     {
       message.error() << "no properties" << messaget::eom;

Original file line number	Diff line number	Diff line change
`@@ -1,4 +1,4 @@`
`1`		`-KNOWNBUG`
	`1`	`+CORE`
`2`	`2`	`bobcount.sv`
`3`	`3`	`--ic3`
`4`	`4`	`^property HOLDS`