Skip to content

Commit 6698aa2

Browse files
committed
ebmc: move IC3 tests
This moves the IC3 tests so they can be run by the script and marks them as KNOWNBUG.
1 parent 6806280 commit 6698aa2

21 files changed

+11
-7093
lines changed

regression/ebmc/ic3/exmp2/test.desc renamed to regression/ebmc/ic3/bobcount.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
CORE
1+
KNOWNBUG
22
bobcount.sv
33
--ic3
44
^property HOLDS

regression/ebmc/ic3/exmp7/test.desc renamed to regression/ebmc/ic3/bobmiterbm1multi.1033.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
CORE
1+
KNOWNBUG
22
bobmiterbm1multi.sv
33
--ic3 --property bobmiterbm1multi.property.1033
44
^property HOLDS

regression/ebmc/ic3/exmp8/test.desc renamed to regression/ebmc/ic3/bobmiterbm1multi.1080.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
CORE
1+
KNOWNBUG
22
bobmiterbm1multi.sv
33
--ic3 --property bobmiterbm1multi.property.1080
44
^property FAILED

regression/ebmc/ic3/exmp6/test.desc renamed to regression/ebmc/ic3/eijks208o.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
CORE
1+
KNOWNBUG
22
eijks208o.sv
33
--ic3
44
^property HOLDS

regression/ebmc/ic3/exmp8/bobmiterbm1multi.sv

Lines changed: 0 additions & 7082 deletions
This file was deleted.

regression/ebmc/ic3/non_inductive1/test.desc renamed to regression/ebmc/ic3/non_inductive1.desc

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,5 @@
1-
CORE
2-
non_inductive.sv
1+
KNOWNBUG
2+
non_inductive1.sv
33
--ic3 --property main.property.p0
44
^property HOLDS$
55
^inductive invariant verification is ok

0 commit comments

Comments
 (0)