diff --git a/src/api/MainSolver.cc b/src/api/MainSolver.cc
index 4aa9afe73..09c67268d 100644
--- a/src/api/MainSolver.cc
+++ b/src/api/MainSolver.cc
@@ -93,7 +93,7 @@ bool MainSolver::pop() {
     frames.pop();
     preprocessor.pop();
     termNames.popScope();
-    firstNotSimplifiedFrame = std::min(firstNotSimplifiedFrame, frames.frameCount());
+    firstNotPreprocessedFrame = std::min(firstNotPreprocessedFrame, frames.frameCount());
     if (not isLastFrameUnsat()) { getSMTSolver().restoreOK(); }
     return true;
 }
@@ -115,15 +115,15 @@ void MainSolver::insertFormula(PTRef fla) {
         // formulas,
         //     thus we need the old value of count. TODO: Find a good interface for this so it cannot be broken this
         //     easily
-        unsigned int partition_index = insertedFormulasCount++;
+        unsigned int partition_index = insertedAssertionsCount++;
         pmanager.assignTopLevelPartitionIndex(partition_index, fla);
         assert(pmanager.getPartitionIndex(fla) != -1);
     } else {
-        ++insertedFormulasCount;
+        ++insertedAssertionsCount;
     }
 
     frames.add(fla);
