polished the version of ic3_bugs branch before submitting PR

diffblue · May 29, 2017 · e1cb500 · e1cb500
1 parent 2602671
commit e1cb500
Show file tree

Hide file tree

Showing 32 changed files with 63 additions and 457 deletions.
diff --git a/regression/ebmc/ic3/exmp1/test.desc b/regression/ebmc/ic3/exmp1/test.desc
@@ -2,6 +2,6 @@ CORE
 pdtvispeterson.sv
 --ic3
 ^property HOLDS
-^verification is ok
+^inductive invariant verification is ok
 --
-^verification failed
+^inductive invariant verification failed
diff --git a/regression/ebmc/ic3/exmp2/test.desc b/regression/ebmc/ic3/exmp2/test.desc
@@ -2,6 +2,6 @@ CORE
 bobcount.sv
 --ic3
 ^property HOLDS
-^verification is ok
+^inductive invariant verification is ok
 --
-^verification failed
+^inductive invariant verification failed
diff --git a/regression/ebmc/ic3/exmp3/test.desc b/regression/ebmc/ic3/exmp3/test.desc
@@ -2,6 +2,6 @@ CORE
 viseisenberg.sv
 --ic3
 ^property FAILED
-^verification is ok
+^cex verification is ok
 --
-^verification failed
+^cex verification failed
diff --git a/regression/ebmc/ic3/exmp4/test.desc b/regression/ebmc/ic3/exmp4/test.desc
@@ -2,6 +2,6 @@ CORE
 visbakery.sv
 --ic3
 ^property FAILED
-^verification is ok
+^cex verification is ok
 --
-^verification failed
+^cex verification failed
diff --git a/regression/ebmc/ic3/exmp5/test.desc b/regression/ebmc/ic3/exmp5/test.desc
@@ -2,6 +2,6 @@ CORE
 ringp0.sv
 --ic3
 ^property FAILED
-^verification is ok
+^cex verification is ok
 --
-^verification failed
+^cex verification failed
diff --git a/regression/ebmc/ic3/exmp6/test.desc b/regression/ebmc/ic3/exmp6/test.desc
@@ -2,6 +2,6 @@ CORE
 eijks208o.sv
 --ic3
 ^property HOLDS
-^verification is ok
+^inductive invariant verification is ok
 --
-^verification failed
+^inductive invariant verification failed
diff --git a/regression/ebmc/ic3/exmp7/test.desc b/regression/ebmc/ic3/exmp7/test.desc
@@ -2,6 +2,6 @@ CORE
 bobmiterbm1multi.sv
 --ic3 --property bobmiterbm1multi.property.1033
 ^property HOLDS
-^verification is ok
+^inductive invariant verification is ok
 --
-^verification failed
+^inductive invariant verification failed
diff --git a/regression/ebmc/ic3/exmp8/test.desc b/regression/ebmc/ic3/exmp8/test.desc
@@ -2,6 +2,6 @@ CORE
 bobmiterbm1multi.sv
 --ic3 --property bobmiterbm1multi.property.1080
 ^property FAILED
-^verification is ok
+^cex verification is ok
 --
-^verification failed
+^cex verification failed
diff --git a/regression/ebmc/ic3/exmp9/test.desc b/regression/ebmc/ic3/exmp9/test.desc
@@ -2,6 +2,6 @@ CORE
 sm98a7multi.sv
 --ic3 --property sm98a7multi.property.2 --constr
 ^property FAILED
-^verification is ok
+^cex verification is ok
 --
-^verification failed
+^cex verification failed
diff --git a/regression/ebmc/ic3/non_inductive1/test.desc b/regression/ebmc/ic3/non_inductive1/test.desc
@@ -2,5 +2,6 @@ CORE
 non_inductive.sv
 --ic3 --property main.property.p0
 ^property HOLDS$
-^verification is ok
+^inductive invariant verification is ok
 --
+^inductive invariant verification failed
diff --git a/src/ebmc/pproc_all.bat b/src/ebmc/pproc_all.bat
diff --git a/src/ebmc/r1esults_multi/exmps11 b/src/ebmc/r1esults_multi/exmps11
diff --git a/src/ebmc/r1esults_multi/multi_prop.pl b/src/ebmc/r1esults_multi/multi_prop.pl
diff --git a/src/ebmc/r1esults_multi/rpnt.txt b/src/ebmc/r1esults_multi/rpnt.txt
diff --git a/src/ebmc/r1esults_multi/sngl_call.bat b/src/ebmc/r1esults_multi/sngl_call.bat
diff --git a/src/ebmc/r2esults_multi/exmps12 b/src/ebmc/r2esults_multi/exmps12
diff --git a/src/ebmc/r2esults_multi/multi_prop.pl b/src/ebmc/r2esults_multi/multi_prop.pl
diff --git a/src/ebmc/r2esults_multi/rpnt.txt b/src/ebmc/r2esults_multi/rpnt.txt
diff --git a/src/ebmc/r2esults_multi/run_ic3.pl b/src/ebmc/r2esults_multi/run_ic3.pl
diff --git a/src/ebmc/r2esults_multi/sngl_call.bat b/src/ebmc/r2esults_multi/sngl_call.bat