blob: 60e764537e13b7bbb7cf831b632750655c930de5 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
|
(set-logic QF_BV)
(set-info :status sat)
(declare-fun v0 () (_ BitVec 4))
(assert (let ((e1(_ bv0 1)))
(let ((e2(_ bv11134 16)))
(let ((e3 (bvadd e2 ((_ sign_extend 12) v0))))
(let ((e4 (ite (= e2 ((_ sign_extend 12) v0)) (_ bv1 1) (_ bv0 1))))
(let ((e5 (bvlshr e3 ((_ sign_extend 12) v0))))
(let ((e6 (bvxnor e2 ((_ zero_extend 12) v0))))
(let ((e7 (ite (bvult ((_ sign_extend 15) e1) e2) (_ bv1 1) (_ bv0 1))))
(let ((e8 (bvugt e7 e1)))
(let ((e9 (bvule ((_ sign_extend 3) e7) v0)))
(let ((e10 (bvsgt e5 ((_ zero_extend 12) v0))))
(let ((e11 (= e6 e3)))
(let ((e12 (bvslt ((_ zero_extend 15) e4) e5)))
(let ((e13 (bvugt e5 e2)))
(let ((e14 (ite e10 e8 e10)))
(let ((e15 (xor e13 e11)))
(let ((e16 (xor e14 e15)))
(let ((e17 (ite e9 e12 e16)))
e17
))))))))))))))))))
(check-sat)
|
