diff options
Diffstat (limited to 'test/regress/regress0')
-rw-r--r-- | test/regress/regress0/arith/Makefile.am | 1 | ||||
-rw-r--r-- | test/regress/regress0/arith/fuzz_3-eq.smt | 46 |
2 files changed, 47 insertions, 0 deletions
diff --git a/test/regress/regress0/arith/Makefile.am b/test/regress/regress0/arith/Makefile.am index a039f028b..700c59b8e 100644 --- a/test/regress/regress0/arith/Makefile.am +++ b/test/regress/regress0/arith/Makefile.am @@ -8,6 +8,7 @@ TESTS = \ arith.02.cvc \ arith.03.cvc \ delta-minimized-row-vector-bug.smt \ + fuzz_3-eq.smt \ leq.01.smt \ miplibtrick.smt diff --git a/test/regress/regress0/arith/fuzz_3-eq.smt b/test/regress/regress0/arith/fuzz_3-eq.smt new file mode 100644 index 000000000..ef44444b7 --- /dev/null +++ b/test/regress/regress0/arith/fuzz_3-eq.smt @@ -0,0 +1,46 @@ +(benchmark fuzzsmt +:logic QF_LRA +:extrafuns ((v0 Real)) +:extrafuns ((v2 Real)) +:extrafuns ((v1 Real)) +:status sat +:formula +(let (?n1 2) +(let (?n2 (* ?n1 ?n1)) +(let (?n3 (~ v0)) +(let (?n4 (* ?n1 ?n3)) +(let (?n5 (- ?n1 ?n1)) +(let (?n6 (- ?n5 v0)) +(let (?n7 (- ?n4 ?n6)) +(flet ($n8 (= ?n2 ?n7)) +(flet ($n9 false) +(let (?n10 (ite $n9 ?n1 v1)) +(let (?n11 (+ ?n1 v2)) +(flet ($n12 (= ?n10 ?n11)) +(let (?n13 (ite $n9 v0 ?n2)) +(let (?n14 (~ ?n1)) +(let (?n15 (ite $n9 ?n14 ?n1)) +(flet ($n16 (= ?n13 ?n15)) +(flet ($n17 (= ?n1 ?n7)) +(let (?n18 (+ ?n1 ?n1)) +(flet ($n19 (= v2 ?n18)) +(let (?n20 (ite $n19 v2 ?n1)) +(let (?n21 (ite $n17 ?n18 ?n20)) +(flet ($n22 (= ?n21 ?n2)) +(let (?n23 (ite $n9 ?n21 ?n2)) +(flet ($n24 (= ?n23 ?n1)) +(flet ($n25 (= ?n7 ?n2)) +(flet ($n26 (iff $n24 $n25)) +(let (?n27 (~ ?n7)) +(flet ($n28 (= ?n27 ?n1)) +(let (?n29 (ite $n28 ?n1 ?n1)) +(flet ($n30 (= ?n1 ?n29)) +(flet ($n31 (implies $n26 $n30)) +(flet ($n32 (implies $n9 $n9)) +(flet ($n33 (if_then_else $n22 $n31 $n32)) +(flet ($n34 (and $n9 $n33)) +(flet ($n35 (if_then_else $n16 $n34 $n9)) +(flet ($n36 (iff $n12 $n35)) +(flet ($n37 (and $n8 $n36)) +$n37 +)))))))))))))))))))))))))))))))))))))) |