Fix issue #1074, improve non-fatal error handling (#1075)
authorAndres Noetzli <andres.noetzli@gmail.com>
Tue, 19 Sep 2017 16:43:58 +0000 (09:43 -0700)
committerGitHub <noreply@github.com>
Tue, 19 Sep 2017 16:43:58 +0000 (09:43 -0700)
commit4983832f0e72d1e1a01654a1f5c2d270d3db8602
treee963bf5c5044ca286b745624e239bbf8f990fe23
parent324eafcb6d243312e366009d140758c40527db54
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.
src/base/modal_exception.h
src/printer/smt2/smt2_printer.cpp
src/proof/unsat_core.cpp
src/smt/command.cpp
src/smt/command.h
src/smt/smt_engine.cpp
test/regress/regress0/Makefile.am
test/regress/regress0/non-fatal-errors.smt2 [new file with mode: 0644]
test/regress/run_regression