Update SMTInterpol and add new theories

lib/ivy.xml

@@ -169,7 +169,7 @@ SPDX-License-Identifier: Apache-2.0
         <dependency org="com.puppycrawl.tools" name="checkstyle" rev="11.0.1" conf="checkstyle->default"/>
 
         <!-- SmtInterpol -->
-        <dependency org="de.uni-freiburg.informatik.ultimate" name="smtinterpol" rev="2.5-1242-g5c50fb6d" conf="runtime-smtinterpol->master; contrib->sources,javadoc"/>
+        <dependency org="de.uni-freiburg.informatik.ultimate" name="smtinterpol" rev="2.5-1388-ga5a4ab0c" conf="runtime-smtinterpol->master; contrib->sources,javadoc"/>
 
         <!-- Princess and Ostrich for our Maven release -->
         <dependency org="io.github.uuverifiers" name="princess_2.13" rev="2025-11-17" conf="runtime-princess-with-javacup->default; contrib->sources,javadoc"/>

src/org/sosy_lab/java_smt/solvers/smtinterpol/FormulaCollectionScript.java

@@ -10,6 +10,7 @@
 
 import static com.google.common.base.Preconditions.checkNotNull;
 
+import com.google.common.collect.FluentIterable;
 import de.uni_freiburg.informatik.ultimate.logic.Annotation;
 import de.uni_freiburg.informatik.ultimate.logic.ApplicationTerm;
 import de.uni_freiburg.informatik.ultimate.logic.Assignments;
@@ -28,6 +29,7 @@
 import java.math.BigDecimal;
 import java.math.BigInteger;
 import java.util.ArrayList;
+import java.util.Arrays;
 import java.util.Collections;
 import java.util.List;
 import java.util.Map;
