diff options
| author | yoni206 <yoni206@users.noreply.github.com> | 2021-06-30 13:22:17 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-06-30 20:22:17 +0000 |
| commit | a1297ed93895f7405923d6d9e84432767a8abaae (patch) | |
| tree | bf855b835b8465b48d2fa26df6d00679c1474a2e | |
| parent | 6e502dbc3def28d0530218a0a2374e9e4c1a946d (diff) | |
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.
| -rw-r--r-- | test/regress/CMakeLists.txt | 1 | ||||
| -rw-r--r-- | test/regress/regress0/nl/pow2-pow-isabelle.smt2 | 20 |
2 files changed, 21 insertions, 0 deletions
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) |