diff options
author | Morgan Deters <mdeters@cs.nyu.edu> | 2014-08-01 15:08:06 -0400 |
---|---|---|
committer | Morgan Deters <mdeters@cs.nyu.edu> | 2014-08-04 13:25:23 -0400 |
commit | 7adf1f2ba37912da65d86d811dd1fd9d572fc747 (patch) | |
tree | 06c3572104faecd824a0ec0889254ef42c4627fd /test | |
parent | 429e6250b70ebd6e1f2bb31ddfebfb61bf10a3e5 (diff) |
Some fixes to symmetry breaker (resolves bug 576).
Diffstat (limited to 'test')
-rw-r--r-- | test/regress/regress0/Makefile.am | 4 | ||||
-rw-r--r-- | test/regress/regress0/bug576.smt2 | 27 | ||||
-rw-r--r-- | test/regress/regress0/bug576a.smt2 | 48 |
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) |