additional model gen and SMT-LIBv2 compliance work: (get-assignment) now supported; work on Result type (biggest noticeable change is that CVC4 now outputs lowercase "sat" and "unsat"), Options class moved to src/smt, to allow for future work on runtime configuration via (set-option) command

18 files changed, 18 insertions, 18 deletions

diff --git a/test/regress/regress0/precedence/and-not.cvc b/test/regress/regress0/precedence/and-not.cvc
index 0de37db83..547633bf1 100644
--- a/test/regress/regress0/precedence/and-not.cvc
+++ b/test/regress/regress0/precedence/and-not.cvc
@@ -1,4 +1,4 @@
-% EXPECT: VALID
+% EXPECT: valid
 % Simple test for right precedence of AND and NOT.
 
 A, B: BOOLEAN;
diff --git a/test/regress/regress0/precedence/and-xor.cvc b/test/regress/regress0/precedence/and-xor.cvc
index 7b29bb95e..dfc03bf22 100644
--- a/test/regress/regress0/precedence/and-xor.cvc
+++ b/test/regress/regress0/precedence/and-xor.cvc
@@ -1,4 +1,4 @@
-% EXPECT: VALID
+% EXPECT: valid
 % Simple test for right precedence of XOR and AND.
 
 A, B, C: BOOLEAN;
diff --git a/test/regress/regress0/precedence/bool-cmp.cvc b/test/regress/regress0/precedence/bool-cmp.cvc
index ef1345cc1..d19ab9aae 100644
--- a/test/regress/regress0/precedence/bool-cmp.cvc
+++ b/test/regress/regress0/precedence/bool-cmp.cvc
@@ -1,4 +1,4 @@
-% EXPECT: VALID
+% EXPECT: valid
 % Simple test for right precedence of comparisons and booleans
 
 x , y, z: INT;
diff --git a/test/regress/regress0/precedence/cmp-plus.cvc b/test/regress/regress0/precedence/cmp-plus.cvc
index af2823fcf..aff12548f 100644
--- a/test/regress/regress0/precedence/cmp-plus.cvc
+++ b/test/regress/regress0/precedence/cmp-plus.cvc
@@ -1,4 +1,4 @@
-% EXPECT: VALID
+% EXPECT: valid
 % Simple test for right precedence of comparisons and plus/minus
 
 x, y, z: INT;
diff --git a/test/regress/regress0/precedence/eq-fun.cvc b/test/regress/regress0/precedence/eq-fun.cvc
index e85b4a3e6..f207071b3 100644
--- a/test/regress/regress0/precedence/eq-fun.cvc
+++ b/test/regress/regress0/precedence/eq-fun.cvc
@@ -1,4 +1,4 @@
-% EXPECT: VALID
+% EXPECT: valid
 % Simple test for right precedence of function application and =
 
 T : TYPE;
diff --git a/test/regress/regress0/precedence/iff-assoc.cvc b/test/regress/regress0/precedence/iff-assoc.cvc
index b92354753..a496ccf16 100644
--- a/test/regress/regress0/precedence/iff-assoc.cvc
+++ b/test/regress/regress0/precedence/iff-assoc.cvc
@@ -1,4 +1,4 @@
-% EXPECT: VALID
+% EXPECT: valid
 % Simple test for right associativity of <=>
 
 A, B, C: BOOLEAN;
diff --git a/test/regress/regress0/precedence/iff-implies.cvc b/test/regress/regress0/precedence/iff-implies.cvc
index 0115fc319..ee2e2479f 100644
--- a/test/regress/regress0/precedence/iff-implies.cvc
+++ b/test/regress/regress0/precedence/iff-implies.cvc
@@ -1,4 +1,4 @@
-% EXPECT: VALID
+% EXPECT: valid
 % Simple test for right precedence of <=> and =>.
 
 A, B, C: BOOLEAN;
diff --git a/test/regress/regress0/precedence/implies-assoc.cvc b/test/regress/regress0/precedence/implies-assoc.cvc
index d465df313..b87038a99 100644
--- a/test/regress/regress0/precedence/implies-assoc.cvc
+++ b/test/regress/regress0/precedence/implies-assoc.cvc
@@ -1,4 +1,4 @@
-% EXPECT: VALID
+% EXPECT: valid
 % Simple test for right associativity of =>
 
 A, B, C: BOOLEAN;
diff --git a/test/regress/regress0/precedence/implies-iff.cvc b/test/regress/regress0/precedence/implies-iff.cvc
index f8c813ceb..4a2aa18a8 100644
--- a/test/regress/regress0/precedence/implies-iff.cvc
+++ b/test/regress/regress0/precedence/implies-iff.cvc
@@ -1,4 +1,4 @@
-% EXPECT: VALID
+% EXPECT: valid
 % Simple test for right precedence of <=> and =>.
 
 A, B, C: BOOLEAN;
