1 files changed, 37 insertions, 0 deletions
diff --git a/test/regress/regress0/arith/bug443.delta01.smt b/test/regress/regress0/arith/bug443.delta01.smt
new file mode 100644
index 000000000..0b8a0d971
--- /dev/null
+++ b/test/regress/regress0/arith/bug443.delta01.smt
@@ -0,0 +1,37 @@
+(benchmark fuzzsmt
+:logic QF_UFLRA
+:extrafuns ((v1 Real))
+:extrafuns ((v2 Real))
+:extrafuns ((v0 Real))
+:extrapreds ((p1 Real))
+:status sat
+:formula
+(let (?n1 0)
+(flet ($n2 (p1 ?n1))
+(let (?n3 1)
+(flet ($n4 (= ?n3 v2))
+(let (?n5 5)
+(let (?n6 (~ ?n5))
+(let (?n7 (* v2 ?n6))
+(let (?n8 (+ ?n7 v1))
+(flet ($n9 (= ?n5 ?n8))
+(let (?n10 (ite $n9 ?n3 v1))
+(flet ($n11 (= ?n7 ?n10))
+(flet ($n12 (p1 v0))
+(let (?n13 (ite $n12 ?n1 v1))
+(flet ($n14 (p1 ?n13))
+(let (?n15 (~ ?n7))
+(let (?n16 (- ?n3 ?n15))
+(flet ($n17 (>= ?n16 ?n8))
+(flet ($n18 (> ?n16 ?n1))
+(flet ($n19 (= ?n8 v0))
+(let (?n20 (ite $n19 ?n8 ?n16))
+(let (?n21 (ite $n18 ?n20 ?n7))
+(let (?n22 (ite $n17 ?n21 v2))
+(flet ($n23 (> ?n22 v1))
+(flet ($n24 (implies $n14 $n23))
+(flet ($n25 (and $n11 $n24))
+(flet ($n26 (implies $n4 $n25))
+(flet ($n27 (xor $n2 $n26))
+$n27
+))))))))))))))))))))))))))))