From: Dejan Jovanović <dejan.jovanovic@gmail.com>
Date: Fri, 8 Jun 2012 20:00:13 +0000 (+0000)
Subject: very small fast example for the bv fail
X-Git-Tag: cvc5-1.0.0~8102
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=dbbca593b8724a03f9cd018a00af4ef7e20dfa8b;p=cvc5.git

very small fast example for the bv fail
---

diff --git a/test/regress/regress0/bv/fuzz15.delta01.smt b/test/regress/regress0/bv/fuzz15.delta01.smt
new file mode 100644
index 000000000..f3eb57e17
--- /dev/null
+++ b/test/regress/regress0/bv/fuzz15.delta01.smt
@@ -0,0 +1,107 @@
+(benchmark fuzzsmt
+:logic QF_BV
+:extrafuns ((v11 BitVec[8]))
+:extrafuns ((v12 BitVec[8]))
+:extrafuns ((v10 BitVec[12]))
+:extrafuns ((v2 BitVec[10]))
+:extrafuns ((v8 BitVec[11]))
+:extrafuns ((v17 BitVec[8]))
+:extrafuns ((v5 BitVec[13]))
+:extrafuns ((v0 BitVec[15]))
+:extrafuns ((v14 BitVec[14]))
+:extrafuns ((v19 BitVec[10]))
+:status unknown
+:formula
+(let (?n1 (sign_extend[2] v11))
+(let (?n2 (sign_extend[6] ?n1))
+(let (?n3 (zero_extend[2] v14))
+(flet ($n4 (bvult ?n2 ?n3))
+(flet ($n5 (not $n4))
+(let (?n6 bv0[12])
+(flet ($n7 (bvslt ?n6 v10))
+(let (?n8 bv1[1])
+(let (?n9 bv0[1])
+(let (?n10 (ite $n7 ?n8 ?n9))
+(let (?n11 (sign_extend[15] ?n10))
+(let (?n12 bv0[10])
+(flet ($n13 (bvslt ?n12 v19))
+(let (?n14 (ite $n13 ?n8 ?n9))
+(flet ($n15 (= ?n8 ?n14))
+(let (?n16 bv0[14])
+(let (?n17 (bvxnor v14 ?n16))
+(let (?n18 (extract[9:0] v0))
+(let (?n19 (sign_extend[4] ?n18))
+(let (?n20 bv6240[14])
+(let (?n21 (bvxnor ?n19 ?n20))
+(let (?n22 (ite $n15 ?n17 ?n21))
+(let (?n23 (zero_extend[2] ?n22))
+(let (?n24 (bvsub ?n11 ?n23))
+(let (?n25 bv0[16])
+(flet ($n26 (bvugt ?n24 ?n25))
+(flet ($n27 (not $n26))
+(flet ($n28 false)
+(let (?n29 (zero_extend[2] v8))
+(let (?n30 bv0[15])
+(flet ($n31 (bvsle v0 ?n30))
+(let (?n32 (ite $n31 ?n8 ?n9))
+(let (?n33 (zero_extend[12] ?n32))
+(let (?n34 (bvshl ?n29 ?n33))
+(flet ($n35 (bvsge ?n25 ?n3))
+(let (?n36 (ite $n35 ?n8 ?n9))
+(let (?n37 (zero_extend[12] ?n36))
+(flet ($n38 (bvugt ?n34 ?n37))
+(flet ($n39 (not $n38))
+(flet ($n40 (distinct ?n3 ?n25))
+(let (?n41 (ite $n40 ?n8 ?n9))
+(let (?n42 (sign_extend[14] ?n41))
+(flet ($n43 (bvsge ?n42 ?n30))
+(flet ($n44 (or $n28 $n39 $n43))
+(let (?n45 bv0[13])
+(let (?n46 (sign_extend[2] v17))
+(let (?n47 (zero_extend[3] ?n46))
+(flet ($n48 (distinct ?n45 ?n47))
+(let (?n49 (ite $n48 ?n8 ?n9))
+(let (?n50 (sign_extend[14] ?n49))
+(let (?n51 (bvnot ?n30))
+(flet ($n52 (bvult ?n50 ?n51))
+(let (?n53 (sign_extend[2] v14))
+(flet ($n54 (bvuge ?n25 ?n53))
+(flet ($n55 (not $n54))
+(flet ($n56 (or $n28 $n52 $n55))
+(let (?n57 (sign_extend[6] v12))
+(flet ($n58 (bvsgt ?n57 ?n21))
+(let (?n59 (ite $n58 ?n8 ?n9))
+(flet ($n60 (bvugt ?n8 ?n59))
+(let (?n61 (zero_extend[1] ?n29))
+(let (?n62 (bvmul ?n20 ?n61))
+(flet ($n63 (bvsgt ?n45 v5))
+(let (?n64 (ite $n63 ?n8 ?n9))
+(let (?n65 (zero_extend[13] ?n64))
+(flet ($n66 (bvule ?n62 ?n65))
+(flet ($n67 (not $n66))
+(let (?n68 (sign_extend[4] v2))
+(let (?n69 (bvxnor ?n16 ?n68))
+(let (?n70 (zero_extend[2] ?n46))
+(let (?n71 (zero_extend[2] ?n70))
+(flet ($n72 (= ?n69 ?n71))
+(let (?n73 (extract[6:3] ?n29))
+(let (?n74 (sign_extend[12] ?n73))
+(flet ($n75 (bvsle ?n25 ?n74))
+(let (?n76 (sign_extend[9] ?n10))
+(let (?n77 (bvxnor v2 ?n76))
+(let (?n78 (extract[3:3] ?n77))
+(flet ($n79 (= ?n8 ?n78))
+(let (?n80 (ite $n79 ?n16 ?n57))
+(flet ($n81 (bvugt ?n1 ?n12))
+(let (?n82 (ite $n81 ?n8 ?n9))
+(let (?n83 (bvnot ?n82))
+(let (?n84 (zero_extend[13] ?n83))
+(flet ($n85 (bvult ?n80 ?n84))
+(let (?n86 (ite $n85 ?n8 ?n9))
+(let (?n87 (zero_extend[12] ?n86))
+(let (?n88 (zero_extend[1] ?n87))
+(flet ($n89 (= ?n16 ?n88))
+(flet ($n90 (or $n28 $n75 $n89))
+(flet ($n91 (and $n5 $n27 $n44 $n56 $n60 $n67 $n72 $n90))
+$n91
+))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))