Fix issue #1074, improve non-fatal error handling (#1075)

Commit 54d24c786d6a843cc72dfb5e377603349ea5e420 was
changing CVC4 to handle certain non-fatal errors
(such as calling get-unsat-core without a proceding
unsat check-sat command) without terminating the
solver. In the case of get-unsat-cores, the changes
lead to the solver crashing because it was trying to
print an unsat core initialized with the default
constructor, so the member variable d_smt was NULL,
which lead to a dereference of a null pointer.

One of the issues of the way non-fatal errors were
handled was that the error reporting was done in the
invoke() method of the command instead of the
printResult() method, which lead to the error
described above and other issues such as a call to
get-value printing a value after reporting an error.

This commit aims to improve the design by adding a
RecoverableModalException for errors that the solver
can recover from and CommandRecoverableFailure to
communicate that a command failed in a way that does
not prohibit the solver from continuing to execute.
The exception RecoverableModalException is thrown by
the SMTEngine and the commands catch it and turn it
into a CommandRecoverableFailure. The commit changes
all error conditions from the commit above and adds a
regression test for them.

1 files changed, 3 insertions, 0 deletions

diff --git a/src/proof/unsat_core.cpp b/src/proof/unsat_core.cpp
index b056e0ef4..c8696868e 100644
--- a/src/proof/unsat_core.cpp
+++ b/src/proof/unsat_core.cpp
@@ -16,6 +16,7 @@
 
 #include "proof/unsat_core.h"
 
+#include "base/cvc4_assert.h"
 #include "expr/expr_iomanip.h"
 #include "options/base_options.h"
 #include "printer/printer.h"
@@ -37,12 +38,14 @@ UnsatCore::const_iterator UnsatCore::end() const {
 }
 
 void UnsatCore::toStream(std::ostream& out) const {
+  Assert(d_smt != NULL);
   smt::SmtScope smts(d_smt);
   expr::ExprDag::Scope scope(out, false);
   Printer::getPrinter(options::outputLanguage())->toStream(out, *this);
 }
 
 void UnsatCore::toStream(std::ostream& out, const std::map<Expr, std::string>& names) const {
+  Assert(d_smt != NULL);
   smt::SmtScope smts(d_smt);
   expr::ExprDag::Scope scope(out, false);
   Printer::getPrinter(options::outputLanguage())->toStream(out, *this, names);