1 files changed, 88 insertions, 0 deletions
diff --git a/test/regress/regress0/uf/eq_diamond14.reduced.smt b/test/regress/regress0/uf/eq_diamond14.reduced.smt
new file mode 100644
index 000000000..b41e4536d
--- /dev/null
+++ b/test/regress/regress0/uf/eq_diamond14.reduced.smt
@@ -0,0 +1,88 @@
+(benchmark eq_diamond14_reduced
+:logic QF_UF
+:source { Reduced by delta debugger from eq_diamond14 to fix a UF bug. }
+:status unsat
+:extrasorts (V)
+:extrafuns ((x13 V))
+:extrafuns ((x0 V))
+:extrafuns ((y12 V))
+:extrafuns ((x12 V))
+:extrafuns ((z11 V))
+:extrafuns ((x11 V))
+:extrafuns ((y11 V))
+:extrafuns ((z10 V))
+:extrafuns ((x10 V))
+:extrafuns ((y10 V))
+:extrafuns ((y9 V))
+:extrafuns ((x9 V))
+:extrafuns ((y8 V))
+:extrafuns ((x8 V))
+:extrafuns ((y7 V))
+:extrafuns ((x7 V))
+:extrafuns ((y6 V))
+:extrafuns ((x6 V))
+:extrafuns ((y5 V))
+:extrafuns ((x5 V))
+:extrafuns ((y4 V))
+:extrafuns ((x4 V))
+:extrafuns ((y3 V))
+:extrafuns ((x3 V))
+:extrafuns ((y2 V))
+:extrafuns ((x2 V))
+:extrafuns ((y1 V))
+:extrafuns ((x1 V))
+:extrafuns ((y0 V))
+:status unknown
+:formula
+(flet ($n1 (= x0 y0))
+(flet ($n2 (= y0 x1))
+(flet ($n3 (and $n1 $n2))
+(flet ($n4 (= x1 y1))
+(flet ($n5 (= y1 x2))
+(flet ($n6 (and $n4 $n5))
+(flet ($n7 (= x2 y2))
+(flet ($n8 (= y2 x3))
+(flet ($n9 (and $n7 $n8))
+(flet ($n10 (= x3 y3))
+(flet ($n11 (= y3 x4))
+(flet ($n12 (and $n10 $n11))
+(flet ($n13 (= x4 y4))
+(flet ($n14 (= y4 x5))
+(flet ($n15 (and $n13 $n14))
+(flet ($n16 (= x5 y5))
+(flet ($n17 (= y5 x6))
+(flet ($n18 (and $n16 $n17))
+(flet ($n19 (= x6 y6))
+(flet ($n20 (= y6 x7))
+(flet ($n21 (and $n19 $n20))
+(flet ($n22 (= x7 y7))
+(flet ($n23 (= y7 x8))
+(flet ($n24 (and $n22 $n23))
+(flet ($n25 (= x8 y8))
+(flet ($n26 (= y8 x9))
+(flet ($n27 (and $n25 $n26))
+(flet ($n28 (= x9 y9))
+(flet ($n29 (= y9 x10))
+(flet ($n30 (and $n28 $n29))
+(flet ($n31 false)
+(flet ($n32 (= y10 x11))
+(flet ($n33 (and $n31 $n32))
+(flet ($n34 (= x10 z10))
+(flet ($n35 (= x11 z10))
+(flet ($n36 (and $n34 $n35))
+(flet ($n37 (or $n33 $n36))
+(flet ($n38 (= x11 y11))
+(flet ($n39 (= y11 x12))
+(flet ($n40 (and $n38 $n39))
+(flet ($n41 (= x11 z11))
+(flet ($n42 (= x12 z11))
+(flet ($n43 (and $n41 $n42))
+(flet ($n44 (or $n40 $n43))
+(flet ($n45 (= x12 y12))
+(flet ($n46 (= y12 x13))
+(flet ($n47 (and $n45 $n46))
+(flet ($n48 (= x0 x13))
+(flet ($n49 (not $n48))
+(flet ($n50 (and $n3 $n6 $n9 $n12 $n15 $n18 $n21 $n24 $n27 $n30 $n37 $n44 $n47 $n49))
+$n50
+)))))))))))))))))))))))))))))))))))))))))))))))))))