1 files changed, 52 insertions, 0 deletions
diff --git a/test/regress/regress0/aufbv/fuzz03.delta01.smt b/test/regress/regress0/aufbv/fuzz03.delta01.smt
new file mode 100644
index 000000000..f1abfed11
--- /dev/null
+++ b/test/regress/regress0/aufbv/fuzz03.delta01.smt
@@ -0,0 +1,52 @@
+(benchmark fuzzsmt
+:logic QF_AUFBV
+:extrafuns ((a8 Array[14:12]))
+:extrafuns ((v1 BitVec[5]))
+:status sat
+:formula
+(let (?n1 bv1[14])
+(let (?n2 bv1[12])
+(let (?n3 (store a8 ?n1 ?n2))
+(flet ($n4 (bvugt v1 v1))
+(let (?n5 bv1[1])
+(let (?n6 bv0[1])
+(let (?n7 (ite $n4 ?n5 ?n6))
+(let (?n8 (sign_extend[13] ?n7))
+(let (?n9 (store ?n3 ?n8 ?n2))
+(let (?n10 bv0[12])
+(let (?n11 (store ?n9 ?n1 ?n10))
+(let (?n12 bv0[14])
+(let (?n13 (select ?n3 ?n12))
+(let (?n14 (zero_extend[2] ?n13))
+(let (?n15 (store ?n11 ?n14 ?n10))
+(let (?n16 (select ?n15 ?n12))
+(flet ($n17 (bvsgt ?n16 ?n10))
+(let (?n18 (bvnor ?n2 ?n10))
+(let (?n19 (zero_extend[2] ?n18))
+(let (?n20 (store ?n9 ?n19 ?n10))
+(flet ($n21 (= a8 ?n9))
+(let (?n22 (ite $n21 ?n5 ?n6))
+(let (?n23 (sign_extend[13] ?n22))
+(let (?n24 (select ?n20 ?n23))
+(let (?n25 (zero_extend[2] ?n24))
+(let (?n26 (select ?n3 ?n25))
+(flet ($n27 (bvuge ?n10 ?n26))
+(flet ($n28 (= ?n9 ?n15))
+(flet ($n29 false)
+(flet ($n30 (bvsle ?n24 ?n10))
+(flet ($n31 (if_then_else $n28 $n29 $n30))
+(let (?n32 (sign_extend[11] ?n5))
+(flet ($n33 (= ?n9 ?n20))
+(let (?n34 (ite $n33 ?n5 ?n6))
+(let (?n35 (sign_extend[13] ?n34))
+(let (?n36 (select ?n3 ?n35))
+(let (?n37 (bvor ?n18 ?n36))
+(flet ($n38 (bvsge ?n32 ?n37))
+(flet ($n39 (if_then_else $n31 $n38 $n31))
+(flet ($n40 (implies $n27 $n39))
+(let (?n41 (store a8 ?n12 ?n10))
+(flet ($n42 (= ?n3 ?n41))
+(flet ($n43 (or $n40 $n42))
+(flet ($n44 (implies $n17 $n43))
+$n44
+)))))))))))))))))))))))))))))))))))))))))))))