Make CAD solver work for empty set of assertions (#5535)

When called with no assertions, the CAD solver would still go to work and then segfault when trying to access the first variable.
This PR adds an explicit check for this case and adds a regression.
Fixes #5534 .

diff --git a/src/theory/arith/nl/cad_solver.cpp b/src/theory/arith/nl/cad_solver.cpp
index 831530995397453706344f1510eac4315d7c0786..ea07392351c5ac944a4556ea82d3bed23b1c353f 100644 (file)
--- 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 8969b6c018e97fdaff83fff41be1531de5a1daa4..816202fa966e9bff69f6c742715a294842c46a6f 100644 (file)
--- 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 (file)
index 0000000..e7a9f0c
--- /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