From: Dejan Jovanović <dejan.jovanovic@gmail.com>
Date: Wed, 13 Jun 2012 03:58:32 +0000 (+0000)
Subject: r2.node == response.node failure
X-Git-Tag: cvc5-1.0.0~8047
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=50d485074c372c94ca99b913d1a0bf22453b8c67;p=cvc5.git

r2.node == response.node failure
---

diff --git a/test/regress/regress0/bv/fuzz40.delta01.smt b/test/regress/regress0/bv/fuzz40.delta01.smt
new file mode 100644
index 000000000..3161c1675
--- /dev/null
+++ b/test/regress/regress0/bv/fuzz40.delta01.smt
@@ -0,0 +1,12 @@
+(benchmark fuzzsmt
+:logic QF_BV
+:extrafuns ((v0 BitVec[4]))
+:status sat
+:formula
+(let (?n1 bv1[4])
+(let (?n2 (bvmul ?n1 v0))
+(let (?n3 (extract[3:0] ?n2))
+(let (?n4 bv0[4])
+(flet ($n5 (bvsge ?n3 ?n4))
+$n5
+))))))
diff --git a/test/regress/regress0/bv/fuzz40.smt b/test/regress/regress0/bv/fuzz40.smt
new file mode 100644
index 000000000..30f6f5ab8
--- /dev/null
+++ b/test/regress/regress0/bv/fuzz40.smt
@@ -0,0 +1,85 @@
+(benchmark fuzzsmt
+:logic QF_BV
+:status unsat
+:extrafuns ((v0 BitVec[4]))
+:extrafuns ((v1 BitVec[10]))
+:extrafuns ((v2 BitVec[15]))
+:formula
+(let (?e3 bv1[3])
+(let (?e4 (ite (bvsgt (sign_extend[7] ?e3) v1) bv1[1] bv0[1]))
+(let (?e5 (bvmul (zero_extend[1] ?e3) v0))
+(let (?e6 (extract[3:0] ?e5))
+(let (?e7 (bvneg ?e3))
+(let (?e8 (bvudiv (zero_extend[6] v0) v1))
+(let (?e9 (extract[9:4] v1))
+(let (?e10 (bvor ?e8 (zero_extend[9] ?e4)))
+(let (?e11 (rotate_right[0] ?e4))
+(let (?e12 (bvxor ?e10 (zero_extend[7] ?e7)))
+(let (?e13 (bvneg ?e11))
+(let (?e14 (ite (bvsle (sign_extend[7] ?e7) v1) bv1[1] bv0[1]))
+(let (?e15 (bvand (zero_extend[11] ?e6) v2))
+(flet ($e16 (bvsgt ?e8 (zero_extend[6] v0)))
+(flet ($e17 (bvuge (zero_extend[12] ?e7) v2))
+(flet ($e18 (= v2 (sign_extend[14] ?e13)))
+(flet ($e19 (bvule (sign_extend[14] ?e13) ?e15))
+(flet ($e20 (bvule (sign_extend[6] ?e6) ?e12))
+(flet ($e21 (bvugt (sign_extend[9] ?e9) v2))
+(flet ($e22 (bvslt (sign_extend[6] ?e6) ?e8))
+(flet ($e23 (bvult v2 (zero_extend[11] v0)))
+(flet ($e24 (bvsgt ?e8 (sign_extend[9] ?e13)))
+(flet ($e25 (bvsgt (zero_extend[4] ?e9) ?e12))
+(flet ($e26 (bvugt (zero_extend[12] ?e7) ?e15))
+(flet ($e27 (bvslt v2 (zero_extend[14] ?e11)))
+(flet ($e28 (bvult (sign_extend[5] ?e13) ?e9))
+(flet ($e29 (= ?e8 (sign_extend[9] ?e11)))
+(flet ($e30 (bvult ?e15 ?e15))
+(flet ($e31 (bvult ?e15 (zero_extend[14] ?e4)))
+(flet ($e32 (bvsge (zero_extend[7] ?e7) v1))
+(flet ($e33 (bvuge (sign_extend[2] ?e6) ?e9))
+(flet ($e34 (bvslt (zero_extend[2] ?e14) ?e7))
+(flet ($e35 (bvsge ?e6 (zero_extend[3] ?e4)))
+(flet ($e36 (bvsgt ?e10 v1))
+(flet ($e37 (bvult ?e10 ?e10))
+(flet ($e38 (bvslt v2 (sign_extend[14] ?e11)))
+(flet ($e39 (bvule v0 (zero_extend[3] ?e14)))
+(flet ($e40 (bvult (sign_extend[9] ?e13) ?e10))
+(flet ($e41 (bvsgt v1 (sign_extend[7] ?e3)))
+(flet ($e42 (bvule ?e9 (sign_extend[2] ?e5)))
+(flet ($e43 (and $e17 $e39))
+(flet ($e44 (not $e43))
+(flet ($e45 (or $e23 $e44))
+(flet ($e46 (xor $e16 $e25))
+(flet ($e47 (if_then_else $e29 $e22 $e45))
+(flet ($e48 (if_then_else $e19 $e37 $e18))
+(flet ($e49 (implies $e46 $e35))
+(flet ($e50 (iff $e48 $e48))
+(flet ($e51 (iff $e28 $e24))
+(flet ($e52 (xor $e20 $e51))
+(flet ($e53 (xor $e47 $e42))
+(flet ($e54 (and $e32 $e41))
+(flet ($e55 (iff $e31 $e21))
+(flet ($e56 (and $e54 $e36))
+(flet ($e57 (and $e56 $e40))
+(flet ($e58 (xor $e57 $e34))
+(flet ($e59 (not $e58))
+(flet ($e60 (xor $e55 $e53))
+(flet ($e61 (not $e52))
+(flet ($e62 (and $e38 $e33))
+(flet ($e63 (implies $e50 $e49))
+(flet ($e64 (and $e59 $e61))
+(flet ($e65 (or $e26 $e60))
+(flet ($e66 (if_then_else $e62 $e65 $e64))
+(flet ($e67 (not $e30))
+(flet ($e68 (implies $e63 $e66))
+(flet ($e69 (xor $e27 $e68))
+(flet ($e70 (not $e67))
+(flet ($e71 (iff $e70 $e70))
+(flet ($e72 (xor $e71 $e71))
+(flet ($e73 (or $e72 $e72))
+(flet ($e74 (and $e69 $e69))
+(flet ($e75 (xor $e73 $e73))
+(flet ($e76 (and $e74 $e75))
+(flet ($e77 (and $e76 (not (= v1 bv0[10]))))
+$e77
+))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
+