#407: remove the solver-specific Z3SolverException.

The specific exception does not bring any benefit over a default SolverException.

Author: kfriedberger

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);
       }
     }
   }

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, SolverException {
     Preconditions.checkState(!closed);
     int status;
     try {
@@ -132,7 +132,7 @@ protected long getUnsatCore0() {
   }
 
   @Override
-  public boolean isUnsat() throws Z3SolverException, InterruptedException {
+  public boolean isUnsat() throws SolverException, InterruptedException {
     Preconditions.checkState(!closed);
     logSolverStack();
     return check() == OptStatus.UNSAT;

src/org/sosy_lab/java_smt/solvers/z3/Z3SolverException.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 SolverException, InterruptedException {
     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 SolverException, InterruptedException {
     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);
       }
     }
   }