blob: 57f248bc95a4cec782857f1fbcc746e5ad173697 (
plain)
1
2
3
4
5
6
7
|
(set-option :incremental false)
(set-info :status sat)
(set-logic QF_BV)
(declare-fun v0 () (_ BitVec 3))
(declare-fun v1 () (_ BitVec 12))
(declare-fun v2 () (_ BitVec 9))
(check-sat-assuming ( (let ((_let_0 ((_ sign_extend 5) (ite (bvsgt ((_ extract 6 6) (_ bv10 9)) ((_ extract 6 6) (_ bv10 9))) (_ bv1 1) (_ bv0 1))))) (let ((_let_1 (concat _let_0 (ite (bvult v2 v2) (_ bv1 1) (_ bv0 1))))) (let ((_let_2 (bvcomp _let_1 ((_ zero_extend 1) _let_0)))) (let ((_let_3 (bvadd ((_ sign_extend 2) (ite (bvule _let_0 ((_ zero_extend 5) _let_2)) (_ bv1 1) (_ bv0 1))) v0))) (let ((_let_4 (ite (bvslt ((_ extract 1 0) v0) ((_ extract 1 0) v0)) (_ bv1 1) (_ bv0 1)))) (let ((_let_5 ((_ sign_extend 8) ((_ extract 6 6) (_ bv10 9))))) (let ((_let_6 (bvlshr _let_5 v2))) (let ((_let_7 (bvxor (ite (bvult _let_0 ((_ sign_extend 4) ((_ extract 1 0) v0))) (_ bv1 1) (_ bv0 1)) (ite (bvult _let_0 ((_ sign_extend 4) ((_ extract 1 0) v0))) (_ bv1 1) (_ bv0 1))))) (let ((_let_8 ((_ sign_extend 7) ((_ extract 1 0) v0)))) (let ((_let_9 (bvnot v1))) (let ((_let_10 (= _let_6 (_ bv10 9)))) (let ((_let_11 (= (ite (bvsgt ((_ extract 6 6) (_ bv10 9)) ((_ extract 6 6) (_ bv10 9))) (_ bv1 1) (_ bv0 1)) ((_ extract 6 6) (_ bv10 9))))) (let ((_let_12 (= (ite (bvult v2 v2) (_ bv1 1) (_ bv0 1)) (ite (bvult v2 v2) (_ bv1 1) (_ bv0 1))))) (let ((_let_13 (= ((_ sign_extend 11) _let_2) v1))) (let ((_let_14 (or (=> (=> (=> (ite (or (= v1 ((_ zero_extend 11) (ite (bvult v2 v2) (_ bv1 1) (_ bv0 1)))) _let_10) (and (or (ite (or _let_11 (= _let_1 ((_ sign_extend 6) (ite (bvult v2 v2) (_ bv1 1) (_ bv0 1))))) (or _let_11 (= _let_1 ((_ sign_extend 6) (ite (bvult v2 v2) (_ bv1 1) (_ bv0 1))))) _let_12) (xor (xor (ite (and (= _let_0 ((_ zero_extend 5) (ite (bvult _let_0 ((_ sign_extend 4) ((_ extract 1 0) v0))) (_ bv1 1) (_ bv0 1)))) (= _let_6 ((_ sign_extend 6) _let_3))) (=> _let_11 (= _let_0 ((_ zero_extend 5) (ite (bvsgt ((_ extract 6 6) (_ bv10 9)) ((_ extract 6 6) (_ bv10 9))) (_ bv1 1) (_ bv0 1))))) (= ((_ sign_extend 2) (ite (bvule _let_0 ((_ zero_extend 5) _let_2)) (_ bv1 1) (_ bv0 1))) _let_3)) (=> _let_12 _let_13)) (= (= _let_9 ((_ zero_extend 3) (_ bv10 9))) (= _let_9 ((_ zero_extend 3) (_ bv10 9)))))) (ite (= ((_ zero_extend 8) (ite (bvsgt ((_ extract 6 6) (_ bv10 9)) ((_ extract 6 6) (_ bv10 9))) (_ bv1 1) (_ bv0 1))) v2) (= (_ bv10 9) ((_ sign_extend 8) (ite (bvult v2 v2) (_ bv1 1) (_ bv0 1)))) (= ((_ sign_extend 6) _let_2) _let_1))) (or (= v1 ((_ zero_extend 11) (ite (bvult v2 v2) (_ bv1 1) (_ bv0 1)))) _let_10)) (or (and (or (not (= _let_4 (ite (bvult _let_0 ((_ sign_extend 4) ((_ extract 1 0) v0))) (_ bv1 1) (_ bv0 1)))) (= _let_9 ((_ sign_extend 3) _let_6))) (or (= ((_ zero_extend 8) (ite (bvult _let_0 ((_ sign_extend 4) ((_ extract 1 0) v0))) (_ bv1 1) (_ bv0 1))) _let_6) (= v0 ((_ zero_extend 2) _let_4)))) (= ((_ sign_extend 6) v0) _let_6))) (ite (= (= (_ bv10 9) (bvand v2 _let_8)) (and _let_10 (= ((_ sign_extend 8) (ite (bvule _let_0 ((_ zero_extend 5) _let_2)) (_ bv1 1) (_ bv0 1))) v2))) (xor (xor (= ((_ zero_extend 8) (ite (bvule _let_0 ((_ zero_extend 5) _let_2)) (_ bv1 1) (_ bv0 1))) (bvand v2 _let_8)) (= ((_ zero_extend 8) (ite (bvule _let_0 ((_ zero_extend 5) _let_2)) (_ bv1 1) (_ bv0 1))) (bvand v2 _let_8))) (xor (xor (= ((_ zero_extend 3) ((_ repeat 2) v0)) ((_ rotate_right 4) _let_6)) (= (= _let_8 v2) _let_13)) (= (= ((_ zero_extend 8) ((_ extract 6 6) (_ bv10 9))) _let_6) (= ((_ zero_extend 2) (ite (bvult v2 v2) (_ bv1 1) (_ bv0 1))) _let_3)))) (= v0 ((_ sign_extend 2) (ite (bvsgt ((_ extract 6 6) (_ bv10 9)) ((_ extract 6 6) (_ bv10 9))) (_ bv1 1) (_ bv0 1)))))) (or (= (= (xor (= _let_2 (ite (bvsgt ((_ extract 6 6) (_ bv10 9)) ((_ extract 6 6) (_ bv10 9))) (_ bv1 1) (_ bv0 1))) (= v2 ((_ zero_extend 8) _let_7))) (= _let_3 ((_ sign_extend 2) _let_2))) (xor (= ((_ zero_extend 11) (ite (bvult v2 v2) (_ bv1 1) (_ bv0 1))) v1) (= (ite (bvsgt ((_ extract 6 6) (_ bv10 9)) ((_ extract 6 6) (_ bv10 9))) (_ bv1 1) (_ bv0 1)) (ite (bvult _let_0 ((_ sign_extend 4) ((_ extract 1 0) v0))) (_ bv1 1) (_ bv0 1))))) (= (= (xor (= _let_2 (ite (bvsgt ((_ extract 6 6) (_ bv10 9)) ((_ extract 6 6) (_ bv10 9))) (_ bv1 1) (_ bv0 1))) (= v2 ((_ zero_extend 8) _let_7))) (= _let_3 ((_ sign_extend 2) _let_2))) (xor (= ((_ zero_extend 11) (ite (bvult v2 v2) (_ bv1 1) (_ bv0 1))) v1) (= (ite (bvsgt ((_ extract 6 6) (_ bv10 9)) ((_ extract 6 6) (_ bv10 9))) (_ bv1 1) (_ bv0 1)) (ite (bvult _let_0 ((_ sign_extend 4) ((_ extract 1 0) v0))) (_ bv1 1) (_ bv0 1))))))) (xor (= (= ((_ zero_extend 8) _let_2) v2) (= ((_ zero_extend 11) _let_7) v1)) (not (ite (= _let_1 ((_ zero_extend 6) ((_ extract 6 6) (_ bv10 9)))) (= _let_3 ((_ sign_extend 2) ((_ extract 6 6) (_ bv10 9)))) (= _let_6 _let_5))))))) (xor (not (=> (not (ite (= ((_ sign_extend 1) ((_ extract 6 6) (_ bv10 9))) ((_ extract 1 0) v0)) (or (= ((_ repeat 2) v0) ((_ zero_extend 5) ((_ extract 6 6) (_ bv10 9)))) (= ((_ zero_extend 1) _let_2) ((_ extract 1 0) v0))) (= ((_ sign_extend 1) _let_4) ((_ extract 1 0) v0)))) (= _let_3 ((_ zero_extend 2) _let_4)))) (or _let_14 _let_14))))))))))))))))) ))
|
