diff --git a/src/org/sosy_lab/java_smt/api/FunctionDeclaration.java b/src/org/sosy_lab/java_smt/api/FunctionDeclaration.java
index d697fddb34..873508bcf6 100644
--- a/src/org/sosy_lab/java_smt/api/FunctionDeclaration.java
+++ b/src/org/sosy_lab/java_smt/api/FunctionDeclaration.java
@@ -29,6 +29,11 @@ public interface FunctionDeclaration<E extends Formula> {
    */
   String getName();
 
+  /**
+   * @return List of indices for the function
+   */
+  ImmutableList<Integer> getIndices();
+
   /**
    * @return Sort of the function output.
    */
diff --git a/src/org/sosy_lab/java_smt/api/FunctionDeclarationKind.java b/src/org/sosy_lab/java_smt/api/FunctionDeclarationKind.java
index 8eef4d99ad..2a53b30eed 100644
--- a/src/org/sosy_lab/java_smt/api/FunctionDeclarationKind.java
+++ b/src/org/sosy_lab/java_smt/api/FunctionDeclarationKind.java
@@ -323,5 +323,147 @@ public enum FunctionDeclarationKind {
    * Solvers support a lot of different built-in theories. We enforce standardization only across a
    * small subset.
    */
-  OTHER
+  OTHER;
+
+  public static int getArity(FunctionDeclarationKind pKind) {
+    return switch (pKind) {
+      case AND,
+          OR,
+          IFF,
+          XOR,
+          IMPLIES,
+          DISTINCT,
+          SUB,
+          ADD,
+          DIV,
+          MUL,
+          LT,
+          LTE,
+          GT,
+          GTE,
+          EQ,
+          BV_CONCAT,
+          BV_OR,
+          BV_AND,
+          BV_XOR,
+          BV_SUB,
+          BV_ADD,
+          BV_MUL,
+          STR_CONCAT,
+          STR_LT,
+          STR_LE,
+          RE_CONCAT,
+          RE_DIFFERENCE,
+          RE_UNION,
+          RE_INTERSECT ->
+          -1;
+      case RE_NONE, SEP_NIL -> 0;
+      case INT_TO_BV,
+          NOT,
+          UMINUS,
+          EQ_ZERO,
+          GTE_ZERO,
+          FLOOR,
+          TO_REAL,
+          CONST,
+          BV_EXTRACT,
+          BV_SIGN_EXTENSION,
+          BV_ZERO_EXTENSION,
+          BV_NOT,
+          BV_NEG,
+          BV_ROTATE_LEFT_BY_INT,
+          BV_ROTATE_RIGHT_BY_INT,
+          UBV_TO_INT,
+          SBV_TO_INT,
+          FP_NEG,
+          FP_ABS,
+          FP_IS_NAN,
+          FP_IS_INF,
+          FP_IS_ZERO,
+          FP_IS_NEGATIVE,
+          FP_IS_SUBNORMAL,
+          FP_IS_NORMAL,
+          FP_AS_IEEEBV,
+          FP_FROM_IEEEBV,
+          RE_PLUS,
+          RE_STAR,
+          INT_TO_STR,
+          STR_FROM_CODE,
+          STR_TO_CODE,
+          STR_LENGTH,
+          STR_TO_INT,
+          STR_TO_RE,
+          RE_COMPLEMENT,
+          RE_OPTIONAL ->
+          1;
+      case SELECT,
+          MODULO,
+          BV_SDIV,
+          BV_UDIV,
+          BV_SREM,
+          BV_UREM,
+          BV_SMOD,
+          BV_ULT,
+          BV_SLT,
+          BV_ULE,
+          BV_SLE,
+          BV_UGT,
+          BV_SGT,
+          BV_UGE,
+          BV_SGE,
+          BV_SHL,
+          BV_LSHR,
+          BV_ASHR,
+          BV_ROTATE_LEFT,
+          BV_ROTATE_RIGHT,
+          BV_UCASTTO_FP,
+          BV_SCASTTO_FP,
+          FP_MAX,
+          FP_MIN,
+          FP_SQRT,
+          FP_REM,
+          FP_LT,
+          FP_LE,
+          FP_GE,
+          FP_GT,
+          FP_EQ,
+          FP_ROUND_TO_INTEGRAL,
+          FP_CASTTO_FP,
+          FP_CASTTO_SBV,
+          FP_CASTTO_UBV,
+          STR_CHAR_AT,
+          STR_CONTAINS,
+          STR_IN_RE,
+          STR_PREFIX,
+          STR_SUFFIX,
+          RE_RANGE,
+          SEP_PTO,
+          SEP_EMP,
+          SEP_STAR,
+          SEP_WAND ->
+          2;
+      case ITE,
+          STORE,
+          FP_SUB,
+          FP_ADD,
+          FP_DIV,
+          FP_MUL,
+          STR_INDEX_OF,
+          STR_REPLACE,
+          STR_REPLACE_ALL,
+          STR_SUBSTRING ->
+          3;
+      default ->
+          throw new IllegalArgumentException(String.format("Unsupported kind: \"%s\"", pKind));
+    };
+  }
+
+  public static int getNumIndices(FunctionDeclarationKind pKind) {
+    // TODO Add missing kinds
+    return switch (pKind) {
+      case BV_ROTATE_LEFT_BY_INT, BV_ROTATE_RIGHT_BY_INT, BV_SIGN_EXTENSION, BV_ZERO_EXTENSION -> 1;
+      case BV_EXTRACT -> 2;
+      default -> 0;
+    };
+  }
 }
diff --git a/src/org/sosy_lab/java_smt/basicimpl/FunctionDeclarationImpl.java b/src/org/sosy_lab/java_smt/basicimpl/FunctionDeclarationImpl.java
index e88a5598d3..4b2f29b0a1 100644
--- a/src/org/sosy_lab/java_smt/basicimpl/FunctionDeclarationImpl.java
+++ b/src/org/sosy_lab/java_smt/basicimpl/FunctionDeclarationImpl.java
@@ -23,6 +23,7 @@
 public record FunctionDeclarationImpl<F extends Formula, T>(
     FunctionDeclarationKind getKind,
     String getName,
+    ImmutableList<Integer> getIndices,
     FormulaType<F> getType,
     ImmutableList<FormulaType<?>> getArgumentTypes,
     T getSolverDeclaration)
@@ -31,6 +32,7 @@ public record FunctionDeclarationImpl<F extends Formula, T>(
   public FunctionDeclarationImpl {
     checkNotNull(getKind);
     checkNotNull(getName);
+    checkNotNull(getIndices);
     checkNotNull(getType);
     checkNotNull(getArgumentTypes);
     checkNotNull(getSolverDeclaration);
@@ -39,11 +41,26 @@ public record FunctionDeclarationImpl<F extends Formula, T>(
   public static <F extends Formula, T> FunctionDeclarationImpl<F, T> of(
       String name,
       FunctionDeclarationKind kind,
+      List<Integer> pIndices,
       List<FormulaType<?>> pArgumentTypes,
       FormulaType<F> pReturnType,
       T pDeclaration) {
     return new FunctionDeclarationImpl<>(
-        kind, name, pReturnType, ImmutableList.copyOf(pArgumentTypes), pDeclaration);
+        kind,
+        name,
+        ImmutableList.copyOf(pIndices),
+        pReturnType,
+        ImmutableList.copyOf(pArgumentTypes),
+        pDeclaration);
+  }
+
+  public static <F extends Formula, T> FunctionDeclaration<F> of(
+      String name,
+      FunctionDeclarationKind kind,
+      List<FormulaType<?>> pArgumentTypes,
+      FormulaType<F> pReturnType,
+      T pDeclaration) {
+    return of(name, kind, ImmutableList.of(), pArgumentTypes, pReturnType, pDeclaration);
   }
 
   @Override
diff --git a/src/org/sosy_lab/java_smt/delegate/trace/TraceFormulaManager.java b/src/org/sosy_lab/java_smt/delegate/trace/TraceFormulaManager.java
index 575d9f1f27..8031ab6f70 100644
--- a/src/org/sosy_lab/java_smt/delegate/trace/TraceFormulaManager.java
+++ b/src/org/sosy_lab/java_smt/delegate/trace/TraceFormulaManager.java
@@ -10,6 +10,7 @@
 
 package org.sosy_lab.java_smt.delegate.trace;
 
+import static com.google.common.base.Preconditions.checkArgument;
 import static org.sosy_lab.common.collect.Collections3.transformedImmutableListCopy;
 import static org.sosy_lab.common.collect.Collections3.transformedImmutableSetCopy;
 
@@ -270,138 +271,7 @@ public <T extends Formula> T makeVariable(FormulaType<T> formulaType, String nam
   }
 
   private <T extends Formula> int getArity(FunctionDeclaration<T> pDeclaration) {
-    return switch (pDeclaration.getKind()) {
-      case AND,
-          OR,
-          IFF,
-          XOR,
-          IMPLIES,
-          DISTINCT,
-          SUB,
-          ADD,
-          DIV,
-          MUL,
-          LT,
-          LTE,
-          GT,
-          GTE,
-          EQ,
-          BV_CONCAT,
-          BV_OR,
-          BV_AND,
-          BV_XOR,
-          BV_SUB,
-          BV_ADD,
-          BV_MUL,
-          STR_CONCAT,
-          STR_LT,
-          STR_LE,
-          RE_CONCAT,
-          RE_DIFFERENCE,
-          RE_UNION,
-          RE_INTERSECT ->
-          -1;
-      case RE_NONE, SEP_NIL -> 0;
-      case INT_TO_BV,
-          NOT,
-          UMINUS,
-          EQ_ZERO,
-          GTE_ZERO,
-          FLOOR,
-          TO_REAL,
-          CONST,
-          BV_EXTRACT,
-          BV_SIGN_EXTENSION,
-          BV_ZERO_EXTENSION,
-          BV_NOT,
-          BV_NEG,
-          BV_ROTATE_LEFT_BY_INT,
-          BV_ROTATE_RIGHT_BY_INT,
-          UBV_TO_INT,
-          SBV_TO_INT,
-          FP_NEG,
-          FP_ABS,
-          FP_IS_NAN,
-          FP_IS_INF,
-          FP_IS_ZERO,
-          FP_IS_NEGATIVE,
-          FP_IS_SUBNORMAL,
-          FP_IS_NORMAL,
-          FP_AS_IEEEBV,
-          FP_FROM_IEEEBV,
-          RE_PLUS,
-          RE_STAR,
-          INT_TO_STR,
-          STR_FROM_CODE,
-          STR_TO_CODE,
-          STR_LENGTH,
-          STR_TO_INT,
-          STR_TO_RE,
-          RE_COMPLEMENT,
-          RE_OPTIONAL ->
-          1;
-      case SELECT,
-          MODULO,
-          BV_SDIV,
-          BV_UDIV,
-          BV_SREM,
-          BV_UREM,
-          BV_SMOD,
-          BV_ULT,
-          BV_SLT,
-          BV_ULE,
-          BV_SLE,
-          BV_UGT,
-          BV_SGT,
-          BV_UGE,
-          BV_SGE,
-          BV_SHL,
-          BV_LSHR,
-          BV_ASHR,
-          BV_ROTATE_LEFT,
-          BV_ROTATE_RIGHT,
-          BV_UCASTTO_FP,
-          BV_SCASTTO_FP,
-          FP_MAX,
-          FP_MIN,
-          FP_SQRT,
-          FP_REM,
-          FP_LT,
-          FP_LE,
-          FP_GE,
-          FP_GT,
-          FP_EQ,
-          FP_ROUND_TO_INTEGRAL,
-          FP_CASTTO_FP,
-          FP_CASTTO_SBV,
-          FP_CASTTO_UBV,
-          STR_CHAR_AT,
-          STR_CONTAINS,
-          STR_IN_RE,
-          STR_PREFIX,
-          STR_SUFFIX,
-          RE_RANGE,
-          SEP_PTO,
-          SEP_EMP,
-          SEP_STAR,
-          SEP_WAND ->
-          2;
-      case ITE,
-          STORE,
-          FP_SUB,
-          FP_ADD,
-          FP_DIV,
-          FP_MUL,
-          STR_INDEX_OF,
-          STR_REPLACE,
-          STR_REPLACE_ALL,
-          STR_SUBSTRING ->
-          3;
-      default ->
-          throw new IllegalArgumentException(
-              "Unsupported kind: \"%s\" (%s)"
-                  .formatted(pDeclaration.getName(), pDeclaration.getKind()));
-    };
+    return FunctionDeclarationKind.getArity(pDeclaration.getKind());
   }
 
   @SuppressWarnings({"unchecked", "rawtypes"})
@@ -569,18 +439,44 @@ public <T extends Formula> T makeApplication(
             yield (T) getRationalFormulaManager().floor((NumeralFormula) args.get(0));
           }
         }
-        // FIXME Requires indexed functions
-        // case INT_TO_BV:
-        // case BV_EXTRACT:
+        case INT_TO_BV -> {
+          checkArgument(declaration.getIndices().size() == 1);
+          yield (T)
+              getBitvectorFormulaManager()
+                  .makeBitvector(declaration.getIndices().get(0), (IntegerFormula) args.get(0));
+        }
+        case BV_EXTRACT -> {
+          checkArgument(declaration.getIndices().size() == 2);
+          yield (T)
+              getBitvectorFormulaManager()
+                  .extract(
+                      (BitvectorFormula) args.get(0),
+                      declaration.getIndices().get(0),
+                      declaration.getIndices().get(1));
+        }
         case BV_CONCAT -> {
-          Preconditions.checkArgument(args.size() == 2);
+          checkArgument(!args.isEmpty(), "Expected at least one argument");
+          var concat = (T) args.get(0);
+          for (var p = 1; p < args.size(); p++) {
+            concat =
+                (T)
+                    getBitvectorFormulaManager()
+                        .concat((BitvectorFormula) concat, (BitvectorFormula) args.get(p));
+          }
+          yield concat;
+        }
+        case BV_SIGN_EXTENSION -> {
+          checkArgument(declaration.getIndices().size() == 1);
           yield (T)
               getBitvectorFormulaManager()
-                  .concat((BitvectorFormula) args.get(0), (BitvectorFormula) args.get(1));
+                  .extend((BitvectorFormula) args.get(0), declaration.getIndices().get(0), true);
+        }
+        case BV_ZERO_EXTENSION -> {
+          checkArgument(declaration.getIndices().size() == 1);
+          yield (T)
+              getBitvectorFormulaManager()
+                  .extend((BitvectorFormula) args.get(0), declaration.getIndices().get(0), false);
         }
-        // FIXME Requires indexed functions
-        // case BV_SIGN_EXTENSION:
-        // case BV_ZERO_EXTENSION:
         case BV_NOT -> (T) getBitvectorFormulaManager().not((BitvectorFormula) args.get(0));
         case BV_NEG -> (T) getBitvectorFormulaManager().negate((BitvectorFormula) args.get(0));
         case BV_OR -> {
@@ -708,9 +604,18 @@ public <T extends Formula> T makeApplication(
             (T)
                 getBitvectorFormulaManager()
                     .rotateRight((BitvectorFormula) args.get(0), (BitvectorFormula) args.get(1));
-        // FIXME Requires indexed functions
-        // case BV_ROTATE_LEFT_BY_INT:
-        // case BV_ROTATE_RIGHT_BY_INT:
+        case BV_ROTATE_LEFT_BY_INT -> {
+          checkArgument(declaration.getIndices().size() == 1);
+          yield (T)
+              getBitvectorFormulaManager()
+                  .rotateLeft((BitvectorFormula) args.get(0), declaration.getIndices().get(0));
+        }
+        case BV_ROTATE_RIGHT_BY_INT -> {
+          checkArgument(declaration.getIndices().size() == 1);
+          yield (T)
+              getBitvectorFormulaManager()
+                  .rotateRight((BitvectorFormula) args.get(0), declaration.getIndices().get(0));
+        }
         case BV_UCASTTO_FP ->
             (T)
                 getFloatingPointFormulaManager()
diff --git a/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaFormulaCreator.java b/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaFormulaCreator.java
index 0589b194d0..5998673f8b 100644
--- a/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaFormulaCreator.java
+++ b/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaFormulaCreator.java
@@ -489,7 +489,12 @@ public <R> R visit(FormulaVisitor<R> visitor, Formula formula, Term f)
           formula,
           arguments.build(),
           FunctionDeclarationImpl.of(
-              name, getDeclarationKind(f), argumentTypes.build(), getFormulaType(f), decl));
+              name,
+              getDeclarationKind(f),
+              ImmutableList.copyOf(f.indices()),
+              argumentTypes.build(),
+              getFormulaType(f),
+              decl));
     }
   }
 