-    firstNotSimplifiedFrame = std::min(firstNotSimplifiedFrame, frames.frameCount() - 1);
+    firstNotPreprocessedFrame = std::min(firstNotPreprocessedFrame, frames.frameCount() - 1);
 }
 
 bool MainSolver::tryAddNamedAssertion(PTRef fla, std::string const & name) {
@@ -140,63 +140,138 @@ bool MainSolver::tryAddTermNameFor(PTRef fla, std::string const & name) {
 
 sstat MainSolver::simplifyFormulas() {
     status = s_Undef;
-    for (std::size_t i = firstNotSimplifiedFrame; i < frames.frameCount() && status != s_False; i++) {
-        PreprocessingContext context{.frameCount = i, .perPartition = trackPartitions()};
-        preprocessor.prepareForProcessingFrame(i);
-        firstNotSimplifiedFrame = i + 1;
-        if (context.perPartition) {
-            vec<PTRef> frameFormulas;
-            for (PTRef fla : frames[i].formulas) {
-                PTRef processed = theory->preprocessAfterSubstitutions(fla, context);
-                pmanager.transferPartitionMembership(fla, processed);
-                frameFormulas.push(processed);
-                preprocessor.addPreprocessedFormula(processed);
-            }
-            if (frameFormulas.size() == 0 or std::all_of(frameFormulas.begin(), frameFormulas.end(),
-                                                         [&](PTRef fla) { return fla == logic.getTerm_true(); })) {
-                continue;
-            }
-            theory->afterPreprocessing(preprocessor.getPreprocessedFormulas());
-            for (PTRef fla : frameFormulas) {
-                if (fla == logic.getTerm_true()) { continue; }
-                assert(pmanager.getPartitionIndex(fla) != -1);
-                // Optimize the dag for cnfization
-                if (logic.isBooleanOperator(fla)) {
-                    PTRef old = fla;
-                    fla = rewriteMaxArity(fla);
-                    pmanager.transferPartitionMembership(old, fla);
-                }
-                assert(pmanager.getPartitionIndex(fla) != -1);
-                pmanager.propagatePartitionMask(fla);
-                status = giveToSolver(fla, frames[i].getId());
-                if (status == s_False) { break; }
-            }
-        } else {
-            PTRef frameFormula = logic.mkAnd(frames[i].formulas);
-            if (context.frameCount > 0) { frameFormula = applyLearntSubstitutions(frameFormula); }
-            frameFormula = theory->preprocessBeforeSubstitutions(frameFormula, context);
-            frameFormula = substitutionPass(frameFormula, context);
-            frameFormula = theory->preprocessAfterSubstitutions(frameFormula, context);
-
-            if (logic.isFalse(frameFormula)) {
-                giveToSolver(logic.getTerm_false(), frames[i].getId());
-                status = s_False;
-                break;
-            }
-            preprocessor.addPreprocessedFormula(frameFormula);
-            theory->afterPreprocessing(preprocessor.getPreprocessedFormulas());
-            // Optimize the dag for cnfization
-            if (logic.isBooleanOperator(frameFormula)) { frameFormula = rewriteMaxArity(frameFormula); }
-            status = giveToSolver(frameFormula, frames[i].getId());
-        }
+    for (std::size_t i = firstNotPreprocessedFrame; i < frames.frameCount(); ++i) {
+        assert(status != s_False);
+        if (tryPreprocessFormulasOfFrame(i)) { continue; }
+        assert(status == s_False);
+        break;
     }
+
     if (status == s_False) {
-        assert(firstNotSimplifiedFrame > 0);
-        rememberUnsatFrame(firstNotSimplifiedFrame - 1);
+        assert(firstNotPreprocessedFrame > 0);
+        rememberUnsatFrame(firstNotPreprocessedFrame - 1);
     }
+
     return status;
 }
 
+bool MainSolver::tryPreprocessFormulasOfFrame(std::size_t i) {
+    auto & frame = frames[i];
+    FrameId const frameId = frame.getId();
+    PreprocessingContext context{.frameCount = i, .perPartition = trackPartitions()};
+    preprocessor.prepareForProcessingFrame(i);
+    firstNotPreprocessedFrame = i + 1;
+
+    assert(status != s_False);
+
+    if (not context.perPartition) {
+        PTRef frameFormula = preprocessFormulasDefault(frame.formulas, context);
+        status = giveToSolver(frameFormula, frameId);
+        return status != s_False;
+    }
+
+    vec<PTRef> processedFormulas = preprocessFormulasPerPartition(frame.formulas, context);
+    for (PTRef fla : processedFormulas) {
+        status = giveToSolver(fla, frameId);
+        if (status == s_False) { return false; }
+    }
+
+    assert(status != s_False);
+    return true;
+}
+
+PTRef MainSolver::preprocessFormulasDefault(vec<PTRef> const & frameFormulas, PreprocessingContext const & context) {
+    assert(not context.perPartition);
+
+    if (frameFormulas.size() == 0) { return logic.getTerm_true(); }
+
+    PTRef frameFormula = logic.mkAnd(frameFormulas);
+    return preprocessFormula(frameFormula, context);
+}
+
+vec<PTRef> MainSolver::preprocessFormulasPerPartition(vec<PTRef> const & frameFormulas,
+                                                      PreprocessingContext const & context) {
+    assert(context.perPartition);
+
+    if (frameFormulas.size() == 0) { return {}; }
+
+    vec<PTRef> processedFormulas;
+    for (PTRef fla : frameFormulas) {
+        PTRef processed = preprocessFormulaBeforeFinalTheoryPreprocessing(fla, context);
+        processedFormulas.push(processed);
+    }
+
+    assert(processedFormulas.size() == frameFormulas.size());
+    assert(processedFormulas.size() > 0);
+    if (std::all_of(processedFormulas.begin(), processedFormulas.end(),
+                    [&](PTRef fla) { return fla == logic.getTerm_true(); })) {
+        return {};
+    }
+
+    preprocessFormulaDoFinalTheoryPreprocessing(context);
+
+    for (PTRef & fla : processedFormulas) {
+        if (fla == logic.getTerm_true()) { continue; }
+        fla = preprocessFormulaAfterFinalTheoryPreprocessing(fla, context);
+    }
+
+    return processedFormulas;
+}
+
+PTRef MainSolver::preprocessFormula(PTRef fla, PreprocessingContext const & context) {
+    PTRef processed = preprocessFormulaBeforeFinalTheoryPreprocessing(fla, context);
+    preprocessFormulaDoFinalTheoryPreprocessing(context);
+    processed = preprocessFormulaAfterFinalTheoryPreprocessing(processed, context);
+    return processed;
+}
+
+PTRef MainSolver::preprocessFormulaBeforeFinalTheoryPreprocessing(PTRef fla, PreprocessingContext const & context) {
+    bool const perPartition = context.perPartition;
+    PTRef processed = fla;
+
+    if (not perPartition) {
+        if (context.frameCount > 0) { processed = applyLearntSubstitutions(processed); }
+        processed = theory->preprocessBeforeSubstitutions(processed, context);
+        processed = substitutionPass(processed, context);
+    }
+
+    processed = theory->preprocessAfterSubstitutions(processed, context);
+
+    if (perPartition) {
+        pmanager.transferPartitionMembership(fla, processed);
+    } else if (logic.isFalse(processed)) {
+        return logic.getTerm_false();
+    }
+
+    preprocessor.addPreprocessedFormula(processed);
+
+    return processed;
+}
+
+void MainSolver::preprocessFormulaDoFinalTheoryPreprocessing(PreprocessingContext const &) {
+    theory->afterPreprocessing(preprocessor.getPreprocessedFormulas());
+}
+
+PTRef MainSolver::preprocessFormulaAfterFinalTheoryPreprocessing(PTRef fla, PreprocessingContext const & context) {
+    bool const perPartition = context.perPartition;
+    PTRef processed = fla;
+
+    assert(not perPartition or pmanager.getPartitionIndex(processed) != -1);
+
+    // Optimize the dag for cnfization
+    if (logic.isBooleanOperator(processed)) {
+        processed = rewriteMaxArity(processed);
+        if (perPartition) { pmanager.transferPartitionMembership(fla, processed); }
+    }
+
+    if (perPartition) {
+        assert(pmanager.getPartitionIndex(processed) != -1);
+        pmanager.propagatePartitionMask(processed);
+    }
+
+    return processed;
+}
+
 vec<PTRef> MainSolver::getCurrentAssertions() const {
     vec<PTRef> assertions;
     size_t const cnt = frames.frameCount();
@@ -316,11 +391,15 @@ sstat MainSolver::giveToSolver(PTRef root, FrameId push_id) {
         std::vector<vec<Lit>> clauses;
         void operator()(vec<Lit> && c) override { clauses.push_back(std::move(c)); }
     };
+
+    if (root == logic.getTerm_true()) { return s_Undef; }
+
     ClauseCallBack callBack;
     ts.setClauseCallBack(&callBack);
     ts.Cnfizer::cnfize(root, push_id);
     bool const keepPartitionsSeparate = trackPartitions();
-    Lit frameLit = push_id == 0 ? Lit{} : term_mapper->getOrCreateLit(frameTerms[push_id]);
+    Lit frameLit;
+    if (push_id != 0) { frameLit = term_mapper->getOrCreateLit(frameTerms[push_id]); }
     int partitionIndex = keepPartitionsSeparate ? pmanager.getPartitionIndex(root) : -1;
     for (auto & clause : callBack.clauses) {
         if (push_id != 0) { clause.push(frameLit); }
diff --git a/src/api/MainSolver.h b/src/api/MainSolver.h
index 396fff93a..20f9c9f84 100644
--- a/src/api/MainSolver.h
+++ b/src/api/MainSolver.h
@@ -89,7 +89,7 @@ class MainSolver {
     void insertFormula(PTRef fla);
     // Alias for `insertFormula`, reserved for future use
     void addAssertion(PTRef fla) { return insertFormula(fla); }
-    std::size_t getInsertedFormulasCount() const { return insertedFormulasCount; }
+    std::size_t getInsertedFormulasCount() const { return insertedAssertionsCount; }
     // Alias for `getInsertedFormulasCount`, reserved for future use
     std::size_t getAssertionsCount() const { return getInsertedFormulasCount(); }
 
@@ -105,6 +105,8 @@ class MainSolver {
     // Simplify formulas until all are simplified or the instance is detected unsat
     // Skip assertion levels that have already been simplified
     sstat simplifyFormulas();
+    // Alias for `simplifyFormulas`, reserved for future use
+    sstat preprocess() { return simplifyFormulas(); }
 
     [[nodiscard]] sstat getStatus() const { return status; }
 
@@ -289,6 +291,16 @@ class MainSolver {
 
     inline bool trackPartitions() const;
 
+    virtual bool tryPreprocessFormulasOfFrame(std::size_t);
+
+    virtual PTRef preprocessFormulasDefault(vec<PTRef> const & frameFormulas, PreprocessingContext const &);
+    virtual vec<PTRef> preprocessFormulasPerPartition(vec<PTRef> const & frameFormulas, PreprocessingContext const &);
+
+    virtual PTRef preprocessFormula(PTRef, PreprocessingContext const &);
+    virtual PTRef preprocessFormulaBeforeFinalTheoryPreprocessing(PTRef, PreprocessingContext const &);
+    virtual void preprocessFormulaDoFinalTheoryPreprocessing(PreprocessingContext const &);
+    virtual PTRef preprocessFormulaAfterFinalTheoryPreprocessing(PTRef, PreprocessingContext const &);
+
     PTRef rewriteMaxArity(PTRef root);
 
     virtual sstat solve_(vec<FrameId> const & enabledFrames);
@@ -322,8 +334,8 @@ class MainSolver {
     int check_called = 0;    // A counter on how many times check was called.
 
     vec<PTRef> frameTerms;
-    std::size_t firstNotSimplifiedFrame = 0;
-    unsigned int insertedFormulasCount = 0;
+    std::size_t firstNotPreprocessedFrame = 0;
+    std::size_t insertedAssertionsCount = 0;
 };
 
 bool MainSolver::trackPartitions() const {