test/regress/regress0/aufbv/fuzz08.smtv1.smt2


1
2
3
4
5
6
7
8

(set-option :incremental false)
(set-info :status sat)
(set-logic QF_AUFBV)
(declare-fun v0 () (_ BitVec 12))
(declare-fun v1 () (_ BitVec 14))
(declare-fun v2 () (_ BitVec 9))
(declare-fun a3 () (Array (_ BitVec 5) (_ BitVec 3)))
(check-sat-assuming ( (let ((_let_0 (ite (bvsge v0 ((_ sign_extend 3) v2)) (_ bv1 1) (_ bv0 1)))) (let ((_let_1 (concat (_ bv0 2) v1))) (let ((_let_2 (select a3 ((_ extract 7 3) v2)))) (let ((_let_3 (select a3 ((_ sign_extend 2) (select a3 ((_ zero_extend 4) _let_0)))))) (let ((_let_4 (bvneg (ite (bvule ((_ zero_extend 2) (_ bv3960 12)) v1) (_ bv1 1) (_ bv0 1))))) (let ((_let_5 (bvnot (select a3 ((_ zero_extend 4) _let_0))))) (let ((_let_6 ((_ rotate_left 2) (select a3 ((_ extract 11 7) v0))))) (let ((_let_7 (bvnand ((_ sign_extend 2) _let_0) _let_6))) (let ((_let_8 ((_ zero_extend 0) _let_1))) (let ((_let_9 ((_ zero_extend 13) (select a3 ((_ zero_extend 4) _let_0))))) (let ((_let_10 ((_ zero_extend 6) _let_2))) (let ((_let_11 (bvsrem _let_10 v2))) (let ((_let_12 (bvsdiv ((_ sign_extend 4) (_ bv3960 12)) _let_1))) (let ((_let_13 (bvxnor v0 ((_ sign_extend 9) _let_5)))) (let ((_let_14 (bvnot _let_3))) (let ((_let_15 (ite (distinct (_ bv0 2) (_ bv0 2)) (_ bv1 1) (_ bv0 1)))) (let ((_let_16 (ite (= (_ bv1 1) ((_ extract 9 9) v1)) _let_6 (select a3 ((_ zero_extend 4) _let_0))))) (let ((_let_17 ((_ zero_extend 13) _let_2))) (let ((_let_18 ((_ zero_extend 1) (_ bv0 2)))) (let ((_let_19 ((_ zero_extend 11) _let_15))) (let ((_let_20 ((_ sign_extend 15) (ite (bvule ((_ zero_extend 2) (_ bv3960 12)) v1) (_ bv1 1) (_ bv0 1))))) (let ((_let_21 ((_ sign_extend 1) (_ bv0 2)))) (let ((_let_22 ((_ sign_extend 2) _let_15))) (let ((_let_23 ((_ zero_extend 11) _let_4))) (let ((_let_24 (bvule _let_4 _let_0))) (let ((_let_25 (xor (xor (bvsge _let_7 _let_6) (bvule _let_4 (ite (bvule ((_ zero_extend 2) (_ bv3960 12)) v1) (_ bv1 1) (_ bv0 1)))) (= _let_8 _let_20)))) (let ((_let_26 (ite (= _let_12 ((_ sign_extend 13) _let_2)) (= (=> (= _let_23 (_ bv3960 12)) (= v2 ((_ sign_extend 8) (ite (bvule ((_ zero_extend 2) (_ bv3960 12)) v1) (_ bv1 1) (_ bv0 1))))) (bvsgt ((_ zero_extend 15) (ite (bvule ((_ zero_extend 2) (_ bv3960 12)) v1) (_ bv1 1) (_ bv0 1))) _let_12)) (ite (= (xor (distinct _let_21 _let_2) (distinct ((_ zero_extend 9) _let_16) _let_13)) (bvsgt ((_ sign_extend 2) _let_4) _let_2)) (bvslt _let_18 _let_2) (ite (= (= _let_9 _let_12) (bvsgt _let_8 ((_ sign_extend 13) (select a3 ((_ extract 11 7) v0))))) (ite (and (bvsle _let_22 _let_6) (bvslt ((_ sign_extend 6) _let_14) _let_11)) (xor (bvult v1 ((_ sign_extend 11) _let_6)) (= ((_ zero_extend 2) (ite (bvule ((_ zero_extend 2) (_ bv3960 12)) v1) (_ bv1 1) (_ bv0 1))) _let_7)) (bvugt _let_16 _let_2)) (=> (bvult _let_12 ((_ zero_extend 13) _let_3)) (bvsge _let_13 (_ bv3960 12)))))))) (let ((_let_27 (not (and (bvsgt _let_16 _let_18) (bvuge _let_22 _let_2))))) (and (and (and (and (or (ite (ite _let_26 (not (bvsgt v0 ((_ zero_extend 3) v2))) _let_26) (= (=> (ite (xor (and (bvslt (_ bv3960 12) ((_ zero_extend 11) (ite (bvule ((_ zero_extend 2) (_ bv3960 12)) v1) (_ bv1 1) (_ bv0 1)))) (bvult v2 ((_ sign_extend 6) (select a3 ((_ zero_extend 4) _let_0))))) (and (and _let_25 _let_25) (xor (bvsgt ((_ zero_extend 13) (select a3 ((_ extract 11 7) v0))) _let_1) (xor (bvult v0 ((_ sign_extend 9) _let_3)) (bvult _let_9 _let_17))))) _let_27 _let_27) (= (bvuge (select a3 ((_ zero_extend 4) _let_0)) (select a3 ((_ extract 11 7) v0))) (or (and (= (bvslt _let_14 _let_7) (ite (bvsgt ((_ sign_extend 14) (_ bv0 2)) _let_9) (= _let_8 ((_ sign_extend 4) _let_13)) (= (= _let_3 _let_7) (bvule _let_9 ((_ zero_extend 13) _let_6))))) (or (bvsle _let_5 _let_18) (or (bvsgt v0 ((_ sign_extend 9) _let_2)) (bvule v0 _let_19)))) (bvuge ((_ zero_extend 11) _let_0) (_ bv3960 12))))) (ite (= (bvult (_ bv3960 12) _let_23) (bvsge ((_ sign_extend 11) (ite (bvule ((_ zero_extend 2) (_ bv3960 12)) v1) (_ bv1 1) (_ bv0 1))) v0)) (or (= _let_24 _let_24) (and (bvsge _let_8 _let_17) (bvuge _let_1 _let_20))) (and (ite (and (bvsgt _let_3 ((_ zero_extend 2) _let_15)) (not (distinct v2 ((_ zero_extend 8) (ite (bvule ((_ zero_extend 2) (_ bv3960 12)) v1) (_ bv1 1) (_ bv0 1)))))) (=> (bvule ((_ zero_extend 2) _let_4) (select a3 ((_ extract 11 7) v0))) (bvuge _let_3 (select a3 ((_ zero_extend 4) _let_0)))) (= (not (bvsle _let_17 _let_8)) (=> (bvsle ((_ zero_extend 11) (select a3 ((_ zero_extend 4) _let_0))) v1) (bvsle (_ bv3960 12) _let_13)))) (=> (=> (distinct _let_21 (select a3 ((_ extract 11 7) v0))) (not (bvslt v1 ((_ zero_extend 11) (select a3 ((_ extract 11 7) v0)))))) (not (=> (xor (bvugt _let_7 _let_2) (bvult ((_ zero_extend 13) _let_7) _let_12)) (bvsgt _let_11 _let_10))))))) (bvslt _let_4 _let_0)) (or (bvslt ((_ zero_extend 5) v2) v1) (ite (not (bvule _let_16 _let_22)) (or (bvuge _let_2 _let_6) (= v0 _let_19)) (ite (bvslt _let_2 _let_2) (or (bvsge _let_9 ((_ zero_extend 13) _let_14)) (bvsgt _let_18 _let_3)) (distinct ((_ zero_extend 1) _let_0) (_ bv0 2)))))) (not (= _let_1 (_ bv0 16)))) (not (= _let_1 (bvnot (_ bv0 16))))) (not (= v2 (_ bv0 9)))) (not (= v2 (bvnot (_ bv0 9))))))))))))))))))))))))))))))))) ))