+//
+// SPDX-License-Identifier: Apache-2.0
+
+package org.sosy_lab.java_smt.basicimpl;
+
+/** Exception thrown if there is an error during Generating SMTLIB2. */
+// TODO Do we need those exception classes?
+public class GeneratorException extends RuntimeException {
+
+ private static final long serialVersionUID = 176487434783322L;
+
+ /** Constructs an UnsupportedOperationException with no detail message. */
+ public GeneratorException() {}
+
+ /**
+ * Constructs an UnsupportedOperationException with the specified detail message.
+ *
+ * @param message the detail message
+ */
+ public GeneratorException(String message) {
+ super(message);
+ }
+
+ /**
+ * Constructs a new exception with the specified detail message and cause.
+ *
+ * Note that the detail message associated with cause is not automatically
+ * incorporated in this exception's detail message.
+ *
+ * @param message the detail message (which is saved for later retrieval by the {@link
+ * Throwable#getMessage()} method).
+ * @param cause the cause (which is saved for later retrieval by the {@link Throwable#getCause()}
+ * method). (A {@code null} value is permitted, and indicates that the cause is nonexistent or
+ * unknown.)
+ * @since 1.5
+ */
+ public GeneratorException(String message, Throwable cause) {
+ super(message, cause);
+ }
+
+ /**
+ * Constructs a new exception with the specified cause and a detail message of {@code (cause==null
+ * ? null : cause.toString())} (which typically contains the class and detail message of {@code
+ * cause}). This constructor is useful for exceptions that are little more than wrappers for other
+ * throwables (for example, {@link java.security.PrivilegedActionException}).
+ *
+ * @param cause the cause (which is saved for later retrieval by the {@link Throwable#getCause()}
+ * method). (A {@code null} value is permitted, and indicates that the cause is nonexistent or
+ * unknown.)
+ * @since 1.5
+ */
+ public GeneratorException(Throwable cause) {
+ super(cause);
+ }
+}
diff --git a/src/org/sosy_lab/java_smt/basicimpl/ModelException.java b/src/org/sosy_lab/java_smt/basicimpl/ModelException.java
new file mode 100644
index 0000000000..39cc1adad9
--- /dev/null
+++ b/src/org/sosy_lab/java_smt/basicimpl/ModelException.java
@@ -0,0 +1,59 @@
+// This file is part of JavaSMT,
+// an API wrapper for a collection of SMT solvers:
+// https://github.com/sosy-lab/java-smt
+//
+// SPDX-FileCopyrightText: 2024 Dirk Beyer
+//
+// SPDX-License-Identifier: Apache-2.0
+
+package org.sosy_lab.java_smt.basicimpl;
+
+/** Exception thrown if there is an error during parsing the model from SMTLIB2. */
+// TODO Do we need those exception classes?
+public class ModelException extends RuntimeException {
+ /** Constructs an UnsupportedOperationException with no detail message. */
+ public ModelException() {}
+
+ /**
+ * Constructs an UnsupportedOperationException with the specified detail message.
+ *
+ * @param message the detail message
+ */
+ public ModelException(String message) {
+ super(message);
+ }
+
+ /**
+ * Constructs a new exception with the specified detail message and cause.
+ *
+ * Note that the detail message associated with cause is not automatically
+ * incorporated in this exception's detail message.
+ *
+ * @param message the detail message (which is saved for later retrieval by the {@link
+ * Throwable#getMessage()} method).
+ * @param cause the cause (which is saved for later retrieval by the {@link Throwable#getCause()}
+ * method). (A {@code null} value is permitted, and indicates that the cause is nonexistent or
+ * unknown.)
+ * @since 1.5
+ */
+ public ModelException(String message, Throwable cause) {
+ super(message, cause);
+ }
+
+ /**
+ * Constructs a new exception with the specified cause and a detail message of {@code (cause==null
+ * ? null : cause.toString())} (which typically contains the class and detail message of {@code
+ * cause}). This constructor is useful for exceptions that are little more than wrappers for other
+ * throwables (for example, {@link java.security.PrivilegedActionException}).
+ *
+ * @param cause the cause (which is saved for later retrieval by the {@link Throwable#getCause()}
+ * method). (A {@code null} value is permitted, and indicates that the cause is nonexistent or
+ * unknown.)
+ * @since 1.5
+ */
+ public ModelException(Throwable cause) {
+ super(cause);
+ }
+
+ static final long serialVersionUID = -1242599979055084673L;
+}
diff --git a/src/org/sosy_lab/java_smt/basicimpl/NumeralGenerator.java b/src/org/sosy_lab/java_smt/basicimpl/NumeralGenerator.java
new file mode 100644
index 0000000000..9a29634f93
--- /dev/null
+++ b/src/org/sosy_lab/java_smt/basicimpl/NumeralGenerator.java
@@ -0,0 +1,243 @@
+// This file is part of JavaSMT,
+// an API wrapper for a collection of SMT solvers:
+// https://github.com/sosy-lab/java-smt
+//
+// SPDX-FileCopyrightText: 2024 Dirk Beyer
+//
+// SPDX-License-Identifier: Apache-2.0
+
+package org.sosy_lab.java_smt.basicimpl;
+
+import com.google.common.collect.ImmutableList;
+import java.math.BigInteger;
+import java.util.ArrayList;
+import java.util.List;
+import java.util.function.Function;
+import org.sosy_lab.java_smt.api.NumeralFormula;
+import org.sosy_lab.java_smt.api.NumeralFormula.IntegerFormula;
+import org.sosy_lab.java_smt.basicimpl.Generator.Keyword;
+
+public class NumeralGenerator {
+ private NumeralGenerator() {}
+
+ /**
+ * @param result solver returned object for the makeNumber() call.
+ * @param number the value of the number as String.
+ */
+ protected static void logMakeNumber(Object result, String number) {
+ Generator.throwExceptionWhenParameterIsNull(ImmutableList.of(result, number));
+ List