@@ -70,33 +72,40 @@ public LBool assertTerm(Term pTerm) throws SMTLIBException {
 
   @Override
   public void declareFun(String fun, Sort[] paramSorts, Sort resultSort) throws SMTLIBException {
-    FunctionSymbol fsym = theory.getFunction(fun, paramSorts);
-
-    if (fsym == null) {
+    var functions = theory.getDeclaredFunctions();
+    if (!functions.containsKey(fun)) {
+      // There is no function with that name yet: create a new symbol
       script.declareFun(fun, paramSorts, resultSort);
     } else {
-      if (!fsym.getReturnSort().equals(resultSort)) {
+      // A symbol with the same name already exists: Check if the signature matches and throw an
+      // exception otherwise
+      var decl = functions.get(fun);
+      if (!Arrays.equals(decl.getParameterSorts(), paramSorts)
+          || !decl.getReturnSort().equals(resultSort)) {
         throw new SMTLIBException(
-            "Function " + fun + " is already declared with different definition");
+            "Function '%s' already declared with a different sort".formatted(fun));
       }
     }
   }
 
   @Override
   public void defineFun(String fun, TermVariable[] params, Sort resultSort, Term definition)
       throws SMTLIBException {
-    Sort[] paramSorts = new Sort[params.length];
-    for (int i = 0; i < paramSorts.length; i++) {
-      paramSorts[i] = params[i].getSort();
-    }
-    FunctionSymbol fsym = theory.getFunction(fun, paramSorts);
-
-    if (fsym == null) {
+    var functions = theory.getDeclaredFunctions();
+    if (!functions.containsKey(fun)) {
+      // There is no function with that name yet: create a new symbol
       script.defineFun(fun, params, resultSort, definition);
     } else {
-      if (!fsym.getDefinition().equals(definition) || !fsym.getReturnSort().equals(resultSort)) {
+      // A symbol with the same name already exists: Check if the signature and the definition
+      // match and throw an exception otherwise
+      var decl = functions.get(fun);
+      if (!Arrays.equals(
+              decl.getParameterSorts(),
+              FluentIterable.from(params).transform(TermVariable::getSort).toArray(Sort.class))
+          || !decl.getReturnSort().equals(resultSort)
+          || !decl.getDefinition().equals(definition)) {
         throw new SMTLIBException(
-            "Function " + fun + " is already defined with different definition");
+            "Function '%s' already declared with a different sort".formatted(fun));
       }
     }
   }

src/org/sosy_lab/java_smt/solvers/smtinterpol/LoggingSmtInterpolInterpolatingProver.java

@@ -90,7 +90,7 @@ public <R> R allSat(AllSatCallback<R> callback, List<BooleanFormula> predicates)
   }
 
   @Override
-  protected boolean isUnsatImpl() throws InterruptedException {
+  protected boolean isUnsatImpl() throws InterruptedException, SolverException {
     out.print("(check-sat)");
     boolean isUnsat = super.isUnsatImpl();
     out.println(" ; " + (isUnsat ? "UNSAT" : "SAT"));

src/org/sosy_lab/java_smt/solvers/smtinterpol/SmtInterpolAbstractProver.java

@@ -106,7 +106,7 @@ protected String addConstraint0(BooleanFormula constraint) {
   }
 
   @Override
-  protected boolean isUnsatImpl() throws InterruptedException {
+  protected boolean isUnsatImpl() throws InterruptedException, SolverException {
     // We actually terminate SmtInterpol during the analysis
     // by using a shutdown listener. However, SmtInterpol resets the
     // mStopEngine flag in DPLLEngine before starting to solve,
@@ -118,21 +118,13 @@ protected boolean isUnsatImpl() throws InterruptedException {
       case SAT -> false;
       case UNSAT -> true;
       case UNKNOWN -> {
-        Object reason = env.getInfo(":reason-unknown");
-        if (!(reason instanceof ReasonUnknown unknown)) {
-          throw new SMTLIBException("checkSat returned UNKNOWN with unknown reason " + reason);
-        }
-        switch (unknown) {
-          case MEMOUT ->
-              // SMTInterpol catches OOM, but we want to have it thrown.
-              throw new OutOfMemoryError("Out of memory during SMTInterpol operation");
-          case CANCELLED -> {
-            shutdownNotifier.shutdownIfNecessary(); // expected if we requested termination
-            throw new SMTLIBException("checkSat returned UNKNOWN with unexpected reason " + reason);
-          }
-          default ->
-              throw new SMTLIBException(
-                  "checkSat returned UNKNOWN with unexpected reason " + reason);
+        var reason = (ReasonUnknown) env.getInfo(":reason-unknown");
+        switch (reason) {
+          case MEMOUT -> throw new OutOfMemoryError();
+          case INCOMPLETE ->
+              throw new SolverException("Incomplete theory, could not decide satisfiability");
+          case CANCELLED -> throw new InterruptedException();
+          default -> throw new RuntimeException("Unknown solver error");
         }
       }
     };

src/org/sosy_lab/java_smt/solvers/smtinterpol/SmtInterpolBitvectorFormulaManager.java

@@ -0,0 +1,197 @@
+/*
+ * This file is part of JavaSMT,
+ * an API wrapper for a collection of SMT solvers:
+ * https://github.com/sosy-lab/java-smt
+ *
+ * SPDX-FileCopyrightText: 2026 Dirk Beyer <https://www.sosy-lab.org>
+ *
+ * SPDX-License-Identifier: Apache-2.0
+ */
+
+package org.sosy_lab.java_smt.solvers.smtinterpol;
+
+import static com.google.common.base.Preconditions.checkArgument;
+
+import de.uni_freiburg.informatik.ultimate.logic.FunctionSymbol;
+import de.uni_freiburg.informatik.ultimate.logic.Script;
+import de.uni_freiburg.informatik.ultimate.logic.Sort;
+import de.uni_freiburg.informatik.ultimate.logic.Term;
+import java.math.BigInteger;
+import org.sosy_lab.java_smt.basicimpl.AbstractBitvectorFormulaManager;
+import org.sosy_lab.java_smt.basicimpl.AbstractBooleanFormulaManager;
+import org.sosy_lab.java_smt.basicimpl.FormulaCreator;
+
+public class SmtInterpolBitvectorFormulaManager
+    extends AbstractBitvectorFormulaManager<Term, Sort, Script, FunctionSymbol> {
+  protected SmtInterpolBitvectorFormulaManager(
+      FormulaCreator<Term, Sort, Script, FunctionSymbol> pCreator,
+      AbstractBooleanFormulaManager<Term, Sort, Script, FunctionSymbol> pBmgr) {
+    super(pCreator, pBmgr);
+  }
+
+  @Override
+  protected Term makeBitvectorImpl(int length, Term pParam1) {
+    return getFormulaCreator()
+        .getEnv()
+        .term("int_to_bv", new String[] {String.valueOf(length)}, null, pParam1);
+  }
+
+  @Override
+  protected Term toIntegerFormulaImpl(Term pI, boolean signed) {
+    return getFormulaCreator().getEnv().term(signed ? "sbv_to_int" : "ubv_to_int", pI);
+  }
+
+  @Override
+  protected Term negate(Term pParam1) {
+    return getFormulaCreator().getEnv().term("bvneg", pParam1);
+  }
+
+  @Override
+  protected Term add(Term pParam1, Term pParam2) {
+    return getFormulaCreator().getEnv().term("bvadd", pParam1, pParam2);
+  }
+
+  @Override
+  protected Term subtract(Term pParam1, Term pParam2) {
+    return getFormulaCreator().getEnv().term("bvsub", pParam1, pParam2);
+  }
+
+  @Override
+  protected Term divide(Term pParam1, Term pParam2, boolean signed) {
+    return getFormulaCreator().getEnv().term(signed ? "bvsdiv" : "bvudiv", pParam1, pParam2);
+  }
+
+  @Override
+  protected Term remainder(Term pParam1, Term pParam2, boolean signed) {
+    return getFormulaCreator().getEnv().term(signed ? "bvsrem" : "bvurem", pParam1, pParam2);
+  }
+
+  @Override
+  protected Term smodulo(Term pParam1, Term pParam2) {
+    return getFormulaCreator().getEnv().term("bvsmod", pParam1, pParam2);
+  }
+
+  @Override
+  protected Term multiply(Term pParam1, Term pParam2) {
+    return getFormulaCreator().getEnv().term("bvmul", pParam1, pParam2);
+  }
+
+  @Override
+  protected Term equal(Term pParam1, Term pParam2) {
+    return getFormulaCreator().getEnv().term("=", pParam1, pParam2);
+  }
+
+  @Override
+  protected Term greaterThan(Term pParam1, Term pParam2, boolean signed) {
+    return getFormulaCreator().getEnv().term(signed ? "bvsgt" : "bvugt", pParam1, pParam2);
+  }
+
+  @Override
+  protected Term greaterOrEquals(Term pParam1, Term pParam2, boolean signed) {
+    return getFormulaCreator().getEnv().term(signed ? "bvsge" : "bvuge", pParam1, pParam2);
+  }
+
+  @Override
+  protected Term lessThan(Term pParam1, Term pParam2, boolean signed) {
+    return getFormulaCreator().getEnv().term(signed ? "bvslt" : "bvult", pParam1, pParam2);
+  }
+
+  @Override
+  protected Term lessOrEquals(Term pParam1, Term pParam2, boolean signed) {
+    return getFormulaCreator().getEnv().term(signed ? "bvsle" : "bvule", pParam1, pParam2);
+  }
+
+  @Override
+  protected Term not(Term pParam1) {
+    return getFormulaCreator().getEnv().term("bvnot", pParam1);
+  }
+
+  @Override
+  protected Term and(Term pParam1, Term pParam2) {
+    return getFormulaCreator().getEnv().term("bvand", pParam1, pParam2);
+  }
+
+  @Override
+  protected Term or(Term pParam1, Term pParam2) {
+    return getFormulaCreator().getEnv().term("bvor", pParam1, pParam2);
+  }
+
+  @Override
+  protected Term xor(Term pParam1, Term pParam2) {
+    return getFormulaCreator().getEnv().term("bvxor", pParam1, pParam2);
+  }
+
+  @Override
+  protected Term makeBitvectorImpl(int pLength, BigInteger pI) {
+    var raw = pI;
+    if (pI.signum() < 0) {
+      var positive = pI.negate();
+      var value = BigInteger.ZERO;
+      for (var p = 0; p < Math.max(pLength, pI.bitLength() + 1); p++) {
+        if (p < positive.bitLength()) {
+          value = !positive.testBit(p) ? value.setBit(p) : value;
+        } else {
+          value = value.setBit(p);
+        }
+      }
+      raw = value.add(BigInteger.ONE);
+    }
+    checkArgument(raw.bitLength() <= pLength);
+    return getFormulaCreator()
+        .getEnv()
+        .getTheory()
+        .constant(raw, formulaCreator.getBitvectorType(pLength));
+  }
+
+  @Override
+  protected Term makeVariableImpl(int pLength, String pVar) {
+    return getFormulaCreator().makeVariable(getFormulaCreator().getBitvectorType(pLength), pVar);
+  }
+
+  @Override
+  protected Term shiftRight(Term pNumber, Term toShift, boolean signed) {
+    return getFormulaCreator().getEnv().term(signed ? "bvashr" : "bvlshr", pNumber, toShift);
+  }
+
+  @Override
+  protected Term shiftLeft(Term pNumber, Term pToShift) {
+    return getFormulaCreator().getEnv().term("bvshl", pNumber, pToShift);
+  }
+
+  @Override
+  protected Term rotateRightByConstant(Term pNumber, int pToRotate) {
+    return getFormulaCreator()
+        .getEnv()
+        .term("rotate_right", new String[] {String.valueOf(pToRotate)}, null, pNumber);
+  }
+
+  @Override
+  protected Term rotateLeftByConstant(Term pNumber, int pToRotate) {
+    return getFormulaCreator()
+        .getEnv()
+        .term("rotate_left", new String[] {String.valueOf(pToRotate)}, null, pNumber);
+  }
+
+  @Override
+  protected Term concat(Term number, Term pAppend) {
+    return getFormulaCreator().getEnv().term("concat", number, pAppend);
+  }
+
+  @Override
+  protected Term extract(Term pNumber, int pMsb, int pLsb) {
+    return getFormulaCreator()
+        .getEnv()
+        .term("extract", new String[] {String.valueOf(pMsb), String.valueOf(pLsb)}, null, pNumber);
+  }
+
+  @Override
+  protected Term extend(Term pNumber, int pExtensionBits, boolean pSigned) {
+    return getFormulaCreator()
+        .getEnv()
+        .term(
+            pSigned ? "sign_extend" : "zero_extend",
+            new String[] {String.valueOf(pExtensionBits)},
+            null,
+            pNumber);
+  }
+}