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.

3 files changed, 41 insertions, 1 deletions

diff --git a/test/regress/regress0/Makefile.am b/test/regress/regress0/Makefile.am
index 1368dd067..dbff6cff1 100644
--- a/test/regress/regress0/Makefile.am
+++ b/test/regress/regress0/Makefile.am
@@ -69,7 +69,8 @@ SMT2_TESTS = \
 	hung10_itesdk_output1.smt2 \
 	hung13sdk_output2.smt2 \
 	declare-funs.smt2 \
-	declare-fun-is-match.smt2
+	declare-fun-is-match.smt2 \
+	non-fatal-errors.smt2
 
 # Regression tests for PL inputs
 CVC_TESTS = \
diff --git a/test/regress/regress0/non-fatal-errors.smt2 b/test/regress/regress0/non-fatal-errors.smt2
new file mode 100644
index 000000000..1e1865883
--- /dev/null
+++ b/test/regress/regress0/non-fatal-errors.smt2
@@ -0,0 +1,29 @@
+; SCRUBBER: sed 's/".*"/""/g'
+; EXPECT: success
+; EXPECT: success
+; EXPECT: success
+; EXPECT: success
+; EXPECT: success
+; EXPECT: success
+; EXPECT: success
+; EXPECT: (error "")
+; EXPECT: (error "")
+; EXPECT: (error "")
+; EXPECT: (error "")
+; EXPECT: (error "")
+; EXPECT: success
+; EXPECT: sat
+(set-option :print-success true)
+(set-option :produce-unsat-cores true)
+(set-option :produce-models true)
+(set-option :produce-proofs true)
+(set-option :produce-assignments true)
+(set-logic UF)
+(declare-fun p () Bool)
+(get-unsat-core)
+(get-value (p))
+(get-proof)
+(get-model)
+(get-assignment)
+(assert true)
+(check-sat)
diff --git a/test/regress/run_regression b/test/regress/run_regression
index 536a3e8a5..5d4165597 100755
--- a/test/regress/run_regression
+++ b/test/regress/run_regression
@@ -130,6 +130,15 @@ if expr "$benchmark" : '.*\.smt$' &>/dev/null; then
   fi
 elif expr "$benchmark" : '.*\.smt2$' &>/dev/null; then
   lang=smt2
+
+  # If this test case requires unsat cores but CVC4 is not built with proof
+  # support, skip it. Note: checking $CVC4_REGRESSION_ARGS instead of $proof
+  # here because $proof is not set for the second run.
+  requires_proof=`grep '(get-unsat-core)' "$benchmark"`
+  if [[ ! "$CVC4_REGRESSION_ARGS" = *"--proof"* ]] && [ -n "$requires_proof" ]; then
+    exit 77
+  fi
+
   if test -e "$benchmark.expect"; then
     scrubber=`grep '^% SCRUBBER: ' "$benchmark.expect" | sed 's,^% SCRUBBER: ,,'`
     errscrubber=`grep '^% ERROR-SCRUBBER: ' "$benchmark.expect" | sed 's,^% ERROR-SCRUBBER: ,,'`
@@ -288,6 +297,7 @@ if [ "$proof" = yes ]; then
     fi
   fi
 fi
+
 if [ -z "$expected_error" ]; then
   # in case expected stderr output is empty, make sure we don't differ
   # by a newline, which we would if we echo "" >"$experrfile"