diff --git a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FormulaCreator.java b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FormulaCreator.java
index c23fad5fc3..37a24a7c3f 100644
--- a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FormulaCreator.java
+++ b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FormulaCreator.java
@@ -456,6 +456,9 @@ public <R> R visit(FormulaVisitor<R> visitor, Formula formula, final Term f) {
       } else if (f.getKind() == Kind.CONSTANT) {
         return visitor.visitFreeVariable(formula, Tokenizer.dequote(f.toString()));
 
+      } else if (f.getKind() == Kind.SEP_NIL) {
+        return visitor.visitConstant(formula, null);
+
       } else if (f.getKind() == Kind.APPLY_CONSTRUCTOR) {
         checkState(
             f.getNumChildren() == 1, "Unexpected formula '%s' with sort '%s'", f, f.getSort());
@@ -464,38 +467,48 @@ public <R> R visit(FormulaVisitor<R> visitor, Formula formula, final Term f) {
       } else {
         // Term expressions like uninterpreted function calls (Kind.APPLY_UF) or operators (e.g.
         // Kind.AND).
-        // These are all treated like operators, so we can get the declaration by f.getOperator()!
+        Kind kind = f.getKind();
 
-        ImmutableList.Builder<Formula> argsBuilder = ImmutableList.builder();
+        // Collect indices
+        ImmutableList.Builder<Integer> indexBuilder = ImmutableList.builder();
+        if (f.hasOp()) {
+          Op operator = f.getOp();
+          for (int p = 0; p < operator.getNumIndices(); p++) {
+            Term index = operator.get(p);
+            if (index.isIntegerValue()) {
+              indexBuilder.add(index.getIntegerValue().intValueExact());
+            }
+          }
+        }
 
-        List<FormulaType<?>> argsTypes = new ArrayList<>();
+        // Collect arguments
+        ImmutableList.Builder<Formula> argsBuilder = ImmutableList.builder();
+        ImmutableList.Builder<FormulaType<?>> argTypesBuilder = ImmutableList.builder();
 
-        // Term operator = normalize(f.getSort());
-        Kind kind = f.getKind();
         if (sort.isFunction() || kind == Kind.APPLY_UF) {
           // The arguments are all children except the first one
           for (int i = 1; i < f.getNumChildren(); i++) {
-            argsTypes.add(getFormulaTypeFromTermType(f.getChild(i).getSort()));
+            argTypesBuilder.add(getFormulaTypeFromTermType(f.getChild(i).getSort()));
             // CVC5s first argument in a function/Uf is the declaration, we don't need that here
             argsBuilder.add(encapsulate(f.getChild(i)));
           }
         } else {
           for (Term arg : f) {
-            argsTypes.add(getFormulaType(arg));
+            argTypesBuilder.add(getFormulaType(arg));
             argsBuilder.add(encapsulate(arg));
           }
         }
 
-        // TODO some operations (BV_SIGN_EXTEND, BV_ZERO_EXTEND, maybe more) encode information as
-        // part of the operator itself, thus the arity is one too small and there might be no
-        // possibility to access the information from user side. Should we encode such information
-        // as additional parameters? We do so for some methods of Princess.
         if (sort.isFunction()) {
           return visitor.visitFunction(
               formula,
               argsBuilder.build(),
               FunctionDeclarationImpl.of(
-                  getName(f), getDeclarationKind(f), argsTypes, getFormulaType(f), normalize(f)));
+                  getName(f),
+                  getDeclarationKind(f),
+                  argTypesBuilder.build(),
+                  getFormulaType(f),
+                  normalize(f)));
         } else if (kind == Kind.APPLY_UF) {
           return visitor.visitFunction(
               formula,
@@ -503,7 +516,7 @@ public <R> R visit(FormulaVisitor<R> visitor, Formula formula, final Term f) {
               FunctionDeclarationImpl.of(
                   getName(f),
                   getDeclarationKind(f),
-                  argsTypes,
+                  argTypesBuilder.build(),
                   getFormulaType(f),
                   normalize(f.getChild(0))));
         } else {
@@ -512,7 +525,12 @@ public <R> R visit(FormulaVisitor<R> visitor, Formula formula, final Term f) {
               formula,
               argsBuilder.build(),
               FunctionDeclarationImpl.of(
-                  getName(f), getDeclarationKind(f), argsTypes, getFormulaType(f), normalize(f)));
+                  getName(f),
+                  getDeclarationKind(f),
+                  indexBuilder.build(),
+                  argTypesBuilder.build(),
+                  getFormulaType(f),
+                  normalize(f)));
         }
       }
     } catch (CVC5ApiException e) {
diff --git a/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5FormulaCreator.java b/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5FormulaCreator.java
index a9bb19b500..0fcef5b73a 100644
--- a/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5FormulaCreator.java
+++ b/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5FormulaCreator.java
@@ -120,6 +120,7 @@
 import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_type_repr;
 
 import com.google.common.base.Preconditions;
+import com.google.common.base.Splitter;
 import com.google.common.collect.ImmutableList;
 import com.google.common.collect.ImmutableSet;
 import com.google.common.primitives.Longs;
@@ -371,6 +372,18 @@ && msat_is_enum_type(environment, msat_term_get_type(f))) {
         return visitor.visitFreeVariable(formula, name);
       }
 
