diff options
| author | Gereon Kremer <gereon.kremer@cs.rwth-aachen.de> | 2020-11-26 17:02:16 +0100 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-11-26 10:02:16 -0600 |
| commit | 865d1ee48de8e4a21d1e97c707be46c34918367d (patch) | |
| tree | d1721f2cd0ccee285d8a4828cd6c184e2c446046 /src | |
| parent | d3eb6f04bcdb6c22a2f796a19ff96094d2cfbb88 (diff) | |
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 .
Diffstat (limited to 'src')
| -rw-r--r-- | src/theory/arith/nl/cad_solver.cpp | 8 |
1 files changed, 8 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()) { |