4 files changed, 24 insertions, 0 deletions
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 7ceb3b4b2..dd6956b09 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -686,6 +686,9 @@ set(regress_0_tests
   regress0/nl/issue5534-no-assertions.smt2
   regress0/nl/issue5726-downpolys.smt2
   regress0/nl/issue5726-sqfactor.smt2
+  regress0/nl/issue5737-div00.smt2
+  regress0/nl/issue5740-mod00.smt2
+  regress0/nl/issue5740-2-mod00.smt2
   regress0/nl/magnitude-wrong-1020-m.smt2
   regress0/nl/mult-po.smt2
   regress0/nl/nia-wrong-tl.smt2
diff --git a/test/regress/regress0/nl/issue5737-div00.smt2 b/test/regress/regress0/nl/issue5737-div00.smt2
new file mode 100644
index 000000000..59de5a3fb
--- /dev/null
+++ b/test/regress/regress0/nl/issue5737-div00.smt2
@@ -0,0 +1,6 @@
+; COMMAND-LINE: --ext-rew-prep -q
+; EXPECT: sat
+(set-logic ALL)
+(set-info :status sat)
+(assert (> (div 0 0) 0))
+(check-sat)
diff --git a/test/regress/regress0/nl/issue5740-2-mod00.smt2 b/test/regress/regress0/nl/issue5740-2-mod00.smt2
new file mode 100644
index 000000000..01930da6d
--- /dev/null
+++ b/test/regress/regress0/nl/issue5740-2-mod00.smt2
@@ -0,0 +1,8 @@
+; COMMAND-LINE: --ext-rewrite-quant --sygus-inst --no-check-models
+; EXPECT: sat
+(set-logic ALL)
+(set-info :status sat)
+(declare-fun c (Int) Bool)
+(define-fun d ((e Int)) Bool (forall ((a Int) (b Int)) (! true :pattern ((c a) (c b)))))
+(assert (exists ((e Int)) (distinct (d e) (= (ite (= e 0) (mod 0 e) 0) 0))))
+(check-sat)
diff --git a/test/regress/regress0/nl/issue5740-mod00.smt2 b/test/regress/regress0/nl/issue5740-mod00.smt2
new file mode 100644
index 000000000..e1287dacb
--- /dev/null
+++ b/test/regress/regress0/nl/issue5740-mod00.smt2
@@ -0,0 +1,7 @@
+; COMMAND-LINE: --ext-rewrite-quant -q
+; EXPECT: sat
+(set-logic ALL)
+(set-info :status sat)
+(define-fun f ((a Int) (b Int)) Int (ite (= b 0) 0 a))
+(assert (exists ((c Int)) (distinct (f c (mod 0 0)) 0)))
+(check-sat)