+      // Collect indices: We need to extract them from the term name in MathSAT
+      FunctionDeclarationKind kind = getDeclarationKind(f);
+      List<String> tokens =
+          Splitter.on('_')
+              .splitToList(name.startsWith("`") ? name.substring(1, name.length() - 1) : name);
+
+      ImmutableList.Builder<Integer> indices = ImmutableList.builder();
+      for (int p = 1; p <= FunctionDeclarationKind.getNumIndices(kind); p++) {
+        indices.add(Integer.valueOf(tokens.get(p)));
+      }
+
+      // Now collect the arguments
       ImmutableList.Builder<Formula> args = ImmutableList.builder();
       ImmutableList.Builder<FormulaType<?>> argTypes = ImmutableList.builder();
       for (int i = 0; i < arity; i++) {
@@ -388,7 +401,8 @@ && msat_is_enum_type(environment, msat_term_get_type(f))) {
           args.build(),
           FunctionDeclarationImpl.of(
               name,
-              getDeclarationKind(f),
+              kind,
+              indices.build(),
               argTypes.build(),
               getFormulaType(f),
               msat_term_get_decl(f)));
diff --git a/src/org/sosy_lab/java_smt/solvers/princess/PrincessEnvironment.java b/src/org/sosy_lab/java_smt/solvers/princess/PrincessEnvironment.java
index b3a5e937e0..81c0c42b8a 100644
--- a/src/org/sosy_lab/java_smt/solvers/princess/PrincessEnvironment.java
+++ b/src/org/sosy_lab/java_smt/solvers/princess/PrincessEnvironment.java
@@ -12,6 +12,7 @@
 import static scala.collection.JavaConverters.collectionAsScalaIterableConverter;
 
 import ap.api.SimpleAPI;
