blob: 2a46d2a21ad4d8e26cecd0cdf550a97c062f28e4 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
|
; COMMAND-LINE: --cbqi-bv
; EXPECT: unsat
(set-logic BV)
(set-info :status unsat)
(declare-fun c_main_~i~6 () (_ BitVec 32))
(declare-fun c_main_~j~6 () (_ BitVec 32))
(declare-fun c_main_~k~6 () (_ BitVec 32))
(assert
(and (bvsle c_main_~i~6 (_ bv3 32)) (bvsle c_main_~i~6 (_ bv2 32))
(exists ((v_nnf_34 (_ BitVec 32)))
(and (bvsle (bvadd v_nnf_34 (_ bv3 32)) c_main_~k~6)
(bvsle v_nnf_34 (_ bv3 32)) (bvsle c_main_~j~6 (bvadd (bvmul (_ bv2 32) v_nnf_34) (_ bv1 32)))))))
(assert
(not
(and (bvsle c_main_~i~6 (_ bv3 32)) (bvsle c_main_~i~6 (_ bv2 32))
(exists ((v_nnf_30 (_ BitVec 32)))
(and (bvsle (bvadd v_nnf_30 (_ bv1 32)) c_main_~k~6)
(bvsle v_nnf_30 (_ bv3 32)) (bvsle c_main_~j~6 (bvadd (bvmul (_ bv2 32) v_nnf_30) (_ bv1 32))))))))
(check-sat)
(exit)
|
