recategorize eq_diamond14 as a regress2 test (instead of regress0)

diff --git a/test/regress/regress0/uf/Makefile.am b/test/regress/regress0/uf/Makefile.am
index f5c97241e5a1a3308e34b2a9b4055ca8d09d7f24..a5ab380ce8aa0645b35215a17949602c7e41ff38 100644 (file)
--- 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 (file)
index f89d0e3..0000000
--- 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))))

diff --git a/test/regress/regress2/Makefile.am b/test/regress/regress2/Makefile.am
index 1651865fdcc85896ae4491303671bd6458da0022..28a814274e705418258e2d2ef35f7d7d9869194e 100644 (file)
--- a/test/regress/regress2/Makefile.am
+++ b/test/regress/regress2/Makefile.am
@@ -21,7 +21,8 @@ TESTS =       bmc-galileo-8.smt \
        bmc-ibm-7.smt \
        friedman_n6_i4.smt \
        hole9.cvc \
-       qwh.35.405.shuffled-as.sat03-1651.smt
+       qwh.35.405.shuffled-as.sat03-1651.smt \
+       eq_diamond14.smt
 
 EXTRA_DIST = $(TESTS)
 

diff --git a/test/regress/regress2/eq_diamond14.smt b/test/regress/regress2/eq_diamond14.smt
new file mode 100644 (file)
index 0000000..f89d0e3
--- /dev/null
+++ b/test/regress/regress2/eq_diamond14.smt
@@ -0,0 +1,41 @@
+(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))))