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