Throw SolverException when interpolation fails

src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaInterpolatingProver.java

@@ -17,6 +17,7 @@
 import java.util.Collection;
 import java.util.List;
 import java.util.Set;
+import java.util.function.Function;
 import org.checkerframework.checker.nullness.qual.Nullable;
 import org.sosy_lab.common.ShutdownNotifier;
 import org.sosy_lab.java_smt.api.BooleanFormula;
@@ -52,13 +53,27 @@ private static Options enableInterpolation(Options pSolverOptions) {
     return addConstraint0(constraint);
   }
 
+  /** Catches interpolation errors and throws a {@link SolverException}. */
+  private <A, B> B callWithError(Function<A, B> f, A args) throws SolverException {
+    try {
+      return f.apply(args);
+    } catch (IllegalArgumentException e) {
+      if (e.getMessage().endsWith("not supported")) {
+        throw new SolverException(e.getMessage());
+      } else {
+        throw e;
+      }
+    }
+  }
+
   @Override
   public BooleanFormula getInterpolant(Collection<Integer> formulasOfA)
       throws SolverException, InterruptedException {
     return creator.encapsulateBoolean(
         formulasOfA.isEmpty()
             ? creator.getEnv().mk_true()
-            : env.get_interpolant(
+            : callWithError(
+                env::get_interpolant,
                 new Vector_Term(FluentIterable.from(formulasOfA).transform(stack.peek()::get))));
   }
 
@@ -72,7 +87,7 @@ public List<BooleanFormula> getSeqInterpolants(
             FluentIterable.from(partitionedFormulas)
                 .transform(
                     p -> new Vector_Term(FluentIterable.from(p).transform(stack.peek()::get))));
-    Vector_Term itps = env.get_interpolants(partitions);
+    Vector_Term itps = callWithError(env::get_interpolants, partitions);
     checkState(
         creator.getEnv().mk_false().equals(Iterables.getLast(itps)),
         "the last interpolant should be false");

src/org/sosy_lab/java_smt/solvers/opensmt/OpenSmtAbstractProver.java

@@ -117,7 +117,7 @@ protected T addConstraintImpl(BooleanFormula pF) throws InterruptedException {
 
   @SuppressWarnings("resource")
   @Override
-  protected Model getModelImpl() {
+  protected Model getModelImpl() throws SolverException {
     return registerEvaluator(
         new OpenSmtModel(
             this, creator, Collections2.transform(getAssertedFormulas(), creator::extractInfo)));

src/org/sosy_lab/java_smt/solvers/opensmt/OpenSmtInterpolatingProver.java

@@ -19,6 +19,7 @@
 import org.sosy_lab.java_smt.api.FormulaManager;
 import org.sosy_lab.java_smt.api.InterpolatingProverEnvironment;
 import org.sosy_lab.java_smt.api.SolverContext.ProverOptions;
+import org.sosy_lab.java_smt.api.SolverException;
 import org.sosy_lab.java_smt.solvers.opensmt.OpenSmtSolverContext.OpenSMTOptions;
 import org.sosy_lab.java_smt.solvers.opensmt.api.PTRef;
 import org.sosy_lab.java_smt.solvers.opensmt.api.VectorInt;
@@ -69,14 +70,25 @@ protected void popImpl() {
   }
 
   @Override
-  public BooleanFormula getInterpolant(Collection<Integer> formulasOfA) {
+  public BooleanFormula getInterpolant(Collection<Integer> formulasOfA) throws SolverException {
+    if (!creator.getLogic().doesLogicSupportInterpolation()) {
+      throw new SolverException(
+          "OpenSMT does not support interpolation for the specified logic %s."
+              .formatted(creator.getLogic()));
+    }
     return creator.encapsulateBoolean(
         osmtSolver.getInterpolationContext().getSingleInterpolant(new VectorInt(formulasOfA)));
   }
 
   @Override
   public List<BooleanFormula> getSeqInterpolants(
-      List<? extends Collection<Integer>> partitionedFormulas) {
+      List<? extends Collection<Integer>> partitionedFormulas) throws SolverException {
+    if (!creator.getLogic().doesLogicSupportInterpolation()) {
+      throw new SolverException(
+          "OpenSMT does not support interpolation for the specified logic %s."
+              .formatted(creator.getLogic()));
+    }
+
     VectorVectorInt partitions = new VectorVectorInt();
     for (int i = 1; i < partitionedFormulas.size(); i++) {
       VectorInt prefix = new VectorInt();

src/org/sosy_lab/java_smt/solvers/opensmt/OpenSmtModel.java

@@ -18,6 +18,7 @@
 import java.util.LinkedHashMap;
 import java.util.List;
 import java.util.Map;
+import org.sosy_lab.java_smt.api.SolverException;
 import org.sosy_lab.java_smt.basicimpl.AbstractModel;
 import org.sosy_lab.java_smt.solvers.opensmt.api.Logic;
 import org.sosy_lab.java_smt.solvers.opensmt.api.Model;
@@ -38,7 +39,8 @@ class OpenSmtModel extends AbstractModel<PTRef, SRef, Logic> {
   OpenSmtModel(
       OpenSmtAbstractProver<?> pProver,
       OpenSmtFormulaCreator pCreator,
-      Collection<PTRef> pAssertedTerms) {
+      Collection<PTRef> pAssertedTerms)
+      throws SolverException {
     super(pProver, pCreator);
 
     osmtLogic = pCreator.getEnv();
@@ -51,7 +53,7 @@ class OpenSmtModel extends AbstractModel<PTRef, SRef, Logic> {
   }
 
   private ImmutableList<ValueAssignment> generateModel(
-      OpenSmtFormulaCreator pCreator, Collection<PTRef> pAssertedTerms) {
+      OpenSmtFormulaCreator pCreator, Collection<PTRef> pAssertedTerms) throws SolverException {
     Map<String, PTRef> userDeclarations = new LinkedHashMap<>();
     for (PTRef asserted : pAssertedTerms) {
       userDeclarations.putAll(creator.extractVariablesAndUFs(asserted, true));
@@ -69,8 +71,7 @@ private ImmutableList<ValueAssignment> generateModel(
       if (osmtLogic.isArraySort(sort)) {
         // INFO: Disable model generation if arrays are used
         // https://github.com/usi-verification-and-security/opensmt/issues/630
-        throw new UnsupportedOperationException(
-            "OpenSMT does not support model generation when arrays are used");
+        throw new SolverException("OpenSMT does not support model generation when arrays are used");
       }
 
       if (numArgs == 0) {

src/org/sosy_lab/java_smt/solvers/yices2/Yices2InterpolatingProver.java

@@ -19,6 +19,7 @@
 import com.sri.yices.InterpolationContext;
 import com.sri.yices.Status;
 import com.sri.yices.Terms;
+import com.sri.yices.YicesException;
 import java.util.ArrayList;
 import java.util.Collection;
 import java.util.List;
@@ -61,7 +62,7 @@ public BooleanFormula getInterpolant(Collection<Integer> formulasOfA)
   }
 
   private int interpolate(Collection<Integer> setA, Collection<Integer> setB)
-      throws InterruptedException {
+      throws InterruptedException, SolverException {
     try (var ctxA = newContext("mcsat");
         var ctxB = newContext("mcsat")) {
 
@@ -72,12 +73,24 @@ private int interpolate(Collection<Integer> setA, Collection<Integer> setB)
       // TODO How to abort this?
       // For now, let's just check before and after the call:
       shutdownNotifier.shutdownIfNecessary();
-      var status = context.check(DEFAULT_PARAMS, false);
+      Status status;
+      try {
+        status = context.check(DEFAULT_PARAMS, false);
+      } catch (YicesException e) {
+        if (ImmutableSet.of(
+                "mcsat: unsupported theory\n",
+                "mcsat: assumption variable has a type that mcsat cannot decide on\n")
+            .contains(e.getMessage())) {
+          throw new SolverException(e.getMessage().stripTrailing());
+        } else {
+          throw e;
+        }
+      }
       shutdownNotifier.shutdownIfNecessary();
       if (status == Status.UNSAT) {
         return context.getInterpolant();
       } else {
-        throw new IllegalArgumentException("Solver state must be unsat");
+        throw new IllegalStateException("Solver state must be unsat");
       }
     }
   }