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/regress/regress0/bug576.smt2 | |
parent | 429e6250b70ebd6e1f2bb31ddfebfb61bf10a3e5 (diff) |
Some fixes to symmetry breaker (resolves bug 576).
Diffstat (limited to 'test/regress/regress0/bug576.smt2')
-rw-r--r-- | test/regress/regress0/bug576.smt2 | 27 |
1 files changed, 27 insertions, 0 deletions
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) |