diff options
author | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2012-06-11 18:54:38 +0000 |
---|---|---|
committer | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2012-06-11 18:54:38 +0000 |
commit | d54c761087af01874ea6674111888cb94ffa4ee6 (patch) | |
tree | 2f196940df9b488a1298ccfdee9bf1b54a70ccac /test/regress/regress0/bv/fuzz16.delta01.smt | |
parent | e148b0a99917b21499b2f596aa22403559baf677 (diff) |
fixing bitvector bugs
* clauses shouldn't be erased when they could be a reason for outside propagation
* propagation of p and !p is ignored as this must lead to a conflict in the subtheory internally
Diffstat (limited to 'test/regress/regress0/bv/fuzz16.delta01.smt')
-rw-r--r-- | test/regress/regress0/bv/fuzz16.delta01.smt | 69 |
1 files changed, 69 insertions, 0 deletions
diff --git a/test/regress/regress0/bv/fuzz16.delta01.smt b/test/regress/regress0/bv/fuzz16.delta01.smt new file mode 100644 index 000000000..c9fef69de --- /dev/null +++ b/test/regress/regress0/bv/fuzz16.delta01.smt @@ -0,0 +1,69 @@ +(benchmark fuzzsmt +:logic QF_BV +:extrafuns ((v1 BitVec[12])) +:extrafuns ((v15 BitVec[8])) +:extrafuns ((v11 BitVec[12])) +:extrafuns ((v12 BitVec[15])) +:status unsat +:formula +(flet ($n1 true) +(let (?n2 bv0[12]) +(flet ($n3 (bvslt ?n2 v1)) +(flet ($n4 (not $n3)) +(let (?n5 bv0[1]) +(let (?n6 bv1[1]) +(let (?n7 bv1[12]) +(flet ($n8 (bvult v11 ?n7)) +(let (?n9 (ite $n8 ?n6 ?n5)) +(flet ($n10 (= ?n6 ?n9)) +(let (?n11 (ite $n10 v11 ?n2)) +(let (?n12 (sign_extend[3] ?n11)) +(flet ($n13 (bvult ?n12 v12)) +(let (?n14 (ite $n13 ?n6 ?n5)) +(flet ($n15 (bvult ?n5 ?n14)) +(flet ($n16 (not $n15)) +(let (?n17 bv0[5]) +(let (?n18 (sign_extend[1] v1)) +(let (?n19 (sign_extend[2] ?n18)) +(let (?n20 (bvxnor v12 ?n19)) +(flet ($n21 (bvult ?n19 ?n20)) +(let (?n22 (ite $n21 ?n6 ?n5)) +(let (?n23 (repeat[5] ?n22)) +(flet ($n24 (bvult ?n17 ?n23)) +(let (?n25 bv0[10]) +(let (?n26 bv0[15]) +(flet ($n27 (bvsge ?n20 ?n26)) +(let (?n28 (ite $n27 ?n6 ?n5)) +(let (?n29 (sign_extend[9] ?n28)) +(flet ($n30 (= ?n25 ?n29)) +(let (?n31 bv1[14]) +(flet ($n32 (bvult ?n22 ?n6)) +(let (?n33 (ite $n32 ?n6 ?n5)) +(let (?n34 (zero_extend[13] ?n33)) +(let (?n35 (bvadd ?n31 ?n34)) +(let (?n36 bv0[14]) +(flet ($n37 (bvugt ?n35 ?n36)) +(flet ($n38 false) +(let (?n39 bv1[15]) +(let (?n40 (zero_extend[4] v15)) +(let (?n41 (bvcomp v11 ?n40)) +(let (?n42 (zero_extend[14] ?n41)) +(flet ($n43 (distinct ?n39 ?n42)) +(let (?n44 (ite $n43 ?n6 ?n5)) +(let (?n45 (sign_extend[11] ?n44)) +(let (?n46 (bvxor v1 ?n45)) +(flet ($n47 (bvsgt ?n2 ?n46)) +(let (?n48 (zero_extend[12] ?n44)) +(let (?n49 bv0[13]) +(flet ($n50 (bvule ?n48 ?n49)) +(flet ($n51 (or $n38 $n47 $n50)) +(flet ($n52 (bvsle ?n2 v1)) +(let (?n53 (ite $n52 ?n6 ?n5)) +(let (?n54 (bvadd ?n6 ?n53)) +(flet ($n55 (bvugt ?n54 ?n5)) +(let (?n56 (ite $n55 ?n6 ?n5)) +(let (?n57 (sign_extend[14] ?n56)) +(flet ($n58 (bvuge ?n57 ?n39)) +(flet ($n59 (and $n4 $n16 $n24 $n30 $n37 $n51 $n58)) +$n59 +)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) |