handle crashes inside TraceCheck s.t. refinement engine can suppress them

Author: danieldietsch

trunk/source/Library-TraceCheckerUtils/src/de/uni_freiburg/informatik/ultimate/lib/tracecheckerutils/singletracecheck/TraceCheck.java

@@ -138,7 +138,6 @@ public class TraceCheck<LETTER extends IAction> implements ITraceCheck {
 	protected NestedSsaBuilder mNsb;
 	protected final TraceCheckStatisticsGenerator mTraceCheckBenchmarkGenerator;
 	protected final AssertCodeBlockOrder mAssertCodeBlocksIncrementally;
-	protected ToolchainCanceledException mToolchainCanceledException;
 	protected final IIcfgSymbolTable mBoogie2SmtSymbolTable;
 	protected final FeasibilityCheckResult mFeasibilityResult;
 
@@ -243,8 +242,16 @@ protected TraceCheck(final IPredicate precondition, final IPredicate postconditi
 					}
 				}
 			}
-		} catch (final ToolchainCanceledException tce) {
-			mToolchainCanceledException = tce;
+		} catch (final ToolchainCanceledException e) {
+			feasibilityResult = new FeasibilityCheckResult(LBool.UNKNOWN,
+					new TraceCheckReasonUnknown(Reason.ULTIMATE_TIMEOUT, e, ExceptionHandlingCategory.KNOWN_THROW),
+					false);
+		} catch (final SMTLIBException e) {
+			feasibilityResult =
+					new FeasibilityCheckResult(LBool.UNKNOWN, TraceCheckReasonUnknown.constructReasonUnknown(e), true);
+		} catch (final Exception e) {
+			feasibilityResult = new FeasibilityCheckResult(LBool.UNKNOWN,
+					new TraceCheckReasonUnknown(Reason.SOLVER_CRASH_OTHER, e, ExceptionHandlingCategory.UNKNOWN), true);
 		} finally {
 			mFeasibilityResult = feasibilityResult;
 			mProvidesIcfgProgramExecution = providesIcfgProgramExecution;
@@ -448,7 +455,7 @@ public IcfgProgramExecution getRcfgProgramExecution() {
 
 	@Override
 	public TraceCheckStatisticsGenerator getStatistics() {
-		if (mTraceCheckFinished || mToolchainCanceledException != null) {
+		if (mTraceCheckFinished) {
 			return mTraceCheckBenchmarkGenerator;
 		}
 		return null;

trunk/source/Library-TraceCheckerUtils/src/de/uni_freiburg/informatik/ultimate/lib/tracecheckerutils/singletracecheck/TraceCheckSpWp.java

@@ -159,8 +159,17 @@ public TraceCheckSpWp(final IPredicate precondition, final IPredicate postcondit
 		}
 		final LBool result = isCorrect();
 		if (result == LBool.UNSAT) {
-			computeInterpolants(new AllIntegers(), interpolation);
-			mInterpolantComputationStatus = new InterpolantComputationStatus();
+			InterpolantComputationStatus actualInterpolationComputationStatus = null;
+			try {
+				computeInterpolants(new AllIntegers(), interpolation);
+				actualInterpolationComputationStatus = new InterpolantComputationStatus();
+			} catch (final ToolchainCanceledException ex) {
+				throw ex;
+			} catch (final Throwable ex) {
+				actualInterpolationComputationStatus =
+						new InterpolantComputationStatus(ItpErrorStatus.SMT_SOLVER_CRASH, ex);
+			}
+			mInterpolantComputationStatus = actualInterpolationComputationStatus;
 		} else if (result == LBool.SAT) {
 			mInterpolantComputationStatus = new InterpolantComputationStatus(ItpErrorStatus.TRACE_FEASIBLE, null);
 		} else {