r2.node == response.node failure

diff --git a/test/regress/regress0/aufbv/fuzz05.delta01.smt b/test/regress/regress0/aufbv/fuzz05.delta01.smt
new file mode 100644 (file)
index 0000000..b2dfdce
--- /dev/null
+++ b/test/regress/regress0/aufbv/fuzz05.delta01.smt
@@ -0,0 +1,14 @@
+(benchmark fuzzsmt
+:logic QF_AUFBV
+:extrafuns ((a2 Array[12:9]))
+:status sast
+:formula
+(let (?n1 bv0[13])
+(let (?n2 (bvsdiv ?n1 ?n1))
+(let (?n3 bv0[12])
+(let (?n4 (select a2 ?n3))
+(let (?n5 (sign_extend[4] ?n4))
+(let (?n6 (bvmul ?n2 ?n5))
+(flet ($n7 (bvsge ?n1 ?n6))
+$n7
+))))))))

diff --git a/test/regress/regress0/aufbv/fuzz05.smt b/test/regress/regress0/aufbv/fuzz05.smt
new file mode 100644 (file)
index 0000000..b838f5f
--- /dev/null
+++ b/test/regress/regress0/aufbv/fuzz05.smt
@@ -0,0 +1,78 @@
+(benchmark fuzzsmt
+:logic QF_AUFBV
+:status sat
+:extrafuns ((v0 BitVec[13]))
+:extrafuns ((a1 Array[5:5]))
+:extrafuns ((a2 Array[12:9]))
+:extrafuns ((a3 Array[8:7]))
+:formula
+(let (?e4 bv6[4])
+(let (?e5 (bvsdiv v0 v0))
+(let (?e6 (bvurem ?e4 ?e4))
+(let (?e7 (store a3 (extract[10:3] v0) (sign_extend[3] ?e6)))
+(let (?e8 (store a2 (extract[11:0] v0) (zero_extend[5] ?e4)))
+(let (?e9 (store a3 (sign_extend[4] ?e4) (zero_extend[3] ?e6)))
+(let (?e10 (select ?e8 (sign_extend[8] ?e6)))
+(let (?e11 (select a1 (extract[6:2] v0)))
+(let (?e12 (select a2 (extract[11:0] ?e5)))
+(let (?e13 (store a1 (extract[8:4] ?e10) (zero_extend[1] ?e6)))
+(let (?e14 (select a2 (sign_extend[8] ?e6)))
+(let (?e15 (store ?e8 (zero_extend[3] ?e10) ?e14))
+(let (?e16 (select a2 (extract[12:1] v0)))
+(let (?e17 (bvmul (sign_extend[4] ?e16) ?e5))
+(let (?e18 (bvadd ?e10 (zero_extend[5] ?e6)))
+(let (?e19 (ite (bvuge ?e16 (sign_extend[4] ?e11)) bv1[1] bv0[1]))
+(let (?e20 (bvnor ?e4 ?e4))
+(let (?e21 (bvcomp v0 (zero_extend[9] ?e4)))
+(let (?e22 (bvnand ?e6 ?e6))
+(let (?e23 (ite (bvsge (zero_extend[4] ?e14) ?e17) bv1[1] bv0[1]))
+(let (?e24 (rotate_left[1] ?e20))
+(let (?e25 (ite (bvuge ?e12 (zero_extend[8] ?e21)) bv1[1] bv0[1]))
+(flet ($e26 (= ?e18 (zero_extend[8] ?e19)))
+(flet ($e27 (bvsge (sign_extend[8] ?e25) ?e10))
+(flet ($e28 (= (zero_extend[4] ?e14) v0))
+(flet ($e29 (bvuge ?e16 ?e18))
+(flet ($e30 (bvult (sign_extend[5] ?e20) ?e16))
+(flet ($e31 (bvslt (zero_extend[4] ?e11) ?e14))
+(flet ($e32 (bvult ?e12 (sign_extend[5] ?e4)))
+(flet ($e33 (bvult ?e12 (sign_extend[5] ?e22)))
+(flet ($e34 (bvsge ?e10 (zero_extend[8] ?e23)))
+(flet ($e35 (bvult (sign_extend[5] ?e6) ?e14))
+(flet ($e36 (bvult (zero_extend[3] ?e19) ?e20))
+(flet ($e37 (= ?e11 (sign_extend[1] ?e6)))
+(flet ($e38 (bvsle (zero_extend[9] ?e24) ?e5))
+(flet ($e39 (bvule ?e5 (sign_extend[4] ?e12)))
+(flet ($e40 (bvugt (zero_extend[1] ?e4) ?e11))
+(flet ($e41 (bvsgt ?e12 (sign_extend[8] ?e23)))
+(flet ($e42 (bvsge ?e6 (sign_extend[3] ?e25)))
+(flet ($e43 (bvsge ?e17 (zero_extend[4] ?e14)))
+(flet ($e44 (bvuge (zero_extend[9] ?e6) v0))
+(flet ($e45 (bvsgt (sign_extend[8] ?e21) ?e14))
+(flet ($e46 (xor $e27 $e36))
+(flet ($e47 (xor $e45 $e33))
+(flet ($e48 (if_then_else $e40 $e39 $e42))
+(flet ($e49 (xor $e31 $e32))
+(flet ($e50 (and $e47 $e28))
+(flet ($e51 (xor $e34 $e29))
+(flet ($e52 (not $e48))
+(flet ($e53 (not $e50))
+(flet ($e54 (if_then_else $e43 $e44 $e41))
+(flet ($e55 (and $e37 $e26))
+(flet ($e56 (not $e38))
+(flet ($e57 (implies $e52 $e56))
+(flet ($e58 (xor $e55 $e35))
+(flet ($e59 (and $e53 $e49))
+(flet ($e60 (if_then_else $e54 $e58 $e54))
+(flet ($e61 (if_then_else $e60 $e59 $e59))
+(flet ($e62 (iff $e46 $e57))
+(flet ($e63 (and $e62 $e61))
+(flet ($e64 (or $e63 $e63))
+(flet ($e65 (and $e30 $e51))
+(flet ($e66 (not $e65))
+(flet ($e67 (xor $e64 $e66))
+(flet ($e68 (and $e67 (not (= v0 bv0[13]))))
+(flet ($e69 (and $e68 (not (= v0 (bvnot bv0[13])))))
+(flet ($e70 (and $e69 (not (= ?e4 bv0[4]))))
+$e70
+))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
+