blob: e9ecb909936b253e989f7967c0032e01def5468e (
plain)
1
2
3
4
5
6
7
8
|
(set-option :incremental false)
(set-info :status unsat)
(set-logic QF_BV)
(declare-fun v0 () (_ BitVec 3))
(declare-fun v1 () (_ BitVec 13))
(declare-fun v2 () (_ BitVec 14))
(declare-fun v3 () (_ BitVec 14))
(check-sat-assuming ( (let ((_let_0 (bvashr v1 ((_ sign_extend 1) (_ bv2692 12))))) (let ((_let_1 (ite (bvult v2 ((_ zero_extend 1) _let_0)) (_ bv1 1) (_ bv0 1)))) (let ((_let_2 (bvsub (_ bv2692 12) ((_ sign_extend 11) (ite (bvugt ((_ zero_extend 1) v1) v2) (_ bv1 1) (_ bv0 1)))))) (let ((_let_3 (ite (bvsle v2 ((_ sign_extend 2) _let_2)) (_ bv1 1) (_ bv0 1)))) (let ((_let_4 (bvmul _let_2 (_ bv2692 12)))) (let ((_let_5 (bvneg _let_4))) (let ((_let_6 (bvsdiv ((_ zero_extend 1) _let_2) _let_0))) (let ((_let_7 (bvsdiv ((_ sign_extend 11) (ite (distinct v3 ((_ zero_extend 13) _let_1)) (_ bv1 1) (_ bv0 1))) (_ bv2692 12)))) (let ((_let_8 ((_ zero_extend 2) _let_5))) (let ((_let_9 ((_ zero_extend 10) v0))) (let ((_let_10 (bvugt (_ bv2692 12) _let_2))) (let ((_let_11 ((_ zero_extend 11) _let_3))) (let ((_let_12 ((_ zero_extend 9) (bvnor ((_ zero_extend 2) _let_1) v0)))) (let ((_let_13 ((_ sign_extend 11) _let_1))) (let ((_let_14 (ite (not (xor (ite (or (bvule ((_ zero_extend 9) v0) _let_2) (bvuge _let_5 _let_7)) (=> (bvsge _let_2 _let_11) _let_10) (not _let_10)) (=> (xor (distinct ((_ zero_extend 12) (ite (bvugt ((_ zero_extend 1) v1) v2) (_ bv1 1) (_ bv0 1))) v1) (=> (bvugt ((_ zero_extend 2) (ite (bvugt ((_ zero_extend 1) v1) v2) (_ bv1 1) (_ bv0 1))) v0) (bvuge ((_ zero_extend 11) (ite (distinct v3 ((_ zero_extend 13) _let_1)) (_ bv1 1) (_ bv0 1))) _let_2))) (xor (or (bvult _let_4 _let_7) (bvsge _let_4 ((_ sign_extend 11) (ite (bvugt ((_ zero_extend 1) v1) v2) (_ bv1 1) (_ bv0 1))))) (or (bvult _let_4 _let_7) (bvsge _let_4 ((_ sign_extend 11) (ite (bvugt ((_ zero_extend 1) v1) v2) (_ bv1 1) (_ bv0 1))))))))) (not (xor (ite (or (bvule ((_ zero_extend 9) v0) _let_2) (bvuge _let_5 _let_7)) (=> (bvsge _let_2 _let_11) _let_10) (not _let_10)) (=> (xor (distinct ((_ zero_extend 12) (ite (bvugt ((_ zero_extend 1) v1) v2) (_ bv1 1) (_ bv0 1))) v1) (=> (bvugt ((_ zero_extend 2) (ite (bvugt ((_ zero_extend 1) v1) v2) (_ bv1 1) (_ bv0 1))) v0) (bvuge ((_ zero_extend 11) (ite (distinct v3 ((_ zero_extend 13) _let_1)) (_ bv1 1) (_ bv0 1))) _let_2))) (xor (or (bvult _let_4 _let_7) (bvsge _let_4 ((_ sign_extend 11) (ite (bvugt ((_ zero_extend 1) v1) v2) (_ bv1 1) (_ bv0 1))))) (or (bvult _let_4 _let_7) (bvsge _let_4 ((_ sign_extend 11) (ite (bvugt ((_ zero_extend 1) v1) v2) (_ bv1 1) (_ bv0 1))))))))) (and (or (xor (xor (bvugt _let_1 _let_1) (bvsgt (bvnor ((_ zero_extend 2) _let_1) v0) (bvnor ((_ zero_extend 2) _let_1) v0))) (and (= (bvult _let_5 _let_2) (bvslt _let_8 v2)) (=> (bvsle v3 ((_ sign_extend 1) _let_6)) (bvuge (_ bv2692 12) ((_ sign_extend 11) (ite (bvugt ((_ zero_extend 1) v1) v2) (_ bv1 1) (_ bv0 1))))))) (bvult _let_0 _let_9)) (bvule v2 ((_ zero_extend 13) (ite (distinct v3 ((_ zero_extend 13) _let_1)) (_ bv1 1) (_ bv0 1)))))))) (and (and (and (and (=> (ite _let_14 _let_14 _let_14) (not (or (not (and (or (= ((_ zero_extend 1) _let_6) v3) (xor (bvsgt _let_6 ((_ sign_extend 12) (ite (distinct v3 ((_ zero_extend 13) _let_1)) (_ bv1 1) (_ bv0 1)))) (bvult ((_ zero_extend 11) v0) v3))) (not (or (ite (ite (bvuge _let_1 _let_1) (= v1 ((_ sign_extend 10) v0)) (bvule ((_ sign_extend 11) _let_3) (_ bv2692 12))) (ite (bvsle _let_2 ((_ zero_extend 11) _let_1)) (ite (= (bvsle _let_5 _let_7) (distinct ((_ sign_extend 11) (ite (bvugt ((_ zero_extend 1) v1) v2) (_ bv1 1) (_ bv0 1))) _let_2)) (bvuge (_ bv2692 12) (_ bv2692 12)) (bvult _let_12 (_ bv2692 12))) (= v0 ((_ zero_extend 2) _let_3))) (xor (bvult _let_7 (_ bv2692 12)) (distinct v0 v0))) (= (_ bv2692 12) _let_12))))) (ite (not (or (= _let_2 (_ bv2692 12)) (= _let_2 _let_11))) (xor (not (bvsle v3 _let_8)) (ite (or (bvule _let_7 _let_12) (and (bvsge _let_1 (ite (distinct v3 ((_ zero_extend 13) _let_1)) (_ bv1 1) (_ bv0 1))) (bvslt _let_7 _let_13))) (ite (= ((_ sign_extend 2) _let_7) v2) (bvsgt ((_ zero_extend 2) _let_4) v2) (=> (bvslt v1 ((_ zero_extend 12) _let_3)) (bvsgt v1 v1))) (not (distinct _let_13 (_ bv2692 12))))) (not (bvule _let_9 _let_6)))))) (not (= _let_0 (_ bv0 13)))) (not (= _let_0 (bvnot (_ bv0 13))))) (not (= (_ bv2692 12) (_ bv0 12)))) (not (= (_ bv2692 12) (bvnot (_ bv0 12)))))))))))))))))))) ))
|
