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

6 files changed, 50 insertions, 6 deletions

diff --git a/test/regress/regress0/Makefile.am b/test/regress/regress0/Makefile.am
index 792754a48..7f18fc12a 100644
--- a/test/regress/regress0/Makefile.am
+++ b/test/regress/regress0/Makefile.am
@@ -94,7 +94,11 @@ BUG_TESTS = \
 	bug168.smt \
 	bug187.smt2 \
 	bug220.smt2 \
+	bug233.cvc \
 	bug239.smt \
+	bug288.smt \
+	bug288b.smt \
+	bug288c.smt \
 	buggy-ite.smt2 \
 	bug303.smt2 \
 	bug310.cvc \
@@ -103,11 +107,6 @@ BUG_TESTS = \
 TESTS =	$(SMT_TESTS) $(SMT2_TESTS) $(CVC_TESTS) $(BUG_TESTS)
 
 EXTRA_DIST = $(TESTS) \
-	bug216.smt2 \
-	bug216.smt2.expect \
-	bug288b.smt \
-	bug288c.smt \
-	bug288.smt \
 	simplification_bug4.smt2.expect
 
 if CVC4_BUILD_PROFILE_COMPETITION
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/bug216.smt2 b/test/regress/regress0/push-pop/bug216.smt2
index 78e0f716c..78e0f716c 100644
--- a/test/regress/regress0/bug216.smt2
+++ b/test/regress/regress0/push-pop/bug216.smt2
diff --git a/test/regress/regress0/bug216.smt2.expect b/test/regress/regress0/push-pop/bug216.smt2.expect
index 9a8435b2d..9a8435b2d 100644
--- a/test/regress/regress0/bug216.smt2.expect
+++ b/test/regress/regress0/push-pop/bug216.smt2.expect
diff --git a/test/regress/regress0/queries0.cvc b/test/regress/regress0/push-pop/bug233.cvc
index c951aaf2e..c951aaf2e 100644
--- a/test/regress/regress0/queries0.cvc
+++ b/test/regress/regress0/push-pop/bug233.cvc
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)