diff options
Diffstat (limited to 'test/regress/regress0/bug576a.smt2')
-rw-r--r-- | test/regress/regress0/bug576a.smt2 | 48 |
1 files changed, 48 insertions, 0 deletions
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) |