diff options
Diffstat (limited to 'test/regress/regress0/bv/fuzz12.smt')
-rw-r--r-- | test/regress/regress0/bv/fuzz12.smt | 57 |
1 files changed, 0 insertions, 57 deletions
diff --git a/test/regress/regress0/bv/fuzz12.smt b/test/regress/regress0/bv/fuzz12.smt deleted file mode 100644 index 017732c4d..000000000 --- a/test/regress/regress0/bv/fuzz12.smt +++ /dev/null @@ -1,57 +0,0 @@ -(benchmark fuzzsmt -:logic QF_BV -:extrafuns ((v1 BitVec[9])) -:extrafuns ((v2 BitVec[10])) -:extrafuns ((v0 BitVec[3])) -:status sat -:formula -(let (?n1 bv1[3]) -(flet ($n2 (= ?n1 v0)) -(let (?n3 bv0[9]) -(let (?n4 bv1[1]) -(let (?n5 (sign_extend[2] v2)) -(let (?n6 (extract[9:9] ?n5)) -(flet ($n7 (= ?n4 ?n6)) -(let (?n8 (bvneg v1)) -(let (?n9 bv1[11]) -(let (?n10 (zero_extend[8] v0)) -(flet ($n11 (bvsgt ?n9 ?n10)) -(let (?n12 bv0[1]) -(let (?n13 (ite $n11 ?n4 ?n12)) -(let (?n14 (zero_extend[8] ?n13)) -(let (?n15 (ite $n7 ?n8 ?n14)) -(flet ($n16 (= ?n3 ?n15)) -(let (?n17 bv1[12]) -(let (?n18 (zero_extend[3] v1)) -(flet ($n19 (bvult ?n17 ?n18)) -(let (?n20 (ite $n19 ?n4 ?n12)) -(let (?n21 (zero_extend[1] v1)) -(let (?n22 (bvlshr v2 ?n21)) -(let (?n23 (zero_extend[2] ?n22)) -(let (?n24 bv0[12]) -(flet ($n25 (= ?n23 ?n24)) -(let (?n26 (ite $n25 ?n4 ?n12)) -(flet ($n27 (= ?n20 ?n26)) -(flet ($n28 (or $n16 $n27)) -(let (?n29 (sign_extend[9] v0)) -(flet ($n30 (= ?n24 ?n29)) -(let (?n31 bv0[10]) -(let (?n32 (rotate_left[3] ?n8)) -(let (?n33 (zero_extend[1] ?n32)) -(let (?n34 (bvmul ?n22 ?n33)) -(let (?n35 (bvcomp ?n31 ?n34)) -(flet ($n36 (= ?n4 ?n35)) -(let (?n37 bv1[9]) -(let (?n38 (bvadd v1 ?n37)) -(let (?n39 (zero_extend[6] v0)) -(flet ($n40 (bvsge ?n38 ?n39)) -(let (?n41 (ite $n40 ?n4 ?n12)) -(let (?n42 (bvnor ?n41 ?n41)) -(flet ($n43 (= ?n4 ?n42)) -(let (?n44 (ite $n43 ?n31 ?n22)) -(flet ($n45 (= ?n31 ?n44)) -(flet ($n46 (if_then_else $n30 $n36 $n45)) -(flet ($n47 (xor $n28 $n46)) -(flet ($n48 (implies $n2 $n47)) -$n48 -))))))))))))))))))))))))))))))))))))))))))))))))) |