4 files changed, 36 insertions, 0 deletions
diff --git a/test/regress/regress0/nl/pow2-native-0.smt2 b/test/regress/regress0/nl/pow2-native-0.smt2
new file mode 100644
index 000000000..f88ac4151
--- /dev/null
+++ b/test/regress/regress0/nl/pow2-native-0.smt2
@@ -0,0 +1,6 @@
+; EXPECT: unsat
+(set-logic QF_NIA)
+(declare-fun x () Int)
+(assert (< x 0))
+(assert (distinct (pow2 x) 0))
+(check-sat)
diff --git a/test/regress/regress0/nl/pow2-native-1.smt2 b/test/regress/regress0/nl/pow2-native-1.smt2
new file mode 100644
index 000000000..1e24ae572
--- /dev/null
+++ b/test/regress/regress0/nl/pow2-native-1.smt2
@@ -0,0 +1,9 @@
+; EXPECT: sat
+(set-logic QF_NIA)
+(set-info :status sat)
+(declare-fun x () Int)
+
+(assert (and (<= 0 x) (< x 16)))
+(assert (> (pow2 x) 0))
+
+(check-sat)
diff --git a/test/regress/regress0/nl/pow2-native-2.smt2 b/test/regress/regress0/nl/pow2-native-2.smt2
new file mode 100644
index 000000000..ba0621dbc
--- /dev/null
+++ b/test/regress/regress0/nl/pow2-native-2.smt2
@@ -0,0 +1,9 @@
+; EXPECT: unsat
+(set-logic QF_NIA)
+(set-info :status unsat)
+(declare-fun x () Int)
+
+(assert (and (<= 0 x) (< x 16)))
+(assert (< (pow2 x) x))
+
+(check-sat)
diff --git a/test/regress/regress0/nl/pow2-native-3.smt2 b/test/regress/regress0/nl/pow2-native-3.smt2
new file mode 100644
index 000000000..45975a474
--- /dev/null
+++ b/test/regress/regress0/nl/pow2-native-3.smt2
@@ -0,0 +1,12 @@
+; EXPECT: unsat
+(set-logic QF_NIA)
+(set-info :status unsat)
+(declare-fun x () Int)
+(declare-fun y () Int)
+
+(assert (<= 0 x))
+(assert (<= 0 y))
+(assert (< x y))
+(assert (> (pow2 x) (pow2 y)))
+
+(check-sat)