+import ap.basetypes.IdealInt;
 import ap.parameters.GlobalSettings;
 import ap.parser.BooleanCompactifier;
 import ap.parser.Environment.EnvironmentException;
@@ -22,6 +23,7 @@
 import ap.parser.IFunApp;
 import ap.parser.IFunction;
 import ap.parser.IIntFormula;
+import ap.parser.IIntLit;
 import ap.parser.ITerm;
 import ap.parser.Parser2InputAbsy.ParseException;
 import ap.parser.Parser2InputAbsy.TranslationException;
@@ -566,6 +568,18 @@ private static String getName(IExpression var) {
   static FormulaType<?> getFormulaType(IExpression pFormula) {
     if (pFormula instanceof IFormula) {
       return FormulaType.BooleanType;
+    } else if (pFormula instanceof IFunApp pApp
+        && pApp.fun().equals(ModuloArithmetic.bv_extract())) {
+      IIntLit upper = (IIntLit) pFormula.apply(0);
+      IIntLit lower = (IIntLit) pFormula.apply(1);
+      IdealInt bwResult = upper.value().$minus(lower.value());
+      return FormulaType.getBitvectorTypeWithSize(bwResult.intValue());
+    } else if (pFormula instanceof IFunApp pApp
+        && pApp.fun().equals(ModuloArithmetic.bv_concat())) {
+      IIntLit upper = (IIntLit) pFormula.apply(0);
+      IIntLit lower = (IIntLit) pFormula.apply(1);
+      IdealInt bwResult = upper.value().$plus(lower.value());
+      return FormulaType.getBitvectorTypeWithSize(bwResult.intValue());
     } else {
       final Sort sort = Sort.sortOf((ITerm) pFormula);
       try {
diff --git a/src/org/sosy_lab/java_smt/solvers/princess/PrincessFormulaCreator.java b/src/org/sosy_lab/java_smt/solvers/princess/PrincessFormulaCreator.java
index 57768d280a..c99985514a 100644
--- a/src/org/sosy_lab/java_smt/solvers/princess/PrincessFormulaCreator.java
+++ b/src/org/sosy_lab/java_smt/solvers/princess/PrincessFormulaCreator.java
@@ -394,6 +394,42 @@ private static boolean isValue(IExpression input) {
   public <R> R visit(FormulaVisitor<R> visitor, final Formula f, final IExpression input) {
     if (isValue(input)) {
       return visitor.visitConstant(f, convertValue(input));
+    } else if (input instanceof IFunApp pApp && pApp.fun().equals(ModuloArithmetic.bv_extract())) {
+      var kind = FunctionDeclarationKind.BV_EXTRACT;
+      var upper = ((IIntLit) input.apply(0)).value().intValue();
+      var lower = ((IIntLit) input.apply(1)).value().intValue();
+      var arg = input.apply(2);
+      var argType = (FormulaType.BitvectorType) PrincessEnvironment.getFormulaType(arg);
+
+      return visitor.visitFunction(
+          f,
+          ImmutableList.of(encapsulateWithTypeOf(arg)),
+          FunctionDeclarationImpl.of(
+              kind.toString(),
+              kind,
+              ImmutableList.of(upper, lower),
+              ImmutableList.of(argType),
+              FormulaType.getBitvectorTypeWithSize(upper - lower),
+              new PrincessFunctionDeclaration.PrincessBitvectorExtractDeclaration(upper, lower)));
+
+    } else if (input instanceof IFunApp pApp && pApp.fun().equals(ModuloArithmetic.bv_concat())) {
+      var kind = FunctionDeclarationKind.BV_CONCAT;
+      var size1 = ((IIntLit) input.apply(0)).value().intValue();
+      var size2 = ((IIntLit) input.apply(1)).value().intValue();
+      var arg1 = input.apply(2);
+      var arg2 = input.apply(3);
+      var arg1Type = (FormulaType.BitvectorType) PrincessEnvironment.getFormulaType(arg1);
+      var arg2Type = (FormulaType.BitvectorType) PrincessEnvironment.getFormulaType(arg2);
+
+      return visitor.visitFunction(
+          f,
+          ImmutableList.of(encapsulateWithTypeOf(arg1), encapsulateWithTypeOf(arg2)),
+          FunctionDeclarationImpl.of(
+              kind.toString(),
+              kind,
+              ImmutableList.of(arg1Type, arg2Type),
+              FormulaType.getBitvectorTypeWithSize(size1 + size2),
+              new PrincessFunctionDeclaration.PrincessBitvectorConcatDeclaration()));
 
     } else if (input instanceof IQuantified iQuantified) {
       return visitQuantifier(visitor, (BooleanFormula) f, iQuantified);
@@ -466,16 +502,13 @@ public <R> R visit(FormulaVisitor<R> visitor, final Formula f, final IExpression
       return visit(visitor, f, iIntFormula.t());
     }
 
-    ImmutableList.Builder<Formula> args = ImmutableList.builder();
-    ImmutableList.Builder<FormulaType<?>> argTypes = ImmutableList.builder();
-    int arity = input.length();
-    int arityStart = 0;
+    int numSortParameters = getNumSortParameters(kind);
+    int numIndices = FunctionDeclarationKind.getNumIndices(kind);
 
     PrincessFunctionDeclaration solverDeclaration;
-    if (isBitvectorOperationWithAdditionalArgument(kind)) {
+    if (numSortParameters > 0) {
       // the first argument is the bitsize, and it is not relevant for the user.
       // we do not want type/sort information as arguments.
-      arityStart = 1;
       if (input instanceof IAtom iAtom) {
         solverDeclaration = new PrincessBitvectorToBooleanDeclaration(iAtom.pred());
       } else if (input instanceof IFunApp iFunApp) {
@@ -496,7 +529,17 @@ public <R> R visit(FormulaVisitor<R> visitor, final Formula f, final IExpression
       solverDeclaration = new PrincessByExampleDeclaration(input);
     }
 
-    for (int i = arityStart; i < arity; i++) {
+    ImmutableList.Builder<Integer> indices = ImmutableList.builder();
+
+    for (int i = numSortParameters; i < numSortParameters + numIndices; i++) {
+      IExpression term = input.apply(i);
+      indices.add(((IIntLit) term).value().intValue());
+    }
+
+    ImmutableList.Builder<Formula> args = ImmutableList.builder();
+    ImmutableList.Builder<FormulaType<?>> argTypes = ImmutableList.builder();
+
+    for (int i = numSortParameters + numIndices; i < input.length(); i++) {
       IExpression arg = input.apply(i);
       FormulaType<?> argumentType = getFormulaType(arg);
       args.add(encapsulate(argumentType, arg));
@@ -507,7 +550,12 @@ public <R> R visit(FormulaVisitor<R> visitor, final Formula f, final IExpression
         f,
         args.build(),
         FunctionDeclarationImpl.of(
-            getName(input), kind, argTypes.build(), getFormulaType(f), solverDeclaration));
+            getName(input),
+            kind,
+            indices.build(),
+            argTypes.build(),
+            getFormulaType(f),
+            solverDeclaration));
   }
 
   private <R> R visitQuantifier(FormulaVisitor<R> visitor, BooleanFormula f, IQuantified input) {
@@ -547,7 +595,8 @@ private String getFreshVariableNameForBody(IFormula body) {
         body, k -> "__JAVASMT__BOUND_VARIABLE_" + boundVariableNames.size());
   }
 
-  private boolean isBitvectorOperationWithAdditionalArgument(FunctionDeclarationKind kind) {
+  private int getNumSortParameters(FunctionDeclarationKind kind) {
+    // TODO Check that his is still right
     return switch (kind) {
       case BV_NOT,
           BV_NEG,
@@ -570,9 +619,13 @@ private boolean isBitvectorOperationWithAdditionalArgument(FunctionDeclarationKi
           BV_SGT,
           BV_UGE,
           BV_SGE,
-          BV_EQ ->
-          true;
-      default -> false;
+          BV_EQ,
+          BV_LSHR,
+          BV_ASHR,
+          BV_SHL ->
+          1;
+      case BV_CONCAT -> 2;
+      default -> 0;
     };
   }
 
diff --git a/src/org/sosy_lab/java_smt/solvers/princess/PrincessFunctionDeclaration.java b/src/org/sosy_lab/java_smt/solvers/princess/PrincessFunctionDeclaration.java
index 6291a81784..f2324570a1 100644
--- a/src/org/sosy_lab/java_smt/solvers/princess/PrincessFunctionDeclaration.java
+++ b/src/org/sosy_lab/java_smt/solvers/princess/PrincessFunctionDeclaration.java
@@ -22,6 +22,7 @@
 import ap.parser.ITerm;
 import ap.parser.ITermITE;
 import ap.terfor.preds.Predicate;
+import ap.theories.bitvectors.ModuloArithmetic$;
 import ap.theories.nia.GroebnerMultiplication;
 import ap.types.Sort;
 import ap.types.Sort$;
@@ -235,4 +236,31 @@ public IExpression makeApp(PrincessEnvironment env, List<IExpression> args) {
       return GroebnerMultiplication.mult((ITerm) args.get(0), (ITerm) args.get(1));
     }
   }
+
+  static final class PrincessBitvectorExtractDeclaration extends PrincessFunctionDeclaration {
+    private final int upper;
+    private final int lower;
+
+    PrincessBitvectorExtractDeclaration(int pUpper, int pLower) {
+      upper = pUpper;
+      lower = pLower;
+    }
+
+    @Override
+    public IExpression makeApp(PrincessEnvironment env, List<IExpression> args) {
+      checkArgument(args.size() == 1);
+      return ModuloArithmetic$.MODULE$.extract(upper, lower, (ITerm) args.get(0));
+    }
+  }
+
+  static final class PrincessBitvectorConcatDeclaration extends PrincessFunctionDeclaration {
+
+    PrincessBitvectorConcatDeclaration() {}
+
+    @Override
+    public IExpression makeApp(PrincessEnvironment env, List<IExpression> args) {
+      checkArgument(args.size() == 2);
+      return ModuloArithmetic$.MODULE$.concat((ITerm) args.get(0), (ITerm) args.get(1));
+    }
+  }
 }
diff --git a/src/org/sosy_lab/java_smt/solvers/yices2/Yices2FormulaCreator.java b/src/org/sosy_lab/java_smt/solvers/yices2/Yices2FormulaCreator.java
index cca8f82dc8..069fad7133 100644
--- a/src/org/sosy_lab/java_smt/solvers/yices2/Yices2FormulaCreator.java
+++ b/src/org/sosy_lab/java_smt/solvers/yices2/Yices2FormulaCreator.java
@@ -505,7 +505,12 @@ private <R> R visitFunctionApplication(
         pFormula,
         args,
         FunctionDeclarationImpl.of(
-            functionName, functionKind, argTypes, getFormulaType(pF), functionDeclaration));
+            functionName,
+            functionKind,
+            functionIndex,
+            argTypes,
+            getFormulaType(pF),
+            functionDeclaration));
   }
 
   private int buildDeclaration(
diff --git a/src/org/sosy_lab/java_smt/solvers/z3/Z3FormulaCreator.java b/src/org/sosy_lab/java_smt/solvers/z3/Z3FormulaCreator.java
index ed679a6597..c49dfde1ec 100644
--- a/src/org/sosy_lab/java_smt/solvers/z3/Z3FormulaCreator.java
+++ b/src/org/sosy_lab/java_smt/solvers/z3/Z3FormulaCreator.java
@@ -22,6 +22,7 @@
 import com.microsoft.z3.Z3Exception;
 import com.microsoft.z3.enumerations.Z3_ast_kind;
 import com.microsoft.z3.enumerations.Z3_decl_kind;
+import com.microsoft.z3.enumerations.Z3_param_kind;
 import com.microsoft.z3.enumerations.Z3_sort_kind;
 import com.microsoft.z3.enumerations.Z3_symbol_kind;
 import java.lang.ref.PhantomReference;
@@ -517,7 +518,8 @@ public <R> R visit(FormulaVisitor<R> visitor, final Formula formula, final Long
 
       case Z3_APP_AST -> {
         int arity = Native.getAppNumArgs(environment, f);
-        int declKind = Native.getDeclKind(environment, Native.getAppDecl(environment, f));
+        long decl = Native.getAppDecl(environment, f);
+        int declKind = Native.getDeclKind(environment, decl);
 
         if (arity == 0) {
           // constants
@@ -563,6 +565,14 @@ public <R> R visit(FormulaVisitor<R> visitor, final Formula formula, final Long
           }
         }
 
+        ImmutableList.Builder<Integer> indexBuilder = ImmutableList.builder();
+        for (int p = 0; p < Native.getDeclNumParameters(environment, decl); p++) {
+          int kind = Native.getDeclParameterKind(environment, decl, p);
+          if (kind == Z3_param_kind.Z3_PK_UINT.toInt()) {
+            indexBuilder.add(Native.getDeclIntParameter(environment, decl, p));
+          }
+        }
+
         // Function application with zero or more parameters
         ImmutableList.Builder<Formula> args = ImmutableList.builder();
         ImmutableList.Builder<FormulaType<?>> argTypes = ImmutableList.builder();
@@ -578,6 +588,7 @@ public <R> R visit(FormulaVisitor<R> visitor, final Formula formula, final Long
             FunctionDeclarationImpl.of(
                 getAppName(f),
                 getDeclarationKind(f),
+                indexBuilder.build(),
                 argTypes.build(),
                 getFormulaType(f),
                 Native.getAppDecl(environment, f)));
diff --git a/src/org/sosy_lab/java_smt/solvers/z3legacy/Z3LegacyFormulaCreator.java b/src/org/sosy_lab/java_smt/solvers/z3legacy/Z3LegacyFormulaCreator.java
index 50753cc294..eecb8dde5f 100644
--- a/src/org/sosy_lab/java_smt/solvers/z3legacy/Z3LegacyFormulaCreator.java
+++ b/src/org/sosy_lab/java_smt/solvers/z3legacy/Z3LegacyFormulaCreator.java
@@ -26,6 +26,7 @@
 import com.microsoft.z3legacy.Z3Exception;
 import com.microsoft.z3legacy.enumerations.Z3_ast_kind;
 import com.microsoft.z3legacy.enumerations.Z3_decl_kind;
+import com.microsoft.z3legacy.enumerations.Z3_param_kind;
 import com.microsoft.z3legacy.enumerations.Z3_sort_kind;
 import com.microsoft.z3legacy.enumerations.Z3_symbol_kind;
 import java.lang.ref.PhantomReference;
@@ -525,7 +526,8 @@ public <R> R visit(FormulaVisitor<R> visitor, final Formula formula, final Long
 
       case Z3_APP_AST -> {
         int arity = Native.getAppNumArgs(environment, f);
-        int declKind = Native.getDeclKind(environment, Native.getAppDecl(environment, f));
+        long decl = Native.getAppDecl(environment, f);
+        int declKind = Native.getDeclKind(environment, decl);
 
         if (arity == 0) {
           // constants
@@ -571,6 +573,14 @@ public <R> R visit(FormulaVisitor<R> visitor, final Formula formula, final Long
           }
         }
 
+        ImmutableList.Builder<Integer> indexBuilder = ImmutableList.builder();
+        for (int p = 0; p < Native.getDeclNumParameters(environment, decl); p++) {
+          int kind = Native.getDeclParameterKind(environment, decl, p);
+          if (kind == Z3_param_kind.Z3_PK_UINT.toInt()) {
+            indexBuilder.add(Native.getDeclIntParameter(environment, decl, p));
+          }
+        }
+
         // Function application with zero or more parameters
         ImmutableList.Builder<Formula> args = ImmutableList.builder();
         ImmutableList.Builder<FormulaType<?>> argTypes = ImmutableList.builder();
@@ -586,6 +596,7 @@ public <R> R visit(FormulaVisitor<R> visitor, final Formula formula, final Long
             FunctionDeclarationImpl.of(
                 getAppName(f),
                 getDeclarationKind(f),
+                indexBuilder.build(),
                 argTypes.build(),
                 getFormulaType(f),
                 Native.getAppDecl(environment, f)));
diff --git a/src/org/sosy_lab/java_smt/test/SolverVisitorTest.java b/src/org/sosy_lab/java_smt/test/SolverVisitorTest.java
index b1b205d3db..68c9d28976 100644
--- a/src/org/sosy_lab/java_smt/test/SolverVisitorTest.java
+++ b/src/org/sosy_lab/java_smt/test/SolverVisitorTest.java
@@ -640,6 +640,94 @@ protected Void visitDefault(Formula f) {
     }
   }
 
+  private void checkIndexedSymbol(
+      FunctionDeclarationKind pExpectedKind, List<Integer> pExpectedIndex, Formula pTerm) {
+    mgr.visit(
+        pTerm,
+        new DefaultFormulaVisitor<Void>() {
+          @Override
+          public Void visitFunction(
+              Formula f, List<Formula> args, FunctionDeclaration<?> functionDeclaration) {
+            assertThat(functionDeclaration.getKind()).isEqualTo(pExpectedKind);
+            assertThat(functionDeclaration.getIndices()).isEqualTo(pExpectedIndex);
+            return null;
+          }
+
+          @Override
+          protected Void visitDefault(Formula f) {
+            throw new AssertionError();
+          }
+        });
+  }
+
+  private List<Formula> getArgs(Formula pFormula) {
+    return mgr.visit(
+        pFormula,
+        new DefaultFormulaVisitor<>() {
+          @Override
+          public List<Formula> visitFunction(
+              Formula f, List<Formula> args, FunctionDeclaration<?> functionDeclaration) {
+            return args;
+          }
+
+          @Override
+          protected List<Formula> visitDefault(Formula f) {
+            throw new AssertionError();
+          }
+        });
+  }
+
+  @Test
+  public void bvExtractVisit() {
+    requireBitvectors();
+    assume()
+        .withMessage("Visiting indexed functions not fully supported on %")
+        .that(solver)
+        .isNotEqualTo(Solvers.CVC4);
+
+    var x = bvmgr.makeVariable(8, "x");
+    var f = bvmgr.extract(x, 3, 0);
+
+    if (solver == Solvers.YICES2) {
+      // Yices2 will rewrite to (bv-array (bit x 3) (bit x 2) (bit x 1) (bit x 0))
+      var args = getArgs(f);
+      assertThat(args).hasSize(4);
+      for (var p = 0; p < args.size(); p++) {
+        checkIndexedSymbol(
+            FunctionDeclarationKind.BV_EXTRACT, ImmutableList.of(3 - p, 3 - p), args.get(p));
+      }
+    } else {
+      checkIndexedSymbol(FunctionDeclarationKind.BV_EXTRACT, ImmutableList.of(3, 0), f);
+    }
+  }
+
+  @Test
+  public void bvExtendVisit() {
+    requireBitvectors();
+    assume()
+        .withMessage("Visiting indexed functions not fully supported on %")
+        .that(solver)
+        .isNoneOf(Solvers.CVC4, Solvers.PRINCESS);
+
+    var x = bvmgr.makeVariable(8, "x");
+    var f = bvmgr.extend(x, 8, false);
+
+    if (solver == Solvers.YICES2) {
+      // Yices2 will rewrite to (bv-array #b0 ... #b0 (bit x 7) ... (bit x 0)
+      var terms = getArgs(f);
+      assertThat(terms).hasSize(16);
+      for (var p = 0; p < terms.size(); p++) {
+        if (p < 8) {
+          assertThat(terms.get(p)).isEqualTo(bvmgr.makeBitvector(1, 0));
+        } else {
+          assertThat(terms.get(p)).isEqualTo(bvmgr.extract(f, 15 - p, 15 - p));
+        }
+      }
+    } else {
+      checkIndexedSymbol(FunctionDeclarationKind.BV_ZERO_EXTENSION, ImmutableList.of(8), f);
+    }
+  }
+
   @Test
   public void bvVisit() throws SolverException, InterruptedException {
     requireBitvectors();