blob: 14ddd16b000888c77070704eacdf113b2db11777 (
plain)
1
2
3
4
5
6
7
8
9
|
(set-option :incremental false)
(set-info :status sat)
(set-logic QF_BV)
(declare-fun v0 () (_ BitVec 7))
(declare-fun v1 () (_ BitVec 3))
(declare-fun v2 () (_ BitVec 2))
(declare-fun v3 () (_ BitVec 15))
(declare-fun v4 () (_ BitVec 11))
(check-sat-assuming ( (let ((_let_0 (concat v0 v0))) (let ((_let_1 (bvsmod ((_ zero_extend 5) ((_ rotate_left 7) (_ bv715 10))) v3))) (let ((_let_2 (bvneg v2))) (let ((_let_3 (ite (= (_ bv1 1) ((_ extract 1 1) _let_1)) (bvashr v3 ((_ sign_extend 5) (_ bv715 10))) ((_ sign_extend 4) v4)))) (let ((_let_4 ((_ sign_extend 12) _let_2))) (let ((_let_5 (bvsge (bvashr v3 ((_ sign_extend 5) (_ bv715 10))) (bvashr v3 ((_ sign_extend 5) (_ bv715 10)))))) (let ((_let_6 (not (or (bvsgt _let_0 ((_ sign_extend 4) (bvsub (bvsub ((_ rotate_left 7) (_ bv715 10)) ((_ rotate_left 7) (_ bv715 10))) ((_ zero_extend 3) v0)))) (not (xor (xor (distinct v4 ((_ zero_extend 2) (ite (= (_ bv1 1) ((_ extract 1 1) v2)) (_ bv331 9) ((_ sign_extend 6) v1)))) (bvslt _let_1 ((_ zero_extend 1) (bvmul (bvurem ((_ zero_extend 7) v0) _let_0) ((_ sign_extend 7) v0))))) (= ((_ sign_extend 14) (ite (bvuge (_ bv715 10) ((_ sign_extend 1) (_ bv331 9))) (_ bv1 1) (_ bv0 1))) v3))))))) (let ((_let_7 (or (bvuge _let_0 ((_ zero_extend 4) (bvsub ((_ rotate_left 7) (_ bv715 10)) ((_ rotate_left 7) (_ bv715 10))))) (not (not (=> (or (= (bvashr v3 ((_ sign_extend 5) (_ bv715 10))) _let_1) (bvult ((_ zero_extend 5) (_ bv331 9)) (bvurem ((_ zero_extend 7) v0) _let_0))) (distinct _let_1 ((_ sign_extend 6) (ite (= (_ bv1 1) ((_ extract 1 1) v2)) (_ bv331 9) ((_ sign_extend 6) v1)))))))))) (and (and (and (and (and (= (not (=> (and (bvugt ((_ zero_extend 1) (bvurem ((_ zero_extend 7) v0) _let_0)) _let_3) (xor (bvult _let_1 ((_ zero_extend 5) ((_ rotate_left 7) (_ bv715 10)))) (bvsgt ((_ sign_extend 1) (bvsub (bvsub ((_ rotate_left 7) (_ bv715 10)) ((_ rotate_left 7) (_ bv715 10))) ((_ zero_extend 3) v0))) (bvnot v4)))) (or (= (xor (bvsgt ((_ sign_extend 1) (_ bv715 10)) (bvnand ((_ sign_extend 9) v2) v4)) (= (and (bvslt _let_4 _let_0) (bvule _let_3 ((_ zero_extend 13) _let_2))) (bvugt ((_ sign_extend 3) v0) ((_ zero_extend 1) (ite (= (_ bv1 1) ((_ extract 1 1) v2)) (_ bv331 9) ((_ sign_extend 6) v1)))))) (bvuge (bvsub (bvsub ((_ rotate_left 7) (_ bv715 10)) ((_ rotate_left 7) (_ bv715 10))) ((_ zero_extend 3) v0)) ((_ sign_extend 9) (ite (bvuge (_ bv715 10) ((_ sign_extend 1) (_ bv331 9))) (_ bv1 1) (_ bv0 1))))) (or (not (= _let_0 ((_ zero_extend 12) v2))) (not (= (bvule v3 v3) (= (bvsge _let_4 (bvmul (bvurem ((_ zero_extend 7) v0) _let_0) ((_ sign_extend 7) v0))) (bvsge _let_1 ((_ zero_extend 13) v2))))))))) (xor (or (and (=> (bvslt (_ bv331 9) (ite (= (_ bv1 1) ((_ extract 1 1) v2)) (_ bv331 9) ((_ sign_extend 6) v1))) (ite (bvsgt ((_ zero_extend 12) v1) (bvashr v3 ((_ sign_extend 5) (_ bv715 10)))) (or (=> (= ((_ zero_extend 4) (bvsub ((_ rotate_left 7) (_ bv715 10)) ((_ rotate_left 7) (_ bv715 10)))) _let_0) (bvult (_ bv331 9) ((_ zero_extend 6) v1))) (bvugt (_ bv715 10) ((_ sign_extend 3) (bvsmod ((_ sign_extend 5) v2) v0)))) (= v0 ((_ zero_extend 6) (ite (bvuge (_ bv715 10) ((_ sign_extend 1) (_ bv331 9))) (_ bv1 1) (_ bv0 1)))))) (=> _let_6 _let_6)) (and _let_5 _let_5)) (or _let_7 _let_7))) (not (= v3 (_ bv0 15)))) (not (= v3 (bvnot (_ bv0 15))))) (not (= v0 (_ bv0 7)))) (not (= v0 (bvnot (_ bv0 7))))) (not (= _let_0 (_ bv0 14)))))))))))) ))
|
