Merge branch 'master' into splitEqRew

1 files changed, 7 insertions, 0 deletions

diff --git a/test/regress/regress0/aufbv/fuzz00.smtv1.smt2 b/test/regress/regress0/aufbv/fuzz00.smtv1.smt2
new file mode 100644
index 000000000..877917743
--- /dev/null
+++ b/test/regress/regress0/aufbv/fuzz00.smtv1.smt2
@@ -0,0 +1,7 @@
+(set-option :incremental false)
+(set-info :status sat)
+(set-logic QF_AUFBV)
+(declare-fun v0 () (_ BitVec 2))
+(declare-fun v1 () (_ BitVec 11))
+(declare-fun a2 () (Array (_ BitVec 5) (_ BitVec 15)))
+(check-sat-assuming ( (let ((_let_0 (ite (= (_ bv1 1) ((_ extract 0 0) v1)) (_ bv10435 15) ((_ sign_extend 6) (_ bv270 9))))) (let ((_let_1 (store a2 ((_ extract 8 4) (_ bv270 9)) (_ bv10435 15)))) (let ((_let_2 (select (store _let_1 ((_ extract 7 3) (_ bv270 9)) (bvsub ((_ sign_extend 13) v0) (_ bv10435 15))) ((_ extract 9 5) (select _let_1 ((_ extract 6 2) (_ bv270 9))))))) (let ((_let_3 (ite (= (_ bv10435 15) (select (store _let_1 ((_ extract 4 0) _let_0) ((_ zero_extend 13) v0)) ((_ zero_extend 4) (ite (bvugt (_ bv10435 15) (_ bv10435 15)) (_ bv1 1) (_ bv0 1))))) (_ bv1 1) (_ bv0 1)))) (let ((_let_4 (bvnor ((_ zero_extend 6) (_ bv270 9)) (select _let_1 ((_ extract 4 0) (select _let_1 ((_ extract 6 2) (_ bv270 9)))))))) (let ((_let_5 (ite (bvsgt (select _let_1 ((_ extract 4 0) (select _let_1 ((_ extract 6 2) (_ bv270 9))))) (select (store _let_1 ((_ extract 4 0) _let_0) ((_ zero_extend 13) v0)) ((_ zero_extend 4) (ite (bvugt (_ bv10435 15) (_ bv10435 15)) (_ bv1 1) (_ bv0 1))))) (_ bv1 1) (_ bv0 1)))) (let ((_let_6 ((_ sign_extend 1) (ite (bvugt (_ bv10435 15) (_ bv10435 15)) (_ bv1 1) (_ bv0 1))))) (let ((_let_7 (bvmul _let_6 v0))) (let ((_let_8 ((_ zero_extend 14) _let_3))) (let ((_let_9 ((_ sign_extend 4) v1))) (let ((_let_10 (= ((_ zero_extend 6) (_ bv270 9)) (bvsub ((_ sign_extend 13) v0) (_ bv10435 15))))) (let ((_let_11 ((_ zero_extend 14) (ite (bvslt v1 ((_ sign_extend 10) (ite (bvugt (_ bv10435 15) (_ bv10435 15)) (_ bv1 1) (_ bv0 1)))) (_ bv1 1) (_ bv0 1))))) (let ((_let_12 (= _let_3 (ite (bvugt (_ bv10435 15) (_ bv10435 15)) (_ bv1 1) (_ bv0 1))))) (let ((_let_13 (and (= _let_2 (select _let_1 ((_ extract 6 2) (_ bv270 9)))) _let_10))) (let ((_let_14 (ite (= ((_ zero_extend 1) (select _let_1 ((_ extract 6 2) v1))) ((_ sign_extend 4) ((_ extract 12 1) _let_2))) (= _let_2 ((_ zero_extend 14) (ite (= (bvsub ((_ sign_extend 13) v0) (_ bv10435 15)) _let_2) (_ bv1 1) (_ bv0 1)))) (= _let_2 ((_ sign_extend 14) (ite (bvslt v1 ((_ sign_extend 10) (ite (bvugt (_ bv10435 15) (_ bv10435 15)) (_ bv1 1) (_ bv0 1)))) (_ bv1 1) (_ bv0 1))))))) (let ((_let_15 (= (= ((_ sign_extend 14) (ite (bvuge (select _let_1 ((_ extract 6 2) (_ bv270 9))) ((_ sign_extend 14) _let_5)) (_ bv1 1) (_ bv0 1))) (select _let_1 ((_ extract 4 0) (select _let_1 ((_ extract 6 2) (_ bv270 9)))))) (= ((_ sign_extend 14) (ite (bvuge (select _let_1 ((_ extract 6 2) (_ bv270 9))) ((_ sign_extend 14) _let_5)) (_ bv1 1) (_ bv0 1))) (select _let_1 ((_ extract 4 0) (select _let_1 ((_ extract 6 2) (_ bv270 9))))))))) (let ((_let_16 (ite (ite (ite (= ((_ zero_extend 13) _let_7) (select _let_1 ((_ extract 6 2) (_ bv270 9)))) (= (select (store _let_1 ((_ extract 4 0) _let_0) ((_ zero_extend 13) v0)) ((_ zero_extend 4) (ite (bvugt (_ bv10435 15) (_ bv10435 15)) (_ bv1 1) (_ bv0 1)))) ((_ sign_extend 14) (ite (bvuge (select _let_1 ((_ extract 6 2) (_ bv270 9))) ((_ sign_extend 14) _let_5)) (_ bv1 1) (_ bv0 1)))) (= _let_0 _let_8)) (or (= ((_ zero_extend 14) (ite (bvuge (select _let_1 ((_ extract 6 2) (_ bv270 9))) ((_ sign_extend 14) _let_5)) (_ bv1 1) (_ bv0 1))) (_ bv10435 15)) (= ((_ zero_extend 10) _let_5) v1)) (= _let_2 ((_ zero_extend 14) _let_5))) (xor (or (= ((_ zero_extend 1) _let_2) ((_ zero_extend 1) (select _let_1 ((_ extract 6 2) v1)))) (= (= v1 v1) (or (= ((_ zero_extend 14) (ite (bvugt (_ bv10435 15) (_ bv10435 15)) (_ bv1 1) (_ bv0 1))) _let_4) (xor (= ((_ sign_extend 13) v0) (bvashr _let_0 ((_ zero_extend 13) v0))) (=> (= ((_ zero_extend 8) (ite (bvuge (select _let_1 ((_ extract 6 2) (_ bv270 9))) ((_ sign_extend 14) _let_5)) (_ bv1 1) (_ bv0 1))) (_ bv270 9)) (and (= ((_ sign_extend 14) (ite (bvuge (select _let_1 ((_ extract 6 2) (_ bv270 9))) ((_ sign_extend 14) _let_5)) (_ bv1 1) (_ bv0 1))) (bvsub ((_ sign_extend 13) v0) (_ bv10435 15))) (= ((_ zero_extend 14) (ite (= (bvsub ((_ sign_extend 13) v0) (_ bv10435 15)) _let_2) (_ bv1 1) (_ bv0 1))) (select _let_1 ((_ extract 4 0) (select _let_1 ((_ extract 6 2) (_ bv270 9)))))))))))) (= (=> (= (bvsub ((_ sign_extend 13) v0) (_ bv10435 15)) ((_ sign_extend 14) (ite (bvugt (_ bv10435 15) (_ bv10435 15)) (_ bv1 1) (_ bv0 1)))) _let_12) (not (= (ite (= (ite (= (bvsub ((_ sign_extend 13) v0) (_ bv10435 15)) _let_2) (_ bv1 1) (_ bv0 1)) (ite (bvuge (select _let_1 ((_ extract 6 2) (_ bv270 9))) ((_ sign_extend 14) _let_5)) (_ bv1 1) (_ bv0 1))) (= _let_0 ((_ zero_extend 6) (_ bv270 9))) (= (ite (bvslt v1 ((_ sign_extend 10) (ite (bvugt (_ bv10435 15) (_ bv10435 15)) (_ bv1 1) (_ bv0 1)))) (_ bv1 1) (_ bv0 1)) (ite (bvuge (select _let_1 ((_ extract 6 2) (_ bv270 9))) ((_ sign_extend 14) _let_5)) (_ bv1 1) (_ bv0 1)))) (ite _let_12 (= (= _let_0 _let_11) (= _let_8 (select (store _let_1 ((_ extract 4 0) _let_0) ((_ zero_extend 13) v0)) ((_ zero_extend 4) (ite (bvugt (_ bv10435 15) (_ bv10435 15)) (_ bv1 1) (_ bv0 1)))))) (= (_ bv10435 15) (select _let_1 ((_ extract 6 2) (_ bv270 9))))))))) (= (xor (= (bvsub ((_ sign_extend 13) v0) (_ bv10435 15)) ((_ zero_extend 4) v1)) (= _let_11 (select _let_1 ((_ extract 6 2) (_ bv270 9))))) (not (or (= (_ bv270 9) ((_ sign_extend 7) _let_7)) (= ((_ zero_extend 13) v0) _let_2))))))) (or (or _let_16 _let_16) (xor (xor (= (ite (bvuge (select _let_1 ((_ extract 6 2) (_ bv270 9))) ((_ sign_extend 14) _let_5)) (_ bv1 1) (_ bv0 1)) (ite (= (bvsub ((_ sign_extend 13) v0) (_ bv10435 15)) _let_2) (_ bv1 1) (_ bv0 1))) (ite (not (= ((_ sign_extend 7) (_ bv270 9)) ((_ zero_extend 1) (select _let_1 ((_ extract 6 2) v1))))) (= (= ((_ zero_extend 1) (select _let_1 ((_ extract 6 2) v1))) ((_ zero_extend 15) (ite (bvslt v1 ((_ sign_extend 10) (ite (bvugt (_ bv10435 15) (_ bv10435 15)) (_ bv1 1) (_ bv0 1)))) (_ bv1 1) (_ bv0 1)))) (not (= ((_ sign_extend 14) _let_5) _let_2))) (ite _let_13 (= (_ bv270 9) ((_ zero_extend 7) _let_7)) _let_13))) (and (or (ite (= (= ((_ sign_extend 15) _let_5) ((_ zero_extend 1) (select _let_1 ((_ extract 6 2) v1)))) (= _let_5 (ite (bvugt (_ bv10435 15) (_ bv10435 15)) (_ bv1 1) (_ bv0 1)))) (xor (ite (not (=> (= (_ bv270 9) ((_ zero_extend 7) v0)) _let_10)) (= ((_ sign_extend 1) (select _let_1 ((_ extract 6 2) (_ bv270 9)))) ((_ zero_extend 1) (select _let_1 ((_ extract 6 2) v1)))) (= ((_ zero_extend 14) (ite (= (bvsub ((_ sign_extend 13) v0) (_ bv10435 15)) _let_2) (_ bv1 1) (_ bv0 1))) (select _let_1 ((_ extract 6 2) v1)))) (= (select _let_1 ((_ extract 6 2) v1)) _let_9)) (=> (not (= (select _let_1 ((_ extract 6 2) v1)) ((_ sign_extend 14) _let_5))) (= ((_ zero_extend 1) (select _let_1 ((_ extract 6 2) v1))) ((_ zero_extend 15) (ite (bvuge (select _let_1 ((_ extract 6 2) (_ bv270 9))) ((_ sign_extend 14) _let_5)) (_ bv1 1) (_ bv0 1)))))) (= (not (= _let_7 ((_ sign_extend 1) _let_3))) (= (select _let_1 ((_ extract 4 0) (select _let_1 ((_ extract 6 2) (_ bv270 9))))) _let_9))) (=> (not (=> _let_15 _let_15)) (=> (or (= (= (= ((_ zero_extend 1) (select _let_1 ((_ extract 6 2) v1))) ((_ zero_extend 15) _let_5)) (= v1 ((_ zero_extend 2) (_ bv270 9)))) (and (= _let_6 _let_7) (and (= (select _let_1 ((_ extract 6 2) v1)) ((_ sign_extend 13) v0)) (=> (= ((_ sign_extend 14) (ite (bvslt v1 ((_ sign_extend 10) (ite (bvugt (_ bv10435 15) (_ bv10435 15)) (_ bv1 1) (_ bv0 1)))) (_ bv1 1) (_ bv0 1))) _let_4) (= (_ bv10435 15) _let_0))))) (not (= _let_4 _let_2))) (=> _let_14 _let_14))))))))))))))))))))))) ))