blob: e8d1efe519ec5e090419af302db11bb1364cae76 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
|
; COMMAND-LINE: --solve-bv-as-int=sum --no-check-unsat-cores
; EXPECT: unsat
(set-logic ALL)
(declare-fun s$ () (_ BitVec 32))
(declare-fun x$ () (_ BitVec 32))
(declare-fun i$ () (_ BitVec 32))
(define-fun bound () Int (bv2nat ((_ int2bv 32) 2048)))
(define-fun bseg ((x (_ BitVec 32)) (s (_ BitVec 32))) Bool (and (< (bv2nat x) bound) (<= (+ (bv2nat x) (bv2nat s)) bound)))
;assumptions
(assert (bseg x$ s$))
(assert (<= (bv2nat i$) (bv2nat s$)))
;conclusion
(assert (not (= (bv2nat (bvadd x$ i$)) (+ (bv2nat x$) (bv2nat i$)))))
(check-sat)
|
