Some fixes to symmetry breaker (resolves bug 576).

3 files changed, 78 insertions, 1 deletions

diff --git a/test/regress/regress0/Makefile.am b/test/regress/regress0/Makefile.am
index cc691f8d2..55a588362 100644
--- a/test/regress/regress0/Makefile.am
+++ b/test/regress/regress0/Makefile.am
@@ -160,7 +160,9 @@ BUG_TESTS = \
 	bug543.smt2 \
 	bug544.smt2 \
 	bug548a.smt2 \
-	bug567.smt2
+	bug567.smt2 \
+	bug576.smt2 \
+	bug576a.smt2
 
 TESTS =	$(SMT_TESTS) $(SMT2_TESTS) $(CVC_TESTS) $(TPTP_TESTS) $(BUG_TESTS)
 
diff --git a/test/regress/regress0/bug576.smt2 b/test/regress/regress0/bug576.smt2
new file mode 100644
index 000000000..c9ca241d7
--- /dev/null
+++ b/test/regress/regress0/bug576.smt2
@@ -0,0 +1,27 @@
+(set-logic QF_UF)
+(set-info :status sat)
+(declare-sort var 0)
+(declare-sort reg 0)
+(declare-fun var5_1 () var)
+(declare-fun b_1 () var)
+(declare-fun a_1 () var)
+(declare-fun r0 () reg)
+(declare-fun r1 () reg)
+(declare-fun r2 () reg)
+(declare-fun r3 () reg)
+(assert (not (= r0 r1)))
+(assert (not (= r0 r2)))
+(assert (not (= r0 r3)))
+(assert (not (= r1 r2)))
+(assert (not (= r1 r3)))
+(assert (not (= r2 r3)))
+(declare-fun assign (var) reg)
+(assert (or (= (assign var5_1) r0) (= (assign var5_1) r1) (= (assign var5_1) r2) (= (assign var5_1) r3) ))
+(assert (or (= (assign b_1) r1) ))
+(assert (or (= (assign a_1) r0) ))
+(assert (not (= (assign b_1) (assign a_1))))
+(assert (= (assign var5_1) r0))
+(assert (= (assign b_1) r1))
+(assert (= (assign a_1) r0))
+(check-sat)
+(exit)
diff --git a/test/regress/regress0/bug576a.smt2 b/test/regress/regress0/bug576a.smt2
new file mode 100644
index 000000000..00487a183
--- /dev/null
+++ b/test/regress/regress0/bug576a.smt2
@@ -0,0 +1,48 @@
+(set-logic QF_UF)
+(set-info :status sat)
+(declare-sort var 0)
+(declare-sort reg 0)
+(declare-fun a1_1 () var)
+(declare-fun a2_1 () var)
+(declare-fun c_3 () var)
+(declare-fun c_4 () var)
+(declare-fun b_3 () var)
+(declare-fun r0 () reg)
+(declare-fun r1 () reg)
+(declare-fun r2 () reg)
+(declare-fun r3 () reg)
+(declare-fun r4 () reg)
+(declare-fun r6 () reg)
+(assert (not (= r0 r1)))
+(assert (not (= r0 r2)))
+(assert (not (= r0 r3)))
+(assert (not (= r0 r4)))
+(assert (not (= r0 r6)))
+(assert (not (= r1 r2)))
+(assert (not (= r1 r3)))
+(assert (not (= r1 r4)))
+(assert (not (= r1 r6)))
+(assert (not (= r2 r3)))
+(assert (not (= r2 r4)))
+(assert (not (= r2 r6)))
+(assert (not (= r3 r4)))
+(assert (not (= r3 r6)))
+(assert (not (= r4 r6)))
+(declare-fun assign (var) reg)
+(assert (or (= (assign a1_1) r0) (= (assign a1_1) r1) (= (assign a1_1) r2) (= (assign a1_1) r3) (= (assign a1_1) r4) (= (assign a1_1) r6) ))
+(assert (or (= (assign a2_1) r0) (= (assign a2_1) r1) (= (assign a2_1) r2) (= (assign a2_1) r3) (= (assign a2_1) r4) (= (assign a2_1) r6) ))
+(assert (or (= (assign c_3) r0) (= (assign c_3) r1) (= (assign c_3) r2) (= (assign c_3) r3) (= (assign c_3) r4) (= (assign c_3) r6) ))
+(assert (or (= (assign c_4) r0) (= (assign c_4) r1) (= (assign c_4) r2) (= (assign c_4) r3) (= (assign c_4) r4) (= (assign c_4) r6) ))
+(assert (or (= (assign b_3) r0) (= (assign b_3) r1) (= (assign b_3) r2) (= (assign b_3) r3) (= (assign b_3) r4) (= (assign b_3) r6) ))
+(assert (not (= (assign a1_1) (assign c_4))))
+(assert (not (= (assign a2_1) (assign c_3))))
+(assert (not (= (assign a2_1) (assign b_3))))
+(assert (not (= (assign c_3) (assign b_3))))
+(assert (not (= (assign c_4) (assign b_3))))
+(assert (= (assign a1_1) r0))
+(assert (= (assign a2_1) r2))
+(assert (= (assign c_3) r1))
+(assert (= (assign c_4) r1))
+(assert (= (assign b_3) r0))
+(check-sat)
+(exit)