diff options
author | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2012-06-11 13:54:42 +0000 |
---|---|---|
committer | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2012-06-11 13:54:42 +0000 |
commit | aabd0696722250f02e878943f534fd41c49ef5dd (patch) | |
tree | 0f14706b1c254aa8fd8fa9b888507ab9816a95d3 /test/regress/regress0/bv/fuzz29.smt | |
parent | 022a5e927ecab4f217b3f26529b09e569bd35d94 (diff) |
failing bv examples
Diffstat (limited to 'test/regress/regress0/bv/fuzz29.smt')
-rw-r--r-- | test/regress/regress0/bv/fuzz29.smt | 98 |
1 files changed, 98 insertions, 0 deletions
diff --git a/test/regress/regress0/bv/fuzz29.smt b/test/regress/regress0/bv/fuzz29.smt new file mode 100644 index 000000000..f1275af5c --- /dev/null +++ b/test/regress/regress0/bv/fuzz29.smt @@ -0,0 +1,98 @@ +(benchmark fuzzsmt +:logic QF_BV +:status unknown +:extrafuns ((v0 BitVec[4])) +:extrafuns ((v1 BitVec[4])) +:extrafuns ((v2 BitVec[4])) +:formula +(let (?e3 bv6[4]) +(let (?e4 bv1[4]) +(let (?e5 bv2[4]) +(let (?e6 (bvashr v0 v1)) +(let (?e7 (bvor v1 ?e6)) +(let (?e8 (ite (bvsge v0 v1) bv1[1] bv0[1])) +(let (?e9 (bvxnor ?e6 ?e7)) +(let (?e10 (ite (bvsgt ?e7 ?e7) bv1[1] bv0[1])) +(let (?e11 (ite (bvsge (sign_extend[3] ?e8) ?e5) bv1[1] bv0[1])) +(let (?e12 (bvxnor ?e5 ?e7)) +(let (?e13 (bvnand v1 ?e9)) +(let (?e14 (bvnor ?e5 ?e4)) +(let (?e15 (bvshl ?e7 (zero_extend[3] ?e11))) +(let (?e16 (repeat[1] ?e13)) +(let (?e17 (bvnor v2 ?e13)) +(let (?e18 (bvnot ?e12)) +(let (?e19 (ite (bvsgt v1 (sign_extend[3] ?e8)) bv1[1] bv0[1])) +(let (?e20 (bvcomp ?e5 ?e13)) +(let (?e21 (rotate_right[2] ?e16)) +(let (?e22 (extract[2:1] v1)) +(let (?e23 (bvashr ?e21 ?e3)) +(flet ($e24 (distinct v0 ?e17)) +(flet ($e25 (bvule ?e13 (sign_extend[3] ?e11))) +(flet ($e26 (bvsge v2 v1)) +(flet ($e27 (bvsge v0 v0)) +(flet ($e28 (bvslt ?e23 v2)) +(flet ($e29 (= ?e6 ?e5)) +(flet ($e30 (bvule ?e19 ?e10)) +(flet ($e31 (bvsle (zero_extend[2] ?e22) ?e17)) +(flet ($e32 (bvsgt ?e14 (sign_extend[3] ?e8))) +(flet ($e33 (bvsgt ?e13 v0)) +(flet ($e34 (bvuge v2 ?e23)) +(flet ($e35 (bvule ?e6 v2)) +(flet ($e36 (bvule ?e22 (sign_extend[1] ?e8))) +(flet ($e37 (bvuge (zero_extend[3] ?e10) ?e13)) +(flet ($e38 (= ?e5 (sign_extend[3] ?e19))) +(flet ($e39 (bvsle ?e16 (sign_extend[3] ?e10))) +(flet ($e40 (bvuge ?e14 ?e18)) +(flet ($e41 (bvugt ?e19 ?e10)) +(flet ($e42 (bvsle (sign_extend[3] ?e11) ?e21)) +(flet ($e43 (bvsge ?e18 ?e13)) +(flet ($e44 (distinct ?e16 ?e15)) +(flet ($e45 (bvult ?e4 ?e6)) +(flet ($e46 (bvule ?e15 ?e5)) +(flet ($e47 (bvugt ?e22 ?e22)) +(flet ($e48 (bvsge (zero_extend[3] ?e20) ?e23)) +(flet ($e49 (bvsle ?e12 ?e5)) +(flet ($e50 (bvsge (zero_extend[2] ?e22) ?e15)) +(flet ($e51 (bvsgt v0 ?e15)) +(flet ($e52 (bvuge ?e6 v1)) +(flet ($e53 (bvsgt ?e7 ?e15)) +(flet ($e54 (bvsge ?e15 (zero_extend[3] ?e19))) +(flet ($e55 (bvult ?e23 v1)) +(flet ($e56 (bvsge ?e23 ?e6)) +(flet ($e57 (distinct ?e12 (sign_extend[3] ?e11))) +(flet ($e58 (bvuge v0 ?e6)) +(flet ($e59 (bvsge (zero_extend[3] ?e11) ?e12)) +(flet ($e60 (bvule ?e17 ?e7)) +(flet ($e61 (bvult (sign_extend[3] ?e8) ?e3)) +(flet ($e62 (= ?e14 (sign_extend[3] ?e11))) +(flet ($e63 (bvuge ?e23 (zero_extend[3] ?e20))) +(flet ($e64 (bvslt ?e7 v2)) +(flet ($e65 (bvsge (zero_extend[3] ?e10) v0)) +(flet ($e66 (bvsge (sign_extend[3] ?e8) ?e9)) +(flet ($e67 +(and + (or $e42 $e44 (not $e63)) + (or (not $e44) (not $e30) (not $e61)) + (or $e41 $e41 (not $e60)) + (or (not $e46) $e29 (not $e65)) + (or $e65 $e46 (not $e44)) + (or $e52 $e59 $e41) + (or $e36 $e50 $e33) + (or (not $e26) $e33 $e26) + (or (not $e65) $e50 (not $e52)) + (or $e57 (not $e36) (not $e60)) + (or $e47 $e27 (not $e50)) + (or (not $e25) (not $e64) $e24) + (or (not $e52) $e34 (not $e58)) + (or (not $e63) (not $e56) $e28) + (or (not $e51) (not $e60) $e59) + (or $e52 (not $e54) $e24) + (or (not $e36) $e47 (not $e57)) + (or (not $e66) $e36 $e65) + (or (not $e46) (not $e61) $e51) + (or $e24 (not $e24) $e53) + (or (not $e58) $e56 $e31) +)) +$e67 +)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) + |