Z3: handle exceptions from Z3 in a few more places.

src/org/sosy_lab/java_smt/solvers/z3/Z3AbstractProver.java

@@ -89,15 +89,15 @@ void addParameter(long z3params, String key, Object value) {
   }
 
   /** dump the current solver stack into a new SMTLIB file. */
-  protected void logSolverStack() throws Z3SolverException {
+  protected void logSolverStack() throws SolverException {
     if (logfile != null) { // if logging is not disabled
       try {
         // write stack content to logfile
         Path filename = logfile.getFreshPath();
         MoreFiles.createParentDirectories(filename);
         Files.writeString(filename, this + "(check-sat)\n");
       } catch (IOException e) {
-        throw new Z3SolverException("Cannot write Z3 log file: " + e.getMessage());
+        throw new SolverException("Cannot write Z3 log file: " + e.getMessage());
       }
     }
   }

src/org/sosy_lab/java_smt/solvers/z3/Z3FormulaCreator.java

@@ -23,6 +23,7 @@
 import com.microsoft.z3.enumerations.Z3_decl_kind;
 import com.microsoft.z3.enumerations.Z3_sort_kind;
 import com.microsoft.z3.enumerations.Z3_symbol_kind;
+import edu.umd.cs.findbugs.annotations.SuppressFBWarnings;
 import java.lang.ref.PhantomReference;
 import java.lang.ref.ReferenceQueue;
 import java.math.BigInteger;
@@ -157,11 +158,38 @@ class Z3FormulaCreator extends FormulaCreator<Long, Long, Long, Long> {
     }
   }
 
