add tests

diff --git a/test/regress/regress0/sets/Makefile.am b/test/regress/regress0/sets/Makefile.am
index fe53838be8c2033fa2a759da81f51fd51868944a..6d718553d1db93679cf3e710f155f8ea94a6e8db 100644 (file)
--- a/test/regress/regress0/sets/Makefile.am
+++ b/test/regress/regress0/sets/Makefile.am
@@ -55,6 +55,10 @@ TESTS =      \
        eqtest.smt2 \
        mar2014/lemmabug-ListElts317minimized.smt2 \
        mar2014/sharing-preregister.smt2 \
+       mar2014/small.smt2 \
+       mar2014/smaller.smt2 \
+       mar2014/UniqueZipper.hs.1030minimized2.cvc4.smt2 \
+       mar2014/UniqueZipper.hs.1030minimized.cvc4.smt2 \
        emptyset.smt2 \
        error2.smt2
 

diff --git a/test/regress/regress0/sets/mar2014/UniqueZipper.hs.1030minimized.cvc4.smt2 b/test/regress/regress0/sets/mar2014/UniqueZipper.hs.1030minimized.cvc4.smt2
index bdec267b7da0ed19ea002435300eff5414500d90..e6f1873318b63f511e1063c312f7b0b3050d2b82 100644 (file)
--- a/test/regress/regress0/sets/mar2014/UniqueZipper.hs.1030minimized.cvc4.smt2
+++ b/test/regress/regress0/sets/mar2014/UniqueZipper.hs.1030minimized.cvc4.smt2
@@ -1,3 +1,4 @@
+; EXPECT: sat
 (set-logic QF_ALL_SUPPORTED)
 (define-sort Elt () Int)
 (define-sort mySet () (Set Elt ))

diff --git a/test/regress/regress0/sets/mar2014/UniqueZipper.hs.1030minimized2.cvc4.smt2 b/test/regress/regress0/sets/mar2014/UniqueZipper.hs.1030minimized2.cvc4.smt2
index 7898318f525ac5df0ca53d972320cefa7574e693..b8a27b967c5070dbf677ce6ee532525a717a9d5b 100644 (file)
--- a/test/regress/regress0/sets/mar2014/UniqueZipper.hs.1030minimized2.cvc4.smt2
+++ b/test/regress/regress0/sets/mar2014/UniqueZipper.hs.1030minimized2.cvc4.smt2
@@ -1,3 +1,4 @@
+; EXPECT: sat
 (set-logic QF_ALL_SUPPORTED)
 (define-sort Elt () Int)
 (define-sort mySet () (Set Elt ))

diff --git a/test/regress/regress0/sets/mar2014/small.smt2 b/test/regress/regress0/sets/mar2014/small.smt2
index ff896a5f067aadf84bd37f0f6cee1832b5a7997f..838a279198b671555cdcdd5ddf6c2f4540f967f6 100644 (file)
--- a/test/regress/regress0/sets/mar2014/small.smt2
+++ b/test/regress/regress0/sets/mar2014/small.smt2
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --simplfication=none
+; COMMAND-LINE: --simplification=none
 
 ; demostrates core issue with UniqueZipper.hs.1030minimized.cvc4.smt2
 ; unlike original benchmark, this is unsat.

diff --git a/test/regress/regress0/sets/mar2014/smaller.smt2 b/test/regress/regress0/sets/mar2014/smaller.smt2
index 307cc87ab058184d523466d0c51cf2ae79d60119..876311de85fa7749a0f88d0fb9307a0041485189 100644 (file)
--- a/test/regress/regress0/sets/mar2014/smaller.smt2
+++ b/test/regress/regress0/sets/mar2014/smaller.smt2
@@ -1,5 +1,5 @@
 ; EXPECT: sat
-; COMMAND-LINE: --simplfication=none
+; COMMAND-LINE: --simplification=none
 
 ; demostrates core issue with UniqueZipper.hs.1030minimized.cvc4.smt2
 ; fails check-model, even though answer is correct