From 865d1ee48de8e4a21d1e97c707be46c34918367d Mon Sep 17 00:00:00 2001
From: Gereon Kremer <gereon.kremer@cs.rwth-aachen.de>
Date: Thu, 26 Nov 2020 17:02:16 +0100
Subject: [PATCH] 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 .
---
 src/theory/arith/nl/cad_solver.cpp                   |  8 ++++++++
 test/regress/CMakeLists.txt                          |  1 +
 .../regress/regress0/nl/issue5534-no-assertions.smt2 | 12 ++++++++++++
 3 files changed, 21 insertions(+)
 create mode 100644 test/regress/regress0/nl/issue5534-no-assertions.smt2

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
-- 
2.30.2