diff --git a/test/regress/regress0/precedence/implies-or.cvc b/test/regress/regress0/precedence/implies-or.cvc
index 24edb4ecd..266daae40 100644
--- a/test/regress/regress0/precedence/implies-or.cvc
+++ b/test/regress/regress0/precedence/implies-or.cvc
@@ -1,4 +1,4 @@
-% EXPECT: VALID
+% EXPECT: valid
 % Simple test for right precedence of => and OR.
 
 A, B, C: BOOLEAN;
diff --git a/test/regress/regress0/precedence/not-and.cvc b/test/regress/regress0/precedence/not-and.cvc
index 8c849a0d9..048d971b4 100644
--- a/test/regress/regress0/precedence/not-and.cvc
+++ b/test/regress/regress0/precedence/not-and.cvc
@@ -1,4 +1,4 @@
-% EXPECT: VALID
+% EXPECT: valid
 % Simple test for right precedence of AND and NOT.
 
 A, B, C: BOOLEAN;
diff --git a/test/regress/regress0/precedence/not-eq.cvc b/test/regress/regress0/precedence/not-eq.cvc
index 6d712d43d..cf4a0e4a5 100644
--- a/test/regress/regress0/precedence/not-eq.cvc
+++ b/test/regress/regress0/precedence/not-eq.cvc
@@ -1,4 +1,4 @@
-% EXPECT: VALID
+% EXPECT: valid
 % Simple test for right precedence of = and NOT.
 
 A, B: INT;
diff --git a/test/regress/regress0/precedence/or-implies.cvc b/test/regress/regress0/precedence/or-implies.cvc
index d91f79dc8..13f3a316e 100644
--- a/test/regress/regress0/precedence/or-implies.cvc
+++ b/test/regress/regress0/precedence/or-implies.cvc
@@ -1,4 +1,4 @@
-% EXPECT: VALID
+% EXPECT: valid
 % Simple test for right precedence of => and OR.
 
 A, B, C: BOOLEAN;
diff --git a/test/regress/regress0/precedence/or-xor.cvc b/test/regress/regress0/precedence/or-xor.cvc
index 47cc87c76..4e19be584 100644
--- a/test/regress/regress0/precedence/or-xor.cvc
+++ b/test/regress/regress0/precedence/or-xor.cvc
@@ -1,4 +1,4 @@
-% EXPECT: VALID
+% EXPECT: valid
 % Simple test for right precedence of OR and XOR.
 
 A, B, C: BOOLEAN;
diff --git a/test/regress/regress0/precedence/plus-mult.cvc b/test/regress/regress0/precedence/plus-mult.cvc
index ecd34f583..9300ae6c4 100644
--- a/test/regress/regress0/precedence/plus-mult.cvc
+++ b/test/regress/regress0/precedence/plus-mult.cvc
@@ -1,4 +1,4 @@
-% EXPECT: VALID
+% EXPECT: valid
 % Simple test for right precedence of plus/minus and mult/divide
 
 a, b, c, d, e: INT;
diff --git a/test/regress/regress0/precedence/xor-and.cvc b/test/regress/regress0/precedence/xor-and.cvc
index ba3f48a7f..950c8ee94 100644
--- a/test/regress/regress0/precedence/xor-and.cvc
+++ b/test/regress/regress0/precedence/xor-and.cvc
@@ -1,4 +1,4 @@
-% EXPECT: VALID
+% EXPECT: valid
 % Simple test for right precedence of XOR and AND.
 
 A, B, C: BOOLEAN;
diff --git a/test/regress/regress0/precedence/xor-assoc.cvc b/test/regress/regress0/precedence/xor-assoc.cvc
index 27911332c..a356f9b3a 100644
--- a/test/regress/regress0/precedence/xor-assoc.cvc
+++ b/test/regress/regress0/precedence/xor-assoc.cvc
@@ -1,4 +1,4 @@
-% EXPECT: VALID
+% EXPECT: valid
 % Simple test for left associativity of XOR
 
 A, B, C: BOOLEAN;
diff --git a/test/regress/regress0/precedence/xor-or.cvc b/test/regress/regress0/precedence/xor-or.cvc
index 2b4436937..837e4c575 100644
--- a/test/regress/regress0/precedence/xor-or.cvc
+++ b/test/regress/regress0/precedence/xor-or.cvc
@@ -1,4 +1,4 @@
-% EXPECT: VALID
+% EXPECT: valid
 % Simple test for right precedence of OR and XOR.
 
 A, B, C: BOOLEAN;