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/fuzz27.smt | |
parent | 022a5e927ecab4f217b3f26529b09e569bd35d94 (diff) |
failing bv examples
Diffstat (limited to 'test/regress/regress0/bv/fuzz27.smt')
-rw-r--r-- | test/regress/regress0/bv/fuzz27.smt | 143 |
1 files changed, 143 insertions, 0 deletions
diff --git a/test/regress/regress0/bv/fuzz27.smt b/test/regress/regress0/bv/fuzz27.smt new file mode 100644 index 000000000..c26632ebc --- /dev/null +++ b/test/regress/regress0/bv/fuzz27.smt @@ -0,0 +1,143 @@ +(benchmark fuzzsmt +:logic QF_BV +:status unknown +:extrafuns ((v0 BitVec[4])) +:extrafuns ((v1 BitVec[4])) +:extrafuns ((v2 BitVec[4])) +:extrafuns ((v3 BitVec[4])) +:formula +(let (?e4 bv8[4]) +(let (?e5 bv9[4]) +(let (?e6 bv11[4]) +(let (?e7 (ite (bvslt ?e6 ?e5) bv1[1] bv0[1])) +(let (?e8 (bvor (sign_extend[3] ?e7) ?e4)) +(let (?e9 (ite (bvslt v0 ?e6) bv1[1] bv0[1])) +(let (?e10 (bvxnor ?e8 ?e5)) +(let (?e11 (zero_extend[0] v3)) +(let (?e12 (bvxnor (sign_extend[3] ?e7) ?e6)) +(let (?e13 (bvnot v3)) +(let (?e14 (ite (bvugt ?e12 v3) bv1[1] bv0[1])) +(let (?e15 (bvcomp ?e10 ?e12)) +(let (?e16 (bvxnor v3 ?e6)) +(let (?e17 (rotate_right[0] ?e9)) +(let (?e18 (bvneg ?e17)) +(let (?e19 (bvor (zero_extend[3] ?e7) ?e10)) +(let (?e20 (bvnot ?e17)) +(let (?e21 (ite (bvsle ?e4 ?e12) bv1[1] bv0[1])) +(let (?e22 (bvxnor ?e9 ?e15)) +(let (?e23 (bvadd v1 ?e19)) +(let (?e24 (bvashr ?e17 ?e22)) +(let (?e25 (bvnor (sign_extend[3] ?e15) ?e16)) +(let (?e26 (ite (bvule ?e11 ?e4) bv1[1] bv0[1])) +(let (?e27 (ite (bvsle ?e4 (sign_extend[3] ?e9)) bv1[1] bv0[1])) +(let (?e28 (ite (bvuge ?e23 v3) bv1[1] bv0[1])) +(let (?e29 (ite (bvsgt ?e11 (sign_extend[3] ?e7)) bv1[1] bv0[1])) +(let (?e30 (ite (= bv1[1] (extract[0:0] ?e29)) (sign_extend[3] ?e24) ?e6)) +(let (?e31 (ite (bvugt v1 ?e16) bv1[1] bv0[1])) +(let (?e32 (bvand v2 ?e23)) +(flet ($e33 (bvugt (sign_extend[3] ?e29) ?e11)) +(flet ($e34 (distinct ?e20 ?e18)) +(flet ($e35 (bvult ?e19 ?e30)) +(flet ($e36 (bvult ?e11 ?e25)) +(flet ($e37 (bvuge (zero_extend[3] ?e14) ?e4)) +(flet ($e38 (= ?e15 ?e17)) +(flet ($e39 (bvslt (sign_extend[3] ?e17) ?e16)) +(flet ($e40 (bvult (zero_extend[3] ?e24) ?e30)) +(flet ($e41 (distinct ?e13 ?e12)) +(flet ($e42 (bvslt ?e16 ?e11)) +(flet ($e43 (bvsle ?e12 (sign_extend[3] ?e22))) +(flet ($e44 (bvuge ?e15 ?e26)) +(flet ($e45 (bvsgt ?e19 (zero_extend[3] ?e18))) +(flet ($e46 (bvslt ?e30 ?e23)) +(flet ($e47 (bvsgt ?e32 ?e8)) +(flet ($e48 (bvule ?e10 (sign_extend[3] ?e31))) +(flet ($e49 (bvslt (sign_extend[3] ?e15) v0)) +(flet ($e50 (bvsgt (sign_extend[3] ?e14) v1)) +(flet ($e51 (bvslt v3 ?e23)) +(flet ($e52 (distinct ?e6 (sign_extend[3] ?e20))) +(flet ($e53 (bvugt v2 ?e32)) +(flet ($e54 (bvsge ?e18 ?e15)) +(flet ($e55 (bvsgt ?e32 (sign_extend[3] ?e20))) +(flet ($e56 (bvuge ?e21 ?e21)) +(flet ($e57 (bvule ?e22 ?e14)) +(flet ($e58 (= ?e28 ?e17)) +(flet ($e59 (bvslt (sign_extend[3] ?e27) ?e19)) +(flet ($e60 (bvult ?e24 ?e20)) +(flet ($e61 (bvugt ?e5 (sign_extend[3] ?e20))) +(flet ($e62 (bvsle ?e26 ?e28)) +(flet ($e63 (bvule ?e31 ?e26)) +(flet ($e64 (bvuge ?e21 ?e18)) +(flet ($e65 (bvuge (sign_extend[3] ?e24) ?e13)) +(flet ($e66 (bvsge ?e23 ?e16)) +(flet ($e67 (bvugt (zero_extend[3] ?e17) ?e12)) +(flet ($e68 (bvsgt ?e30 v1)) +(flet ($e69 (bvule ?e16 ?e30)) +(flet ($e70 (bvult ?e22 ?e17)) +(flet ($e71 (bvult v1 ?e19)) +(flet ($e72 (bvuge ?e24 ?e28)) +(flet ($e73 (bvsge ?e11 (sign_extend[3] ?e22))) +(flet ($e74 (bvsgt ?e7 ?e18)) +(flet ($e75 (distinct ?e32 ?e16)) +(flet ($e76 (bvsge v3 ?e16)) +(flet ($e77 (bvsle (sign_extend[3] ?e15) v1)) +(flet ($e78 (bvule ?e8 ?e23)) +(flet ($e79 (bvsge ?e30 (sign_extend[3] ?e14))) +(flet ($e80 (bvsge ?e4 (zero_extend[3] ?e18))) +(flet ($e81 (bvslt v1 ?e4)) +(flet ($e82 (bvslt ?e5 v3)) +(flet ($e83 (distinct ?e29 ?e7)) +(flet ($e84 (bvult v1 ?e32)) +(flet ($e85 (bvslt (zero_extend[3] ?e27) ?e5)) +(flet ($e86 (bvslt v0 (zero_extend[3] ?e17))) +(flet ($e87 (bvsge (sign_extend[3] ?e24) ?e8)) +(flet ($e88 (bvslt ?e16 ?e12)) +(flet ($e89 (bvsge ?e29 ?e18)) +(flet ($e90 (bvsge v1 (sign_extend[3] ?e26))) +(flet ($e91 (bvsle (sign_extend[3] ?e26) ?e25)) +(flet ($e92 (bvsgt v0 ?e32)) +(flet ($e93 (bvult ?e17 ?e17)) +(flet ($e94 (distinct v0 ?e11)) +(flet ($e95 (bvsgt ?e4 ?e5)) +(flet ($e96 (bvsge ?e7 ?e18)) +(flet ($e97 (distinct ?e16 ?e32)) +(flet ($e98 (bvslt v3 (sign_extend[3] ?e22))) +(flet ($e99 (bvsge ?e28 ?e9)) +(flet ($e100 +(and + (or $e96 $e47 $e61) + (or (not $e97) (not $e88) (not $e40)) + (or $e40 (not $e45) $e61) + (or (not $e86) (not $e95) $e82) + (or $e65 $e59 (not $e50)) + (or $e35 (not $e70) (not $e83)) + (or $e40 $e98 (not $e96)) + (or $e84 (not $e87) (not $e95)) + (or (not $e58) $e98 $e41) + (or (not $e64) (not $e46) $e85) + (or $e43 (not $e60) $e89) + (or $e55 (not $e38) (not $e34)) + (or $e35 $e58 (not $e39)) + (or $e87 (not $e47) $e68) + (or $e52 (not $e79) $e35) + (or (not $e67) $e65 $e43) + (or $e60 (not $e71) (not $e84)) + (or (not $e46) $e63 (not $e67)) + (or $e57 $e41 $e88) + (or (not $e60) $e52 $e50) + (or (not $e57) $e88 (not $e99)) + (or $e69 $e45 $e35) + (or (not $e38) (not $e48) $e77) + (or (not $e38) $e60 $e69) + (or (not $e94) (not $e77) $e68) + (or (not $e76) (not $e68) $e97) + (or (not $e75) (not $e43) $e72) + (or (not $e54) $e42 (not $e61)) + (or (not $e89) $e42 $e44) + (or (not $e73) $e68 $e39) + (or $e82 $e69 (not $e89)) + (or (not $e38) (not $e67) $e55) + (or (not $e92) (not $e63) $e99) +)) +$e100 +)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) + |