1 files changed, 45 insertions, 0 deletions
diff --git a/test/regress/regress0/auflia/fuzz01.delta01.smt b/test/regress/regress0/auflia/fuzz01.delta01.smt
new file mode 100644
index 000000000..cec8c91a5
--- /dev/null
+++ b/test/regress/regress0/auflia/fuzz01.delta01.smt
@@ -0,0 +1,45 @@
+(benchmark fuzzsmt
+:logic QF_AUFLIA
+:extrapreds ((p1 Array))
+:extrafuns ((f1 Array Array Array Array))
+:extrafuns ((v0 Int))
+:extrafuns ((v4 Array))
+:extrafuns ((v3 Array))
+:extrafuns ((v1 Int))
+:extrapreds ((p0 Int))
+:extrafuns ((f0 Int Int Int Int))
+:status unknown
+:formula
+(let (?n1 0)
+(flet ($n2 (> ?n1 v0))
+(let (?n3 (store v4 v1 ?n1))
+(flet ($n4 (p0 v0))
+(let (?n5 (store v4 ?n1 v0))
+(let (?n6 (ite $n4 ?n5 v4))
+(let (?n7 (ite $n2 ?n3 ?n6))
+(flet ($n8 (p0 ?n1))
+(let (?n9 1)
+(let (?n10 (ite $n8 ?n9 ?n1))
+(flet ($n11 (= ?n1 ?n10))
+(flet ($n12 (p0 ?n9))
+(let (?n13 (ite $n12 ?n9 ?n1))
+(let (?n14 3)
+(let (?n15 (* v1 ?n14))
+(flet ($n16 (< ?n13 ?n15))
+(flet ($n17 (p1 ?n5))
+(let (?n18 (ite $n17 ?n3 ?n5))
+(let (?n19 (ite $n16 v3 ?n18))
+(let (?n20 (ite $n11 ?n19 v3))
+(let (?n21 (f1 ?n7 v4 ?n20))
+(flet ($n22 (p1 ?n21))
+(let (?n23 (f0 ?n1 ?n1 ?n1))
+(flet ($n24 (p0 ?n23))
+(let (?n25 (ite $n24 ?n9 ?n1))
+(flet ($n26 (<= ?n15 ?n25))
+(let (?n27 (ite $n26 v4 v3))
+(let (?n28 (ite $n16 v3 ?n5))
+(let (?n29 (f1 v4 ?n27 ?n28))
+(flet ($n30 (p1 ?n29))
+(flet ($n31 (or $n22 $n30))
+$n31
+))))))))))))))))))))))))))))))))