Skip to content

Commit fe2d2fa

Browse files
authored
Merge pull request #273 from diffblue/ic3
ebmc: re-enable IC3
2 parents 27ece61 + b142b96 commit fe2d2fa

22 files changed

+24
-7083
lines changed

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

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,8 @@
11
CORE
22
bobcount.sv
33
--ic3
4+
^EXIT=2$
5+
^SIGNAL=0$
46
^property HOLDS
57
^inductive invariant verification is ok
68
--

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

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,8 @@
11
CORE
22
bobmiterbm1multi.sv
33
--ic3 --property bobmiterbm1multi.property.1033
4+
^EXIT=2$
5+
^SIGNAL=0$
46
^property HOLDS
57
^inductive invariant verification is ok
68
--

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

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,8 @@
11
CORE
22
bobmiterbm1multi.sv
33
--ic3 --property bobmiterbm1multi.property.1080
4+
^EXIT=1$
5+
^SIGNAL=0$
46
^property FAILED
57
^cex verification is ok
68
--

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

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,8 @@
11
CORE
22
eijks208o.sv
33
--ic3
4+
^EXIT=2$
5+
^SIGNAL=0$
46
^property HOLDS
57
^inductive invariant verification is ok
68
--

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: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,8 @@
11
CORE
2-
non_inductive.sv
2+
non_inductive1.sv
33
--ic3 --property main.property.p0
4+
^EXIT=2$
5+
^SIGNAL=0$
46
^property HOLDS$
57
^inductive invariant verification is ok
68
--

0 commit comments

Comments
 (0)