3 files changed, 30 insertions, 0 deletions
diff --git a/test/regress/Makefile.tests b/test/regress/Makefile.tests
index 6400411cb..f707da219 100644
--- a/test/regress/Makefile.tests
+++ b/test/regress/Makefile.tests
@@ -503,6 +503,7 @@ REG0_TESTS = \
 	regress0/nl/magnitude-wrong-1020-m.smt2 \
 	regress0/nl/mult-po.smt2 \
 	regress0/nl/nia-wrong-tl.smt2 \
+	regress0/nl/nlExtPurify-test.smt2 \
 	regress0/nl/nta/cos-sig-value.smt2 \
 	regress0/nl/nta/exp-n0.5-lb.smt2 \
 	regress0/nl/nta/exp-n0.5-ub.smt2 \
@@ -1301,6 +1302,7 @@ REG1_TESTS = \
 	regress1/quantifiers/model_6_1_bv.smt2 \
 	regress1/quantifiers/mutualrec2.cvc \
 	regress1/quantifiers/nested9_true-unreach-call.i_575.smt2 \
+	regress1/quantifiers/nl-pow-trick.smt2 \
 	regress1/quantifiers/nra-interleave-inst.smt2 \
 	regress1/quantifiers/opisavailable-12.smt2 \
 	regress1/quantifiers/parametric-lists.smt2 \
diff --git a/test/regress/regress0/nl/nlExtPurify-test.smt2 b/test/regress/regress0/nl/nlExtPurify-test.smt2
new file mode 100644
index 000000000..1a2391c3b
--- /dev/null
+++ b/test/regress/regress0/nl/nlExtPurify-test.smt2
@@ -0,0 +1,15 @@
+; COMMAND-LINE: --nl-ext-purify
+; EXPECT: sat
+(set-info :smt-lib-version 2.6)
+(set-logic QF_NRA)
+(set-info :category "crafted")
+(set-info :status sat)
+(declare-fun skoX () Real)
+(declare-fun skoS3 () Real)
+(declare-fun skoSX () Real)
+
+(assert (and (not (<= skoX 0)) (and (not (<= (* (+ skoS3 skoSX) (+ skoS3 skoSX) (+ skoS3 skoSX) (+ skoS3 skoSX) (+ skoS3 skoSX) (+ skoS3 skoSX) (+ skoS3 skoSX) (+ skoS3 skoSX) (+ skoS3 skoSX) (+ skoS3 skoSX) (+ skoS3 skoSX) (+ skoS3 skoSX) (+ skoS3 skoSX) (+ skoS3 skoSX) (+ skoS3 skoSX) (+ skoS3 skoSX) (+ skoS3 skoSX) (+ skoS3 skoSX) (+ skoS3 skoSX) (+ skoS3 skoSX) (+ skoS3 skoSX) (+ skoS3 skoSX) (+ skoS3 skoSX) (+ skoS3 skoSX) (+ skoS3 skoSX) (+ skoS3 skoSX) (+ skoS3 skoSX) (+ skoS3 skoSX) (+ skoS3 skoSX) (+ skoS3 skoSX) (+ skoS3 skoSX) (+ skoS3 skoSX)) 0)) (not (<= skoS3 0)))))
+
+
+(check-sat)
+(exit)
diff --git a/test/regress/regress1/quantifiers/nl-pow-trick.smt2 b/test/regress/regress1/quantifiers/nl-pow-trick.smt2
new file mode 100644
index 000000000..a369fd9f9
--- /dev/null
+++ b/test/regress/regress1/quantifiers/nl-pow-trick.smt2
@@ -0,0 +1,13 @@
+; COMMAND-LINE: --cbqi-all
+; EXPECT: unsat
+(set-logic NIA)
+(declare-fun a () Int)
+(declare-fun b () Int)
+(declare-fun c () Int)
+(define-fun s ((x Int)) Int (+ x 1))
+(define-fun seq ((a Int) (b Int) (k Int) (x Int)) Bool ( = x (mod (+ 1 (* b (+ 1 k))) a)))
+(define-fun power ((a Int) (b Int) (c Int)) Bool 
+(exists ((x Int) (y Int)) (and (seq x y 0 1) (seq x y b c) (forall ((k Int) (z Int)) (=> (and (< k b) (seq x y k z)) (seq x y (+ 1 k) (* a z))))))
+)
+(assert (power 2 3 8))
+(check-sat)