diff options
Diffstat (limited to 'test/regress/regress0/bv/fuzz07-delta.smt')
-rw-r--r-- | test/regress/regress0/bv/fuzz07-delta.smt | 39 |
1 files changed, 0 insertions, 39 deletions
diff --git a/test/regress/regress0/bv/fuzz07-delta.smt b/test/regress/regress0/bv/fuzz07-delta.smt deleted file mode 100644 index 50bdd4cb2..000000000 --- a/test/regress/regress0/bv/fuzz07-delta.smt +++ /dev/null @@ -1,39 +0,0 @@ -(benchmark fuzzsmt -:logic QF_BV -:extrafuns ((v1 BitVec[2])) -:status unknown -:formula -(let (?n1 bv0[8]) -(let (?n2 bv0[2]) -(let (?n3 bv0[5]) -(let (?n4 (sign_extend[3] v1)) -(flet ($n5 (= ?n3 ?n4)) -(let (?n6 bv1[1]) -(let (?n7 bv0[1]) -(let (?n8 (ite $n5 ?n6 ?n7)) -(let (?n9 (concat ?n8 ?n3)) -(let (?n10 (concat ?n2 ?n9)) -(flet ($n11 (= ?n1 ?n10)) -(flet ($n12 false) -(let (?n13 bv0[4]) -(let (?n14 bv1[2]) -(let (?n15 (bvcomp v1 ?n14)) -(flet ($n16 (bvugt ?n15 ?n7)) -(let (?n17 (ite $n16 ?n6 ?n7)) -(let (?n18 (sign_extend[1] ?n17)) -(let (?n19 (sign_extend[2] ?n18)) -(flet ($n20 (= ?n13 ?n19)) -(flet ($n21 true) -(let (?n22 bv0[16]) -(let (?n23 bv0[3]) -(flet ($n24 (bvsle ?n2 ?n18)) -(let (?n25 (ite $n24 ?n6 ?n7)) -(let (?n26 (zero_extend[2] ?n25)) -(flet ($n27 (distinct ?n23 ?n26)) -(let (?n28 (ite $n27 ?n6 ?n7)) -(let (?n29 (zero_extend[15] ?n28)) -(flet ($n30 (= ?n22 ?n29)) -(flet ($n31 (if_then_else $n20 $n21 $n30)) -(flet ($n32 (if_then_else $n11 $n12 $n31)) -$n32 -))))))))))))))))))))))))))))))))) |