Skip to content

Commit 994f2eb

Browse files
committed
polished the version of ic3_bugs branch before submitting PR
1 parent 26f1354 commit 994f2eb

32 files changed

+63
-457
lines changed

regression/ebmc/ic3/exmp1/test.desc

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -2,6 +2,6 @@ CORE
22
pdtvispeterson.sv
33
--ic3
44
^property HOLDS
5-
^verification is ok
5+
^inductive invariant verification is ok
66
--
7-
^verification failed
7+
^inductive invariant verification failed

regression/ebmc/ic3/exmp2/test.desc

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -2,6 +2,6 @@ CORE
22
bobcount.sv
33
--ic3
44
^property HOLDS
5-
^verification is ok
5+
^inductive invariant verification is ok
66
--
7-
^verification failed
7+
^inductive invariant verification failed

regression/ebmc/ic3/exmp3/test.desc

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -2,6 +2,6 @@ CORE
22
viseisenberg.sv
33
--ic3
44
^property FAILED
5-
^verification is ok
5+
^cex verification is ok
66
--
7-
^verification failed
7+
^cex verification failed

regression/ebmc/ic3/exmp4/test.desc

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -2,6 +2,6 @@ CORE
22
visbakery.sv
33
--ic3
44
^property FAILED
5-
^verification is ok
5+
^cex verification is ok
66
--
7-
^verification failed
7+
^cex verification failed

regression/ebmc/ic3/exmp5/test.desc

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -2,6 +2,6 @@ CORE
22
ringp0.sv
33
--ic3
44
^property FAILED
5-
^verification is ok
5+
^cex verification is ok
66
--
7-
^verification failed
7+
^cex verification failed

regression/ebmc/ic3/exmp6/test.desc

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -2,6 +2,6 @@ CORE
22
eijks208o.sv
33
--ic3
44
^property HOLDS
5-
^verification is ok
5+
^inductive invariant verification is ok
66
--
7-
^verification failed
7+
^inductive invariant verification failed

regression/ebmc/ic3/exmp7/test.desc

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -2,6 +2,6 @@ CORE
22
bobmiterbm1multi.sv
33
--ic3 --property bobmiterbm1multi.property.1033
44
^property HOLDS
5-
^verification is ok
5+
^inductive invariant verification is ok
66
--
7-
^verification failed
7+
^inductive invariant verification failed

regression/ebmc/ic3/exmp8/test.desc

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -2,6 +2,6 @@ CORE
22
bobmiterbm1multi.sv
33
--ic3 --property bobmiterbm1multi.property.1080
44
^property FAILED
5-
^verification is ok
5+
^cex verification is ok
66
--
7-
^verification failed
7+
^cex verification failed

regression/ebmc/ic3/exmp9/test.desc

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -2,6 +2,6 @@ CORE
22
sm98a7multi.sv
33
--ic3 --property sm98a7multi.property.2 --constr
44
^property FAILED
5-
^verification is ok
5+
^cex verification is ok
66
--
7-
^verification failed
7+
^cex verification failed

regression/ebmc/ic3/non_inductive1/test.desc

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -2,5 +2,6 @@ CORE
22
non_inductive.sv
33
--ic3 --property main.property.p0
44
^property HOLDS$
5-
^verification is ok
5+
^inductive invariant verification is ok
66
--
7+
^inductive invariant verification failed

0 commit comments

Comments
 (0)