diff options
Diffstat (limited to 'test')
| -rw-r--r-- | test/regress/CMakeLists.txt | 1 | ||||
| -rw-r--r-- | test/regress/regress0/nl/pow2-pow.smt2 | 6 | ||||
| -rw-r--r-- | test/regress/regress1/arith/bug716.1.cvc | 4 |
3 files changed, 9 insertions, 2 deletions
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index d2d6f0855..abd21e222 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -737,6 +737,7 @@ set(regress_0_tests regress0/nl/pow2-native-1.smt2 regress0/nl/pow2-native-2.smt2 regress0/nl/pow2-native-3.smt2 + regress0/nl/pow2-pow.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.smt2 b/test/regress/regress0/nl/pow2-pow.smt2 new file mode 100644 index 000000000..8fdbfa659 --- /dev/null +++ b/test/regress/regress0/nl/pow2-pow.smt2 @@ -0,0 +1,6 @@ +; EXPECT: unsat +(set-logic QF_NIA) +(declare-fun x () Int) +(assert (< x 0)) +(assert (distinct (^ 2 x) 0)) +(check-sat) diff --git a/test/regress/regress1/arith/bug716.1.cvc b/test/regress/regress1/arith/bug716.1.cvc index 854062beb..50be132af 100644 --- a/test/regress/regress1/arith/bug716.1.cvc +++ b/test/regress/regress1/arith/bug716.1.cvc @@ -1,6 +1,6 @@ % EXPECT: The exponent of the POW(^) operator can only be a positive integral constant below 67108864. Exception occurred in: -% EXPECT: 2 ^ x +% EXPECT: 3 ^ x % EXIT: 1 x: INT; -ASSERT 2^x = 8; +ASSERT 3^x = 27; QUERY x=3; |