diff options
Diffstat (limited to 'test/regress/regress1/bv2int-isabelle.smt2')
| -rw-r--r-- | test/regress/regress1/bv2int-isabelle.smt2 | 16 |
1 files changed, 16 insertions, 0 deletions
diff --git a/test/regress/regress1/bv2int-isabelle.smt2 b/test/regress/regress1/bv2int-isabelle.smt2 new file mode 100644 index 000000000..e8d1efe51 --- /dev/null +++ b/test/regress/regress1/bv2int-isabelle.smt2 @@ -0,0 +1,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) |