adding some regressions to the usual regressions runs; several recently-fixed incremental bugs are closed

5 files changed, 70 insertions, 1 deletions

diff --git a/test/regress/regress0/push-pop/Makefile.am b/test/regress/regress0/push-pop/Makefile.am
index 413b8c60a..624afe856 100644
--- a/test/regress/regress0/push-pop/Makefile.am
+++ b/test/regress/regress0/push-pop/Makefile.am
@@ -23,9 +23,15 @@ CVC_TESTS = \
 SMT2_TESTS = \
 	tiny_bug.smt2
 
+BUG_TESTS = \
+	bug216.smt2 \
+	bug233.cvc
+
 TESTS =	$(SMT_TESTS) $(SMT2_TESTS) $(CVC_TESTS) $(BUG_TESTS)
 
-EXTRA_DIST = $(TESTS) 
+EXTRA_DIST = $(TESTS) \
+	bug216.smt2.expect \
+	bug326.smt2
 
 # synonyms for "check" in this directory
 .PHONY: regress regress0 test
diff --git a/test/regress/regress0/push-pop/bug216.smt2 b/test/regress/regress0/push-pop/bug216.smt2
new file mode 100644
index 000000000..78e0f716c
--- /dev/null
+++ b/test/regress/regress0/push-pop/bug216.smt2
@@ -0,0 +1,8 @@
+(set-logic QF_UF)
+(declare-fun x () Bool)
+(declare-fun y () Bool)
+(assert (=> x y))
+(check-sat) ; returns sat
+(assert (=> y x))
+(assert (and x (not y)))
+(check-sat) ; returns sat --> ERROR
diff --git a/test/regress/regress0/push-pop/bug216.smt2.expect b/test/regress/regress0/push-pop/bug216.smt2.expect
new file mode 100644
index 000000000..9a8435b2d
--- /dev/null
+++ b/test/regress/regress0/push-pop/bug216.smt2.expect
@@ -0,0 +1,4 @@
+% COMMAND-LINE: --incremental
+% EXPECT: sat
+% EXPECT: unsat
+% EXIT: 20
diff --git a/test/regress/regress0/push-pop/bug233.cvc b/test/regress/regress0/push-pop/bug233.cvc
new file mode 100644
index 000000000..c951aaf2e
--- /dev/null
+++ b/test/regress/regress0/push-pop/bug233.cvc
@@ -0,0 +1,12 @@
+% Tests the invariants for multiple queries.
+% COMMAND-LINE: --incremental
+
+a, b: BOOLEAN;
+
+% EXPECT: valid
+QUERY (a AND b) OR NOT (a AND b);
+
+% EXPECT: invalid
+QUERY (a OR b);
+
+% EXIT: 10
diff --git a/test/regress/regress0/push-pop/bug326.smt2 b/test/regress/regress0/push-pop/bug326.smt2
new file mode 100644
index 000000000..3797cb105
--- /dev/null
+++ b/test/regress/regress0/push-pop/bug326.smt2
@@ -0,0 +1,39 @@
+(set-logic AUFLIA)
+
+(declare-fun R (Int Int) Bool)
+
+;; reflexive
+(assert-rewrite ((x Int)) () (R x x) true ())
+
+;; anti-symmetric
+(assert-reduction ((x Int) (y Int)) () ((R x y) (R y x)) (= x y) ())
+
+;; transitive
+(assert-propagation ((x Int) (y Int) (z Int)) () ((R x y) (R y z)) (R x z) ())
+
+
+(declare-fun e1 () Int)
+(declare-fun e2 () Int)
+(declare-fun e3 () Int)
+(declare-fun e4 () Int)
+
+; EXPECT: unsat
+(push);;unsat
+(assert (not (=> (and (R e1 e2) (R e2 e4) (R e1 e3) (R e3 e4) (= e1 e4)) (= e2 e3))))
+(check-sat)
+(pop)
+
+; EXPECT: unsat
+(push);;unsat
+(assert (not (=> (and (R e1 e2) (R e1 e3) (or (R e2 e4) (R e3 e4)) ) (R e1 e4))))
+(check-sat)
+(pop)
+
+; EXPECT: sat
+(push);;sat
+(assert (and (not (R e1 e3)) (R e4 e1)))
+(check-sat)
+(pop)
+
+
+(exit)