3 files changed, 21 insertions, 0 deletions
diff --git a/src/theory/arith/nl/cad_solver.cpp b/src/theory/arith/nl/cad_solver.cpp
index 831530995..ea0739235 100644
--- a/src/theory/arith/nl/cad_solver.cpp
+++ b/src/theory/arith/nl/cad_solver.cpp
@@ -71,6 +71,10 @@ void CadSolver::initLastCall(const std::vector<Node>& assertions)
 void CadSolver::checkFull()
 {
 #ifdef CVC4_POLY_IMP
+  if (d_CAC.getConstraints().getConstraints().empty()) {
+    Trace("nl-cad") << "No constraints. Return." << std::endl;
+    return;
+  }
   auto covering = d_CAC.getUnsatCover();
   if (covering.empty())
   {
@@ -101,6 +105,10 @@ void CadSolver::checkFull()
 void CadSolver::checkPartial()
 {
 #ifdef CVC4_POLY_IMP
+  if (d_CAC.getConstraints().getConstraints().empty()) {
+    Trace("nl-cad") << "No constraints. Return." << std::endl;
+    return;
+  }
   auto covering = d_CAC.getUnsatCover(0, true);
   if (covering.empty())
   {
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 8969b6c01..816202fa9 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -622,6 +622,7 @@ set(regress_0_tests
   regress0/nl/issue3971.smt2
   regress0/nl/issue3991.smt2
   regress0/nl/issue4007-rint-uf.smt2
+  regress0/nl/issue5534-no-assertions.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/issue5534-no-assertions.smt2 b/test/regress/regress0/nl/issue5534-no-assertions.smt2
new file mode 100644
index 000000000..e7a9f0cd1
--- /dev/null
+++ b/test/regress/regress0/nl/issue5534-no-assertions.smt2
@@ -0,0 +1,12 @@
+; COMMAND-LINE: --incremental
+; EXPECT: unsat
+; EXPECT: sat
+(set-logic QF_UFNRA)
+(declare-fun r () Real)
+(declare-fun u (Real Real) Bool)
+(assert (u 0.0 (* r r)))
+(push)
+(assert (and (< r 0.0) (< 0.0 r)))
+(check-sat)
+(pop)
+(check-sat)
+\ No newline at end of file