diff options
author | Morgan Deters <mdeters@gmail.com> | 2010-08-18 03:59:26 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2010-08-18 03:59:26 +0000 |
commit | 29c72e0fd6d0161de275060bbd05370394f1f708 (patch) | |
tree | b19b68eca57c0905d68cc24cefaa5f730121a4c6 /test/regress/regress0/uf/eq_diamond14.reduced.smt | |
parent | 08a57829cdd0ef4c02fee349b4b721d3e4a3f6d1 (diff) |
more tests, configuration for UF
Diffstat (limited to 'test/regress/regress0/uf/eq_diamond14.reduced.smt')
-rw-r--r-- | test/regress/regress0/uf/eq_diamond14.reduced.smt | 88 |
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 +))))))))))))))))))))))))))))))))))))))))))))))))))) |