blob: 970b9b3eab9d0b2a7daa5dc42070479c8a9c42b2 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
|
; COMMAND-LINE: --solve-bv-as-int=sum --nl-ext-tplanes
; EXPECT: unsat
(set-logic ALL)
(declare-fun x$ () (_ BitVec 32))
(declare-fun y$ () (_ BitVec 32))
(declare-fun z$ () (_ BitVec 32))
(declare-fun q$ () (_ BitVec 32))
(declare-fun n$ () Int)
(assert (>= n$ 0))
(define-fun bound () Int (bv2nat ((_ int2bv 32) (^ 2 11))))
;assumptions
(assert (< (bv2nat x$) bound))
(assert (< (bv2nat y$) (^ 2 (+ 11 n$))))
(assert (< (bv2nat z$) (^ 2 16)))
(assert (< (bv2nat q$) bound))
;conclusion
(assert (not (< (div (+ (bv2nat x$) (bv2nat y$)) (^ 2 n$)) (^ 2 32))))
(check-sat)
|
