diff options
Diffstat (limited to 'test/regress/regress0/aufbv')
-rw-r--r-- | test/regress/regress0/aufbv/Makefile.am | 1 | ||||
-rw-r--r-- | test/regress/regress0/aufbv/fuzz13.smt | 90 |
2 files changed, 91 insertions, 0 deletions
diff --git a/test/regress/regress0/aufbv/Makefile.am b/test/regress/regress0/aufbv/Makefile.am index 1a698b180..c67ce5b00 100644 --- a/test/regress/regress0/aufbv/Makefile.am +++ b/test/regress/regress0/aufbv/Makefile.am @@ -44,6 +44,7 @@ TESTS = \ fuzz10.smt \ fuzz11.smt \ fuzz12.smt \ + fuzz13.smt \ fifo32bc06k08.delta01.smt \ rewrite_bug.smt \ array_rewrite_bug.smt diff --git a/test/regress/regress0/aufbv/fuzz13.smt b/test/regress/regress0/aufbv/fuzz13.smt new file mode 100644 index 000000000..d8c0b8480 --- /dev/null +++ b/test/regress/regress0/aufbv/fuzz13.smt @@ -0,0 +1,90 @@ +(benchmark fuzzsmt +:logic QF_AUFBV +:status sat +:extrafuns ((v0 BitVec[9])) +:extrafuns ((v1 BitVec[14])) +:extrafuns ((a2 Array[2:5])) +:extrafuns ((a3 Array[8:5])) +:formula +(let (?e4 bv712[10]) +(let (?e5 (ite (bvslt ?e4 ?e4) bv1[1] bv0[1])) +(let (?e6 (ite (= bv1[1] (extract[2:2] v1)) (sign_extend[5] v0) v1)) +(let (?e7 (store a2 (sign_extend[1] ?e5) (extract[12:8] ?e6))) +(let (?e8 (store ?e7 (zero_extend[1] ?e5) (extract[6:2] v1))) +(let (?e9 (select ?e8 (extract[12:11] v1))) +(let (?e10 (select a2 (extract[2:1] ?e4))) +(let (?e11 (store ?e8 (zero_extend[1] ?e5) ?e10)) +(let (?e12 (select ?e11 (extract[1:0] ?e10))) +(let (?e13 (select a2 (extract[3:2] ?e9))) +(let (?e14 (ite (bvsge (zero_extend[4] ?e10) v0) bv1[1] bv0[1])) +(let (?e15 (bvnand ?e4 (zero_extend[5] ?e13))) +(let (?e16 (ite (bvule ?e12 ?e12) bv1[1] bv0[1])) +(let (?e17 (extract[0:0] ?e5)) +(let (?e18 (zero_extend[0] ?e6)) +(let (?e19 (bvsdiv (zero_extend[9] ?e12) v1)) +(let (?e20 (bvsdiv (zero_extend[9] ?e9) ?e6)) +(flet ($e21 (bvugt v1 (zero_extend[9] ?e12))) +(flet ($e22 (bvuge ?e9 (sign_extend[4] ?e14))) +(flet ($e23 (bvslt ?e6 (sign_extend[9] ?e10))) +(flet ($e24 (bvugt ?e19 v1)) +(flet ($e25 (bvult (sign_extend[4] ?e12) v0)) +(flet ($e26 (= (sign_extend[4] ?e15) v1)) +(flet ($e27 (= ?e19 (sign_extend[9] ?e12))) +(flet ($e28 (bvsge (zero_extend[9] ?e9) ?e6)) +(flet ($e29 (bvuge ?e13 (zero_extend[4] ?e5))) +(flet ($e30 (distinct (zero_extend[4] ?e14) ?e9)) +(flet ($e31 (bvsle (zero_extend[4] ?e14) ?e12)) +(flet ($e32 (bvslt ?e10 ?e12)) +(flet ($e33 (distinct ?e6 ?e18)) +(flet ($e34 (bvsge (sign_extend[4] ?e12) v0)) +(flet ($e35 (bvsge ?e6 (zero_extend[5] v0))) +(flet ($e36 (distinct v0 (sign_extend[4] ?e13))) +(flet ($e37 (= ?e18 (sign_extend[5] v0))) +(flet ($e38 (bvugt ?e16 ?e5)) +(flet ($e39 (bvslt ?e9 (sign_extend[4] ?e16))) +(flet ($e40 (distinct (zero_extend[9] ?e13) ?e19)) +(flet ($e41 (bvsle ?e19 (zero_extend[13] ?e5))) +(flet ($e42 (bvslt (zero_extend[4] ?e12) v0)) +(flet ($e43 (bvugt ?e14 ?e17)) +(flet ($e44 (bvsle (sign_extend[4] ?e14) ?e13)) +(flet ($e45 (bvugt (zero_extend[4] ?e14) ?e12)) +(flet ($e46 (bvsge ?e19 ?e6)) +(flet ($e47 (bvsle ?e10 (zero_extend[4] ?e14))) +(flet ($e48 (bvsle ?e20 (zero_extend[4] ?e4))) +(flet ($e49 (and $e22 $e30)) +(flet ($e50 (or $e38 $e29)) +(flet ($e51 (xor $e41 $e34)) +(flet ($e52 (iff $e21 $e48)) +(flet ($e53 (iff $e46 $e23)) +(flet ($e54 (iff $e33 $e44)) +(flet ($e55 (and $e24 $e43)) +(flet ($e56 (implies $e32 $e31)) +(flet ($e57 (or $e56 $e47)) +(flet ($e58 (xor $e50 $e40)) +(flet ($e59 (or $e57 $e45)) +(flet ($e60 (iff $e42 $e59)) +(flet ($e61 (or $e35 $e36)) +(flet ($e62 (if_then_else $e51 $e60 $e25)) +(flet ($e63 (or $e55 $e54)) +(flet ($e64 (xor $e53 $e39)) +(flet ($e65 (and $e63 $e63)) +(flet ($e66 (or $e61 $e28)) +(flet ($e67 (and $e27 $e27)) +(flet ($e68 (or $e26 $e26)) +(flet ($e69 (or $e65 $e49)) +(flet ($e70 (xor $e58 $e62)) +(flet ($e71 (implies $e68 $e37)) +(flet ($e72 (if_then_else $e52 $e52 $e70)) +(flet ($e73 (implies $e66 $e67)) +(flet ($e74 (xor $e64 $e71)) +(flet ($e75 (and $e73 $e73)) +(flet ($e76 (implies $e72 $e69)) +(flet ($e77 (xor $e76 $e75)) +(flet ($e78 (iff $e77 $e74)) +(flet ($e79 (and $e78 (not (= v1 bv0[14])))) +(flet ($e80 (and $e79 (not (= v1 (bvnot bv0[14]))))) +(flet ($e81 (and $e80 (not (= ?e6 bv0[14])))) +(flet ($e82 (and $e81 (not (= ?e6 (bvnot bv0[14]))))) +$e82 +)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) + |