projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: d3eb6f0) | patch
Make CAD solver work for empty set of assertions (#5535)
authorGereon Kremer <gereon.kremer@cs.rwth-aachen.de>
Thu, 26 Nov 2020 16:02:16 +0000 (17:02 +0100)
committerGitHub <noreply@github.com>
Thu, 26 Nov 2020 16:02:16 +0000 (10:02 -0600)
commit865d1ee48de8e4a21d1e97c707be46c34918367d
treed1721f2cd0ccee285d8a4828cd6c184e2c446046tree
parentd3eb6f04bcdb6c22a2f796a19ff96094d2cfbb88commit | 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 .
src/theory/arith/nl/cad_solver.cpp diff | blob | history
test/regress/CMakeLists.txt diff | blob | history
test/regress/regress0/nl/issue5534-no-assertions.smt2 [new file with mode: 0644] blob