summaryrefslogtreecommitdiff
path: root/test/regress/regress0/decision/error122.smt
diff options
context:
space:
mode:
Diffstat (limited to 'test/regress/regress0/decision/error122.smt')
-rw-r--r--test/regress/regress0/decision/error122.smt53
1 files changed, 0 insertions, 53 deletions
diff --git a/test/regress/regress0/decision/error122.smt b/test/regress/regress0/decision/error122.smt
deleted file mode 100644
index 2503ba01e..000000000
--- a/test/regress/regress0/decision/error122.smt
+++ /dev/null
@@ -1,53 +0,0 @@
-(benchmark fuzzsmt
-:logic QF_AUFBV
-:status unsat
-:extrafuns ((v0 BitVec[16]))
-:extrafuns ((a1 Array[16:4]))
-:extrafuns ((a2 Array[16:7]))
-:formula
-(let (?e3 bv8911[14])
-(let (?e4 (ite (bvsgt (zero_extend[2] ?e3) v0) bv1[1] bv0[1]))
-(let (?e5 (store a2 v0 (extract[13:7] v0)))
-(let (?e6 (store a2 (zero_extend[15] ?e4) (zero_extend[6] ?e4)))
-(let (?e7 (select ?e5 (zero_extend[2] ?e3)))
-(let (?e8 (store ?e5 (sign_extend[2] ?e3) (sign_extend[6] ?e4)))
-(let (?e9 (select a1 v0))
-(let (?e10 (store ?e8 (zero_extend[15] ?e4) (extract[6:0] v0)))
-(let (?e11 (bvadd (zero_extend[6] ?e4) ?e7))
-(let (?e12 (ite (bvult ?e11 ?e7) bv1[1] bv0[1]))
-(let (?e13 (ite (bvult (zero_extend[3] ?e12) ?e9) bv1[1] bv0[1]))
-(let (?e14 (bvlshr (sign_extend[12] ?e9) v0))
-(let (?e15 (ite (= bv1[1] (extract[12:12] ?e3)) ?e14 ?e14))
-(flet ($e16 (bvslt ?e15 v0))
-(flet ($e17 (bvult (sign_extend[15] ?e4) ?e14))
-(flet ($e18 (= (sign_extend[15] ?e12) ?e15))
-(flet ($e19 (distinct (sign_extend[15] ?e12) v0))
-(flet ($e20 (bvugt ?e11 ?e11))
-(flet ($e21 (bvule ?e13 ?e13))
-(flet ($e22 (bvslt ?e15 (sign_extend[9] ?e11)))
-(flet ($e23 (bvslt (zero_extend[9] ?e11) v0))
-(flet ($e24 (bvult v0 (sign_extend[15] ?e12)))
-(flet ($e25 (bvslt ?e7 (sign_extend[6] ?e4)))
-(flet ($e26 (bvule (zero_extend[12] ?e9) ?e15))
-(flet ($e27 (bvuge ?e13 ?e13))
-(flet ($e28 (distinct (zero_extend[6] ?e12) ?e7))
-(flet ($e29 (distinct ?e3 (sign_extend[13] ?e12)))
-(flet ($e30 (xor $e27 $e17))
-(flet ($e31 (or $e25 $e28))
-(flet ($e32 (iff $e31 $e21))
-(flet ($e33 (and $e18 $e22))
-(flet ($e34 (iff $e30 $e33))
-(flet ($e35 (and $e24 $e24))
-(flet ($e36 (and $e29 $e20))
-(flet ($e37 (and $e34 $e26))
-(flet ($e38 (iff $e36 $e16))
-(flet ($e39 (or $e38 $e32))
-(flet ($e40 (not $e19))
-(flet ($e41 (xor $e23 $e35))
-(flet ($e42 (and $e41 $e40))
-(flet ($e43 (implies $e42 $e37))
-(flet ($e44 (not $e43))
-(flet ($e45 (and $e39 $e44))
-$e45
-))))))))))))))))))))))))))))))))))))))))))))
-
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback