diff options
author | Morgan Deters <mdeters@gmail.com> | 2010-09-02 08:24:12 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2010-09-02 08:24:12 +0000 |
commit | 81e6b35ed60ef25a4b8da6361f7156456459c37d (patch) | |
tree | 416511267560eab40dee5d7ab8e16bd9a2a9606f /test/regress/regress0/uf | |
parent | ab8e5a034964c45796168e4e140e31d33a51932b (diff) |
recategorize eq_diamond14 as a regress2 test (instead of regress0)
Diffstat (limited to 'test/regress/regress0/uf')
-rw-r--r-- | test/regress/regress0/uf/Makefile.am | 1 | ||||
-rw-r--r-- | test/regress/regress0/uf/eq_diamond14.smt | 41 |
2 files changed, 0 insertions, 42 deletions
diff --git a/test/regress/regress0/uf/Makefile.am b/test/regress/regress0/uf/Makefile.am index f5c97241e..a5ab380ce 100644 --- a/test/regress/regress0/uf/Makefile.am +++ b/test/regress/regress0/uf/Makefile.am @@ -17,7 +17,6 @@ TESTS = \ euf_simp12.smt \ euf_simp13.smt \ eq_diamond1.smt \ - eq_diamond14.smt \ eq_diamond14.reduced.smt \ eq_diamond14.reduced2.smt \ dead_dnd002.smt \ diff --git a/test/regress/regress0/uf/eq_diamond14.smt b/test/regress/regress0/uf/eq_diamond14.smt deleted file mode 100644 index f89d0e3b7..000000000 --- a/test/regress/regress0/uf/eq_diamond14.smt +++ /dev/null @@ -1,41 +0,0 @@ -(benchmark eq_diamond14 -:source{ -Generating minimum transitivity constraints in P-time for deciding Equality Logic, -Ofer Strichman and Mirron Rozanov, -SMT Workshop 2005. - -Translator: Leonardo de Moura. } -:status unsat -:category { crafted } -:logic QF_UF -:difficulty { 0 } -:extrafuns ((x0 U) (y0 U) (z0 U) -(x1 U) (y1 U) (z1 U) -(x2 U) (y2 U) (z2 U) -(x3 U) (y3 U) (z3 U) -(x4 U) (y4 U) (z4 U) -(x5 U) (y5 U) (z5 U) -(x6 U) (y6 U) (z6 U) -(x7 U) (y7 U) (z7 U) -(x8 U) (y8 U) (z8 U) -(x9 U) (y9 U) (z9 U) -(x10 U) (y10 U) (z10 U) -(x11 U) (y11 U) (z11 U) -(x12 U) (y12 U) (z12 U) -(x13 U) (y13 U) (z13 U) -) -:formula (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)))) |