diff options
Diffstat (limited to 'test/regress/regress0/arith/bug443.delta01.smt')
-rw-r--r-- | test/regress/regress0/arith/bug443.delta01.smt | 37 |
1 files changed, 0 insertions, 37 deletions
diff --git a/test/regress/regress0/arith/bug443.delta01.smt b/test/regress/regress0/arith/bug443.delta01.smt deleted file mode 100644 index 0b8a0d971..000000000 --- a/test/regress/regress0/arith/bug443.delta01.smt +++ /dev/null @@ -1,37 +0,0 @@ -(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 -)))))))))))))))))))))))))))) |