1 files changed, 129 insertions, 0 deletions
diff --git a/test/regress/regress0/bv/fuzz19.delta01.smt b/test/regress/regress0/bv/fuzz19.delta01.smt
new file mode 100644
index 000000000..e6395f1aa
--- /dev/null
+++ b/test/regress/regress0/bv/fuzz19.delta01.smt
@@ -0,0 +1,129 @@
+(benchmark fuzzsmt
+:logic QF_BV
+:extrafuns ((v0 BitVec[4]))
+:extrafuns ((v1 BitVec[4]))
+:extrafuns ((v2 BitVec[4]))
+:extrafuns ((v3 BitVec[4]))
+:extrafuns ((v4 BitVec[4]))
+:extrafuns ((v5 BitVec[4]))
+:status unknown
+:formula
+(flet ($n1 true)
+(let (?n2 (extract[0:0] v2))
+(let (?n3 (zero_extend[1] ?n2))
+(let (?n4 (zero_extend[2] ?n3))
+(let (?n5 bv0[4])
+(flet ($n6 (distinct ?n5 v4))
+(let (?n7 bv1[1])
+(let (?n8 bv0[1])
+(let (?n9 (ite $n6 ?n7 ?n8))
+(let (?n10 (sign_extend[3] ?n9))
+(let (?n11 (bvadd ?n4 ?n10))
+(flet ($n12 (bvsle ?n11 ?n5))
+(let (?n13 (ite $n12 ?n7 ?n8))
+(let (?n14 (sign_extend[3] ?n13))
+(let (?n15 bv11[4])
+(flet ($n16 (bvsge ?n15 v5))
+(let (?n17 (ite $n16 ?n7 ?n8))
+(let (?n18 (zero_extend[3] ?n17))
+(flet ($n19 (bvult ?n14 ?n18))
+(let (?n20 (ite $n19 ?n7 ?n8))
+(flet ($n21 (bvsge v2 ?n15))
+(let (?n22 (ite $n21 ?n7 ?n8))
+(let (?n23 (sign_extend[3] ?n22))
+(let (?n24 (bvlshr v4 ?n23))
+(let (?n25 (bvmul v5 ?n24))
+(flet ($n26 (bvslt ?n25 v2))
+(let (?n27 (ite $n26 ?n7 ?n8))
+(flet ($n28 (bvsge ?n20 ?n27))
+(let (?n29 (ite $n28 ?n7 ?n8))
+(let (?n30 (zero_extend[3] ?n29))
+(flet ($n31 (bvugt v3 ?n30))
+(flet ($n32 (bvugt v0 ?n5))
+(let (?n33 (ite $n32 ?n7 ?n8))
+(let (?n34 (zero_extend[3] ?n33))
+(flet ($n35 (bvsge v1 ?n34))
+(let (?n36 (ite $n35 ?n7 ?n8))
+(let (?n37 (sign_extend[3] ?n36))
+(let (?n38 (bvashr v1 ?n37))
+(let (?n39 bv10[4])
+(flet ($n40 (bvult ?n38 ?n39))
+(flet ($n41 false)
+(let (?n42 (bvashr v3 ?n4))
+(let (?n43 bv1[4])
+(flet ($n44 (bvule ?n42 ?n43))
+(let (?n45 (ite $n44 ?n7 ?n8))
+(let (?n46 (zero_extend[3] ?n45))
+(flet ($n47 (bvsge ?n46 ?n38))
+(let (?n48 (ite $n47 ?n7 ?n8))
+(let (?n49 (sign_extend[1] ?n48))
+(let (?n50 bv0[2])
+(flet ($n51 (bvsge ?n49 ?n50))
+(let (?n52 (ite $n51 ?n7 ?n8))
+(flet ($n53 (= ?n27 ?n52))
+(let (?n54 (ite $n53 ?n7 ?n8))
+(flet ($n55 (bvult ?n25 v1))
+(let (?n56 (ite $n55 ?n7 ?n8))
+(let (?n57 (bvadd ?n7 ?n56))
+(let (?n58 (bvneg v4))
+(flet ($n59 (bvslt ?n58 ?n5))
+(let (?n60 (ite $n59 ?n7 ?n8))
+(let (?n61 (bvashr ?n57 ?n60))
+(let (?n62 (sign_extend[3] ?n61))
+(let (?n63 (sign_extend[3] ?n54))
+(flet ($n64 (bvugt ?n62 ?n63))
+(let (?n65 (ite $n64 ?n7 ?n8))
+(flet ($n66 (distinct ?n54 ?n65))
+(flet ($n67 (not $n66))
+(let (?n68 (sign_extend[3] ?n45))
+(let (?n69 (bvcomp v3 ?n68))
+(flet ($n70 (bvule ?n7 ?n69))
+(flet ($n71 (or $n41 $n67 $n70))
+(let (?n72 (sign_extend[3] ?n7))
+(flet ($n73 (bvsle ?n72 ?n58))
+(let (?n74 (sign_extend[3] ?n2))
+(flet ($n75 (distinct ?n5 ?n74))
+(let (?n76 (ite $n75 ?n7 ?n8))
+(let (?n77 (sign_extend[3] ?n76))
+(flet ($n78 (bvsle ?n25 ?n5))
+(let (?n79 (ite $n78 ?n7 ?n8))
+(let (?n80 (zero_extend[3] ?n79))
+(let (?n81 (bvxnor ?n11 ?n80))
+(flet ($n82 (bvsle ?n77 ?n81))
+(flet ($n83 (not $n82))
+(let (?n84 (extract[2:0] v3))
+(let (?n85 (concat ?n84 ?n52))
+(flet ($n86 (bvsle ?n85 ?n72))
+(flet ($n87 (bvuge ?n5 ?n10))
+(let (?n88 (ite $n87 ?n7 ?n8))
+(let (?n89 (zero_extend[3] ?n88))
+(let (?n90 (bvmul v4 ?n89))
+(flet ($n91 (bvsgt ?n90 ?n5))
+(let (?n92 (ite $n91 ?n7 ?n8))
+(let (?n93 (sign_extend[3] ?n92))
+(flet ($n94 (bvsgt ?n18 ?n5))
+(let (?n95 (ite $n94 ?n7 ?n8))
+(flet ($n96 (bvult v4 v4))
+(let (?n97 (ite $n96 ?n7 ?n8))
+(flet ($n98 (bvsge ?n95 ?n97))
+(let (?n99 (ite $n98 ?n7 ?n8))
+(let (?n100 (zero_extend[3] ?n99))
+(flet ($n101 (bvsge ?n93 ?n100))
+(let (?n102 (ite $n101 ?n7 ?n8))
+(flet ($n103 (bvsle ?n8 ?n102))
+(flet ($n104 (or $n41 $n86 $n103))
+(let (?n105 (zero_extend[3] ?n20))
+(flet ($n106 (bvuge ?n5 ?n105))
+(flet ($n107 (bvule ?n25 ?n5))
+(let (?n108 (ite $n107 ?n7 ?n8))
+(let (?n109 (sign_extend[2] ?n108))
+(flet ($n110 (= ?n2 ?n7))
+(let (?n111 (ite $n110 ?n25 ?n42))
+(flet ($n112 (bvsle ?n5 ?n111))
+(let (?n113 (ite $n112 ?n7 ?n8))
+(let (?n114 (extract[1:0] ?n38))
+(let (?n115 (concat ?n113 ?n114))
+(flet ($n116 (= ?n109 ?n115))
+(flet ($n117 (and $n31 $n40 $n71 $n73 $n83 $n104 $n106 $n116))
+$n117
+))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))