From a1297ed93895f7405923d6d9e84432767a8abaae Mon Sep 17 00:00:00 2001
From: yoni206 <yoni206@users.noreply.github.com>
Date: Wed, 30 Jun 2021 13:22:17 -0700
Subject: [PATCH] pow2: new test (#6819)

This PR adds a more "real life" unit test for the pow2 solver. Thanks @4tXJ7f for the help with the options.
---
 test/regress/CMakeLists.txt                   |  1 +
 .../regress0/nl/pow2-pow-isabelle.smt2        | 20 +++++++++++++++++++
 2 files changed, 21 insertions(+)
 create mode 100644 test/regress/regress0/nl/pow2-pow-isabelle.smt2

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 5312e70a3..fe49d8b39 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -739,6 +739,7 @@ set(regress_0_tests
   regress0/nl/pow2-native-2.smt2
   regress0/nl/pow2-native-3.smt2
   regress0/nl/pow2-pow.smt2
+  regress0/nl/pow2-pow-isabelle.smt2
   regress0/nl/real-as-int.smt2
   regress0/nl/real-div-ufnra.smt2
   regress0/nl/sin-cos-346-b-chunk-0169.smt2
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)
-- 
2.30.2