diff options
Diffstat (limited to 'test/regress/regress0/aufbv/fuzz07.smt')
-rw-r--r-- | test/regress/regress0/aufbv/fuzz07.smt | 143 |
1 files changed, 143 insertions, 0 deletions
diff --git a/test/regress/regress0/aufbv/fuzz07.smt b/test/regress/regress0/aufbv/fuzz07.smt new file mode 100644 index 000000000..e57d45e7f --- /dev/null +++ b/test/regress/regress0/aufbv/fuzz07.smt @@ -0,0 +1,143 @@ +(benchmark fuzzsmt +:logic QF_AUFBV +:status sat +:extrafuns ((v0 BitVec[6])) +:extrafuns ((v1 BitVec[16])) +:extrafuns ((v2 BitVec[1])) +:extrafuns ((a3 Array[1:16])) +:extrafuns ((a4 Array[16:1])) +:formula +(let (?e5 bv6[4]) +(let (?e6 (ite (bvult v0 (sign_extend[5] v2)) bv1[1] bv0[1])) +(let (?e7 (sign_extend[0] v1)) +(let (?e8 (ite (bvslt ?e5 (zero_extend[3] ?e6)) bv1[1] bv0[1])) +(let (?e9 (store a4 (sign_extend[15] ?e6) ?e8)) +(let (?e10 (select ?e9 (zero_extend[15] ?e6))) +(let (?e11 (select a3 (extract[4:4] v0))) +(let (?e12 (select a3 (extract[0:0] ?e5))) +(let (?e13 (store ?e9 (sign_extend[15] ?e6) (extract[4:4] v1))) +(let (?e14 (select ?e13 ?e11)) +(let (?e15 (select ?e13 ?e12)) +(let (?e16 (bvadd (sign_extend[15] ?e15) v1)) +(let (?e17 (bvlshr ?e12 (sign_extend[12] ?e5))) +(let (?e18 (bvsdiv (zero_extend[15] ?e10) ?e11)) +(let (?e19 (bvlshr ?e14 ?e8)) +(let (?e20 (rotate_right[0] ?e6)) +(let (?e21 (ite (bvugt ?e7 (sign_extend[15] ?e15)) bv1[1] bv0[1])) +(let (?e22 (bvxnor (zero_extend[5] ?e15) v0)) +(let (?e23 (bvsdiv (sign_extend[15] v2) ?e18)) +(flet ($e24 (distinct (zero_extend[15] ?e8) ?e12)) +(flet ($e25 (bvult (sign_extend[5] ?e10) v0)) +(flet ($e26 (bvsle ?e12 ?e16)) +(flet ($e27 (bvsle (zero_extend[15] ?e19) ?e11)) +(flet ($e28 (bvult ?e17 ?e16)) +(flet ($e29 (bvsgt ?e14 ?e15)) +(flet ($e30 (bvsgt v0 (zero_extend[5] ?e14))) +(flet ($e31 (bvslt (zero_extend[15] ?e19) ?e7)) +(flet ($e32 (bvuge v1 ?e7)) +(flet ($e33 (bvsge ?e5 ?e5)) +(flet ($e34 (bvsge (sign_extend[15] ?e20) ?e7)) +(flet ($e35 (= (zero_extend[15] ?e14) v1)) +(flet ($e36 (bvugt ?e15 ?e10)) +(flet ($e37 (bvugt (zero_extend[15] ?e19) ?e18)) +(flet ($e38 (bvule ?e23 (sign_extend[15] ?e19))) +(flet ($e39 (bvsle (sign_extend[15] v2) ?e17)) +(flet ($e40 (bvsle ?e21 v2)) +(flet ($e41 (bvult ?e21 v2)) +(flet ($e42 (bvugt v0 (zero_extend[2] ?e5))) +(flet ($e43 (bvule ?e19 ?e15)) +(flet ($e44 (bvuge v0 (zero_extend[5] v2))) +(flet ($e45 (bvsle ?e8 v2)) +(flet ($e46 (bvsle ?e5 (zero_extend[3] ?e6))) +(flet ($e47 (bvuge ?e15 ?e6)) +(flet ($e48 (bvslt (sign_extend[10] v0) v1)) +(flet ($e49 (distinct ?e11 (sign_extend[10] v0))) +(flet ($e50 (distinct ?e11 ?e18)) +(flet ($e51 (bvugt (zero_extend[15] ?e15) ?e12)) +(flet ($e52 (bvuge ?e16 ?e23)) +(flet ($e53 (bvult ?e15 ?e15)) +(flet ($e54 (distinct ?e20 ?e20)) +(flet ($e55 (= v1 ?e7)) +(flet ($e56 (bvult (zero_extend[15] ?e21) ?e7)) +(flet ($e57 (distinct ?e12 ?e23)) +(flet ($e58 (bvult (zero_extend[5] ?e8) v0)) +(flet ($e59 (bvsle ?e8 ?e19)) +(flet ($e60 (= ?e10 ?e14)) +(flet ($e61 (bvult ?e6 ?e19)) +(flet ($e62 (bvsle ?e17 (zero_extend[15] ?e10))) +(flet ($e63 (bvugt ?e12 ?e18)) +(flet ($e64 (bvsgt ?e20 ?e10)) +(flet ($e65 (= ?e17 v1)) +(flet ($e66 (bvule ?e6 ?e19)) +(flet ($e67 (bvsle (sign_extend[15] ?e8) ?e12)) +(flet ($e68 (bvsle (sign_extend[15] ?e10) v1)) +(flet ($e69 (bvslt ?e23 (zero_extend[15] ?e10))) +(flet ($e70 (bvule ?e7 ?e12)) +(flet ($e71 (bvsle ?e7 (sign_extend[15] v2))) +(flet ($e72 (bvult ?e21 ?e10)) +(flet ($e73 (= v1 (zero_extend[10] v0))) +(flet ($e74 (bvsgt (zero_extend[3] ?e20) ?e5)) +(flet ($e75 (bvule ?e23 (zero_extend[10] ?e22))) +(flet ($e76 (xor $e41 $e34)) +(flet ($e77 (xor $e57 $e53)) +(flet ($e78 (xor $e43 $e46)) +(flet ($e79 (if_then_else $e59 $e49 $e77)) +(flet ($e80 (not $e42)) +(flet ($e81 (iff $e26 $e63)) +(flet ($e82 (xor $e45 $e79)) +(flet ($e83 (xor $e69 $e58)) +(flet ($e84 (xor $e29 $e51)) +(flet ($e85 (iff $e60 $e81)) +(flet ($e86 (or $e55 $e55)) +(flet ($e87 (if_then_else $e33 $e52 $e35)) +(flet ($e88 (if_then_else $e37 $e70 $e87)) +(flet ($e89 (not $e86)) +(flet ($e90 (or $e28 $e84)) +(flet ($e91 (and $e83 $e56)) +(flet ($e92 (and $e85 $e91)) +(flet ($e93 (and $e32 $e80)) +(flet ($e94 (or $e92 $e72)) +(flet ($e95 (and $e36 $e47)) +(flet ($e96 (implies $e40 $e89)) +(flet ($e97 (implies $e94 $e95)) +(flet ($e98 (iff $e71 $e61)) +(flet ($e99 (iff $e93 $e38)) +(flet ($e100 (implies $e27 $e30)) +(flet ($e101 (and $e97 $e96)) +(flet ($e102 (if_then_else $e50 $e99 $e99)) +(flet ($e103 (and $e65 $e48)) +(flet ($e104 (not $e44)) +(flet ($e105 (xor $e103 $e39)) +(flet ($e106 (if_then_else $e82 $e101 $e104)) +(flet ($e107 (or $e68 $e54)) +(flet ($e108 (or $e90 $e90)) +(flet ($e109 (or $e107 $e100)) +(flet ($e110 (xor $e67 $e88)) +(flet ($e111 (xor $e110 $e31)) +(flet ($e112 (or $e102 $e64)) +(flet ($e113 (not $e78)) +(flet ($e114 (if_then_else $e74 $e98 $e66)) +(flet ($e115 (iff $e108 $e109)) +(flet ($e116 (and $e25 $e73)) +(flet ($e117 (xor $e111 $e116)) +(flet ($e118 (xor $e115 $e106)) +(flet ($e119 (or $e112 $e24)) +(flet ($e120 (implies $e76 $e76)) +(flet ($e121 (xor $e113 $e62)) +(flet ($e122 (or $e120 $e120)) +(flet ($e123 (not $e75)) +(flet ($e124 (and $e122 $e118)) +(flet ($e125 (and $e119 $e123)) +(flet ($e126 (or $e105 $e105)) +(flet ($e127 (iff $e124 $e114)) +(flet ($e128 (or $e126 $e117)) +(flet ($e129 (xor $e125 $e121)) +(flet ($e130 (iff $e127 $e129)) +(flet ($e131 (or $e130 $e128)) +(flet ($e132 (and $e131 (not (= ?e11 bv0[16])))) +(flet ($e133 (and $e132 (not (= ?e11 (bvnot bv0[16]))))) +(flet ($e134 (and $e133 (not (= ?e18 bv0[16])))) +(flet ($e135 (and $e134 (not (= ?e18 (bvnot bv0[16]))))) +$e135 +)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) + |