-  final Z3Exception handleZ3Exception(Z3Exception e) throws Z3Exception, InterruptedException {
+  /**
+   * Utility helper method to hide a checked exception as unchecked exception.
+   *
+   * <p>The generic E simulates a generic (unchecked) Exception at compile time and lets us throw
+   * the correct (checked) Exception at run time.
+   */
+  @SuppressWarnings("unchecked")
+  @SuppressFBWarnings("THROWS_METHOD_THROWS_CLAUSE_THROWABLE")
+  private static <E extends Throwable> void throwCheckedAsUnchecked(Throwable e) throws E {
+    throw (E) e;
+  }
+
+  /**
+   * This method throws an {@link InterruptedException} if Z3 was interrupted by a shutdown hook.
+   * Otherwise, the given exception is thrown.
+   *
+   * <p>We handle Z3Exceptions in several places, including usage in Java interfaces like
+   * Iterable/Iterator, where checked exceptions can not be specified. This method signature does
+   * not specify a checked exception like {@link InterruptedException} to be thrown.
+   *
+   * @return actually nothing, because an exception is thrown.
+   */
+  final Z3Exception handleZ3Exception(Z3Exception e) {
     if (Z3_INTERRUPT_ERRORS.contains(e.getMessage())) {
-      shutdownNotifier.shutdownIfNecessary();
+      try {
+        shutdownNotifier.shutdownIfNecessary();
+      } catch (InterruptedException interrupt) {
+        throwCheckedAsUnchecked(interrupt);
+      }
     }
-    throw e;
+    throwCheckedAsUnchecked(new SolverException("Z3 has thrown an exception", e));
+    throw new AssertionError("unreachable code"); // we throw something before this line
   }
 
   @Override
@@ -995,10 +1023,9 @@ static boolean isOP(long z3context, long expr, Z3_decl_kind op) {
    * Apply multiple tactics in sequence.
    *
    * @throws InterruptedException thrown by JNI code in case of termination request
-   * @throws SolverException thrown by JNI code in case of error
    */
   public long applyTactics(long z3context, final Long pF, String... pTactics)
-      throws InterruptedException, SolverException {
+      throws InterruptedException {
     long overallResult = pF;
     for (String tactic : pTactics) {
       overallResult = applyTactic(z3context, overallResult, tactic);

src/org/sosy_lab/java_smt/solvers/z3/Z3Model.java

@@ -13,6 +13,7 @@
 import com.google.common.collect.ImmutableList;
 import com.microsoft.z3.Native;
 import com.microsoft.z3.Native.LongPtr;
+import com.microsoft.z3.Z3Exception;
 import com.microsoft.z3.enumerations.Z3_decl_kind;
 import com.microsoft.z3.enumerations.Z3_sort_kind;
 import java.util.ArrayList;
@@ -21,6 +22,7 @@
 import java.util.List;
 import java.util.Set;
 import java.util.regex.Pattern;
+import org.checkerframework.checker.nullness.qual.Nullable;
 import org.sosy_lab.java_smt.basicimpl.AbstractModel;
 import org.sosy_lab.java_smt.basicimpl.AbstractProver;
 
@@ -45,23 +47,29 @@ public ImmutableList<ValueAssignment> asList() {
     Preconditions.checkState(!isClosed());
     ImmutableList.Builder<ValueAssignment> out = ImmutableList.builder();
 
-    // Iterate through constants.
-    for (int constIdx = 0; constIdx < Native.modelGetNumConsts(z3context, model); constIdx++) {
-      long keyDecl = Native.modelGetConstDecl(z3context, model, constIdx);
-      Native.incRef(z3context, keyDecl);
-      out.addAll(getConstAssignments(keyDecl));
-      Native.decRef(z3context, keyDecl);
-    }
+    try {
 
-    // Iterate through function applications.
-    for (int funcIdx = 0; funcIdx < Native.modelGetNumFuncs(z3context, model); funcIdx++) {
-      long funcDecl = Native.modelGetFuncDecl(z3context, model, funcIdx);
-      Native.incRef(z3context, funcDecl);
-      if (!isInternalSymbol(funcDecl)) {
-        String functionName = z3creator.symbolToString(Native.getDeclName(z3context, funcDecl));
-        out.addAll(getFunctionAssignments(funcDecl, funcDecl, functionName));
+      // Iterate through constants.
+      for (int constIdx = 0; constIdx < Native.modelGetNumConsts(z3context, model); constIdx++) {
+        long keyDecl = Native.modelGetConstDecl(z3context, model, constIdx);
+        Native.incRef(z3context, keyDecl);
+        out.addAll(getConstAssignments(keyDecl));
+        Native.decRef(z3context, keyDecl);
+      }
+
+      // Iterate through function applications.
+      for (int funcIdx = 0; funcIdx < Native.modelGetNumFuncs(z3context, model); funcIdx++) {
+        long funcDecl = Native.modelGetFuncDecl(z3context, model, funcIdx);
+        Native.incRef(z3context, funcDecl);
+        if (!isInternalSymbol(funcDecl)) {
+          String functionName = z3creator.symbolToString(Native.getDeclName(z3context, funcDecl));
+          out.addAll(getFunctionAssignments(funcDecl, funcDecl, functionName));
+        }
+        Native.decRef(z3context, funcDecl);
       }
-      Native.decRef(z3context, funcDecl);
+
+    } catch (Z3Exception exception) {
+      throw z3creator.handleZ3Exception(exception);
     }
 
     return out.build();
@@ -363,7 +371,11 @@ private ValueAssignment getFunctionAssignment(
   @Override
   public String toString() {
     Preconditions.checkState(!isClosed());
-    return Native.modelToString(z3context, model);
+    try {
+      return Native.modelToString(z3context, model);
+    } catch (Z3Exception exception) {
+      throw z3creator.handleZ3Exception(exception);
+    }
   }
 
   @Override
@@ -375,9 +387,14 @@ public void close() {
   }
 
   @Override
-  protected Long evalImpl(Long formula) {
+  protected @Nullable Long evalImpl(Long formula) {
     LongPtr resultPtr = new LongPtr();
-    boolean satisfiableModel = Native.modelEval(z3context, model, formula, false, resultPtr);
+    boolean satisfiableModel;
+    try {
+      satisfiableModel = Native.modelEval(z3context, model, formula, false, resultPtr);
+    } catch (Z3Exception exception) {
+      throw z3creator.handleZ3Exception(exception);
+    }
     Preconditions.checkState(satisfiableModel);
     if (resultPtr.value == 0) {
       // unknown evaluation

src/org/sosy_lab/java_smt/solvers/z3/Z3OptimizationProver.java

@@ -72,7 +72,7 @@ public int minimize(Formula objective) {
   }
 
   @Override
-  public OptStatus check() throws InterruptedException, Z3SolverException {
+  public OptStatus check() throws InterruptedException {
     Preconditions.checkState(!closed);
     int status;
     try {
@@ -132,7 +132,7 @@ protected long getUnsatCore0() {
   }
 
   @Override
-  public boolean isUnsat() throws Z3SolverException, InterruptedException {
+  public boolean isUnsat() throws InterruptedException, SolverException {
     Preconditions.checkState(!closed);
     logSolverStack();
     return check() == OptStatus.UNSAT;

src/org/sosy_lab/java_smt/solvers/z3/Z3TheoremProver.java

@@ -23,6 +23,7 @@
 import org.sosy_lab.java_smt.api.BooleanFormula;
 import org.sosy_lab.java_smt.api.ProverEnvironment;
 import org.sosy_lab.java_smt.api.SolverContext.ProverOptions;
+import org.sosy_lab.java_smt.api.SolverException;
 import org.sosy_lab.java_smt.api.UserPropagator;
 
 class Z3TheoremProver extends Z3AbstractProver implements ProverEnvironment {
@@ -82,7 +83,7 @@ protected void assertContraintAndTrack(long constraint, long symbol) {
   }
 
   @Override
-  public boolean isUnsat() throws Z3SolverException, InterruptedException {
+  public boolean isUnsat() throws InterruptedException, SolverException {
     Preconditions.checkState(!closed);
     logSolverStack();
     int result;
@@ -97,7 +98,7 @@ public boolean isUnsat() throws Z3SolverException, InterruptedException {
 
   @Override
   public boolean isUnsatWithAssumptions(Collection<BooleanFormula> assumptions)
-      throws Z3SolverException, InterruptedException {
+      throws InterruptedException, SolverException {
     Preconditions.checkState(!closed);
 
     int result;
@@ -116,7 +117,7 @@ public boolean isUnsatWithAssumptions(Collection<BooleanFormula> assumptions)
   }
 
   private void undefinedStatusToException(int solverStatus)
-      throws Z3SolverException, InterruptedException {
+      throws SolverException, InterruptedException {
     if (solverStatus == Z3_lbool.Z3_L_UNDEF.toInt()) {
       creator.shutdownNotifier.shutdownIfNecessary();
       final String reason = Native.solverGetReasonUnknown(z3context, z3solver);
@@ -126,7 +127,7 @@ private void undefinedStatusToException(int solverStatus)
         case "interrupted from keyboard": // see Z3: src/solver/check_sat_result.cpp
           throw new InterruptedException(reason);
         default:
-          throw new Z3SolverException("Solver returned 'unknown' status, reason: " + reason);
+          throw new SolverException("Z3 returned 'unknown' status, reason: " + reason);
       }
     }
   }