diff options
Diffstat (limited to 'test/regress/regress0/decision/error20.smt')
-rw-r--r-- | test/regress/regress0/decision/error20.smt | 66 |
1 files changed, 0 insertions, 66 deletions
diff --git a/test/regress/regress0/decision/error20.smt b/test/regress/regress0/decision/error20.smt deleted file mode 100644 index adc638500..000000000 --- a/test/regress/regress0/decision/error20.smt +++ /dev/null @@ -1,66 +0,0 @@ -(benchmark fuzzsmt -:logic QF_AUFBV -:status sat -:extrafuns ((v0 BitVec[16])) -:extrafuns ((v1 BitVec[1])) -:extrafuns ((a2 Array[12:10])) -:extrafuns ((a3 Array[14:11])) -:extrafuns ((a4 Array[1:7])) -:formula -(let (?e5 bv1[1]) -(let (?e6 (ite (= bv1[1] (extract[0:0] v1)) (sign_extend[15] ?e5) v0)) -(let (?e7 (store a4 (extract[4:4] v0) (extract[9:3] v0))) -(let (?e8 (store ?e7 ?e5 (extract[12:6] v0))) -(let (?e9 (store ?e8 v1 (sign_extend[6] ?e5))) -(let (?e10 (select a4 v1)) -(let (?e11 (store ?e8 ?e5 (zero_extend[6] v1))) -(let (?e12 (select ?e8 v1)) -(let (?e13 (store a2 (extract[14:3] v0) (zero_extend[3] ?e10))) -(let (?e14 (rotate_right[0] v1)) -(let (?e15 (rotate_right[3] ?e10)) -(let (?e16 (ite (bvsge ?e12 (zero_extend[6] v1)) bv1[1] bv0[1])) -(let (?e17 (repeat[5] ?e14)) -(let (?e18 (bvsdiv (sign_extend[9] ?e15) ?e6)) -(let (?e19 (bvmul (zero_extend[15] ?e5) v0)) -(flet ($e20 (= (zero_extend[15] ?e5) ?e18)) -(flet ($e21 (bvugt (zero_extend[9] ?e10) ?e19)) -(flet ($e22 (bvsgt ?e15 (zero_extend[6] v1))) -(flet ($e23 (bvslt ?e14 ?e16)) -(flet ($e24 (bvugt ?e19 (zero_extend[15] v1))) -(flet ($e25 (distinct ?e12 ?e12)) -(flet ($e26 (bvule ?e17 (sign_extend[4] ?e5))) -(flet ($e27 (bvsle ?e18 (zero_extend[15] ?e16))) -(flet ($e28 (bvsle ?e10 ?e15)) -(flet ($e29 (bvsgt ?e12 (zero_extend[6] ?e16))) -(flet ($e30 (bvsgt (sign_extend[4] ?e5) ?e17)) -(flet ($e31 (bvsle ?e17 (zero_extend[4] ?e14))) -(flet ($e32 (bvult (zero_extend[11] ?e17) ?e6)) -(flet ($e33 (bvult ?e5 ?e5)) -(flet ($e34 (bvugt ?e12 (sign_extend[2] ?e17))) -(flet ($e35 (bvsle (sign_extend[6] v1) ?e15)) -(flet ($e36 (bvule ?e15 (zero_extend[6] ?e14))) -(flet ($e37 (bvsgt v0 ?e6)) -(flet ($e38 (if_then_else $e23 $e25 $e26)) -(flet ($e39 (iff $e33 $e35)) -(flet ($e40 (or $e21 $e36)) -(flet ($e41 (or $e20 $e32)) -(flet ($e42 (and $e22 $e39)) -(flet ($e43 (not $e41)) -(flet ($e44 (implies $e24 $e31)) -(flet ($e45 (or $e42 $e44)) -(flet ($e46 (iff $e27 $e37)) -(flet ($e47 (or $e29 $e46)) -(flet ($e48 (not $e28)) -(flet ($e49 (and $e47 $e43)) -(flet ($e50 (iff $e40 $e30)) -(flet ($e51 (xor $e34 $e50)) -(flet ($e52 (iff $e45 $e51)) -(flet ($e53 (if_then_else $e49 $e49 $e52)) -(flet ($e54 (or $e53 $e38)) -(flet ($e55 (iff $e54 $e54)) -(flet ($e56 (and $e48 $e55)) -(flet ($e57 (and $e56 (not (= ?e6 bv0[16])))) -(flet ($e58 (and $e57 (not (= ?e6 (bvnot bv0[16]))))) -$e58 -))))))))))))))))))))))))))))))))))))))))))))))))))))))) - |