diff options
author | Andres Noetzli <andres.noetzli@gmail.com> | 2019-09-26 17:52:37 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2019-09-26 17:52:37 -0700 |
commit | 3aafd4a2ced87f0fd82ebe5279b73c84552502d5 (patch) | |
tree | 2e96b3cf82d4a1d2c74bb5a6b3227d5afb3716d1 /test/regress/regress3/eq_diamond14.smtv1.smt2 | |
parent | 9ba1854be7d798a899a2b46c2707d376938c5d18 (diff) | |
parent | 923abd7000a2ab6e3c0776c59d159bdc3a4d9a52 (diff) |
Merge branch 'master' into splitEqRew
Diffstat (limited to 'test/regress/regress3/eq_diamond14.smtv1.smt2')
-rw-r--r-- | test/regress/regress3/eq_diamond14.smtv1.smt2 | 54 |
1 files changed, 54 insertions, 0 deletions
diff --git a/test/regress/regress3/eq_diamond14.smtv1.smt2 b/test/regress/regress3/eq_diamond14.smtv1.smt2 new file mode 100644 index 000000000..e055c6cee --- /dev/null +++ b/test/regress/regress3/eq_diamond14.smtv1.smt2 @@ -0,0 +1,54 @@ +(set-option :incremental false) +(set-info :source "Generating minimum transitivity constraints in P-time for deciding Equality Logic, +Ofer Strichman and Mirron Rozanov, +SMT Workshop 2005. + +Translator: Leonardo de Moura.") +(set-info :status unsat) +(set-info :category "crafted") +(set-info :difficulty "0") +(set-logic QF_UF) +(declare-sort U 0) +(declare-fun x0 () U) +(declare-fun y0 () U) +(declare-fun z0 () U) +(declare-fun x1 () U) +(declare-fun y1 () U) +(declare-fun z1 () U) +(declare-fun x2 () U) +(declare-fun y2 () U) +(declare-fun z2 () U) +(declare-fun x3 () U) +(declare-fun y3 () U) +(declare-fun z3 () U) +(declare-fun x4 () U) +(declare-fun y4 () U) +(declare-fun z4 () U) +(declare-fun x5 () U) +(declare-fun y5 () U) +(declare-fun z5 () U) +(declare-fun x6 () U) +(declare-fun y6 () U) +(declare-fun z6 () U) +(declare-fun x7 () U) +(declare-fun y7 () U) +(declare-fun z7 () U) +(declare-fun x8 () U) +(declare-fun y8 () U) +(declare-fun z8 () U) +(declare-fun x9 () U) +(declare-fun y9 () U) +(declare-fun z9 () U) +(declare-fun x10 () U) +(declare-fun y10 () U) +(declare-fun z10 () U) +(declare-fun x11 () U) +(declare-fun y11 () U) +(declare-fun z11 () U) +(declare-fun x12 () U) +(declare-fun y12 () U) +(declare-fun z12 () U) +(declare-fun x13 () U) +(declare-fun y13 () U) +(declare-fun z13 () U) +(check-sat-assuming ( (and (or (and (= x0 y0) (= y0 x1)) (and (= x0 z0) (= z0 x1))) (or (and (= x1 y1) (= y1 x2)) (and (= x1 z1) (= z1 x2))) (or (and (= x2 y2) (= y2 x3)) (and (= x2 z2) (= z2 x3))) (or (and (= x3 y3) (= y3 x4)) (and (= x3 z3) (= z3 x4))) (or (and (= x4 y4) (= y4 x5)) (and (= x4 z4) (= z4 x5))) (or (and (= x5 y5) (= y5 x6)) (and (= x5 z5) (= z5 x6))) (or (and (= x6 y6) (= y6 x7)) (and (= x6 z6) (= z6 x7))) (or (and (= x7 y7) (= y7 x8)) (and (= x7 z7) (= z7 x8))) (or (and (= x8 y8) (= y8 x9)) (and (= x8 z8) (= z8 x9))) (or (and (= x9 y9) (= y9 x10)) (and (= x9 z9) (= z9 x10))) (or (and (= x10 y10) (= y10 x11)) (and (= x10 z10) (= z10 x11))) (or (and (= x11 y11) (= y11 x12)) (and (= x11 z11) (= z11 x12))) (or (and (= x12 y12) (= y12 x13)) (and (= x12 z12) (= z12 x13))) (not (= x0 x13))) )) |