diff --git a/src/logics/ArithLogic.cc b/src/logics/ArithLogic.cc
index 7b75cab69..ca9be0776 100644
--- a/src/logics/ArithLogic.cc
+++ b/src/logics/ArithLogic.cc
@@ -1,10 +1,11 @@
 #include "ArithLogic.h"
 
-#include "DivModRewriter.h"
 #include "FastRational.h"
 #include "OsmtApiException.h"
 #include "OsmtInternalException.h"
 #include "Polynomial.h"
+#include "Rewriter.h"
+#include "Rewritings.h"
 #include "PtStore.h"
 #include "SStore.h"
 #include "StringConv.h"
@@ -1147,16 +1148,9 @@ PTRef ArithLogic::removeAuxVars(PTRef tr) {
     class AuxSymbolMatcherConfig : public DefaultRewriterConfig {
         ArithLogic & logic;
     public:
-        AuxSymbolMatcherConfig(ArithLogic & logic) : logic(logic) {}
+        explicit AuxSymbolMatcherConfig(ArithLogic & logic) : logic(logic) {}
         PTRef rewrite(PTRef tr) override {
-            if (not logic.isVar(tr)) return tr; // Only variables can match
-            auto symName = std::string_view(logic.getSymName(tr));
-            if (symName.compare(0, DivModConfig::divPrefix.size(), DivModConfig::divPrefix) == 0) {
-                return DivModConfig::getDivTermFor(logic, tr);
-            } else if (symName.compare(0, DivModConfig::divPrefix.size(), DivModConfig::modPrefix) == 0){
-                return DivModConfig::getModTermFor(logic, tr);
-            }
-            return tr;
+            return opensmt::rewritings::tryGetOriginalDivModTerm(logic, tr).value_or(tr);
         }
     };
     // Note: this has negligible impact on performance, no need to check if there are divs or mods
diff --git a/src/logics/ArrayTheory.cc b/src/logics/ArrayTheory.cc
index 4092a95b2..77589465f 100644
--- a/src/logics/ArrayTheory.cc
+++ b/src/logics/ArrayTheory.cc
@@ -7,7 +7,9 @@
 #include "ArrayTheory.h"
 
 #include "ArrayHelpers.h"
-#include "DistinctRewriter.h"
+#include "Rewritings.h"
+
+using namespace opensmt::rewritings;
 
 PTRef ArrayTheory::preprocessAfterSubstitutions(PTRef fla, PreprocessingContext const &) {
     // TODO: simplify select over store on the same index
diff --git a/src/logics/LATheory.h b/src/logics/LATheory.h
index 20f2b1f2d..6ec9075db 100644
--- a/src/logics/LATheory.h
+++ b/src/logics/LATheory.h
@@ -10,8 +10,7 @@
 #define OPENSMT_LATHEORY_H
 #include "Theory.h"
 #include "ArithmeticEqualityRewriter.h"
-#include "DistinctRewriter.h"
-#include "DivModRewriter.h"
+#include "Rewritings.h"
 
 template<typename LinAlgLogic, typename LinAlgTHandler>
 class LATheory : public Theory
@@ -40,14 +39,14 @@ PTRef rewriteDivMod(TLogic &, PTRef fla) { return fla; }
 template<>
 PTRef rewriteDivMod<ArithLogic>(ArithLogic & logic, PTRef fla) {
     // Real logic cannot have div and mod
-    return not logic.hasIntegers() ? fla : DivModRewriter(logic).rewrite(fla);
+    return not logic.hasIntegers() ? fla : opensmt::rewritings::rewriteDivMod(logic,fla);
 }
 
 }
 
 template<typename LinAlgLogic, typename LinAlgTSHandler>
 PTRef LATheory<LinAlgLogic,LinAlgTSHandler>::preprocessAfterSubstitutions(PTRef fla, PreprocessingContext const &) {
-    fla = rewriteDistincts(getLogic(), fla);
+    fla = opensmt::rewritings::rewriteDistincts(getLogic(), fla);
     fla = rewriteDivMod<LinAlgLogic>(lalogic, fla);
     ArithmeticEqualityRewriter equalityRewriter(lalogic);
     fla = equalityRewriter.rewrite(fla);
diff --git a/src/logics/UFLATheory.cc b/src/logics/UFLATheory.cc
index 436d1ba72..16763e646 100644
--- a/src/logics/UFLATheory.cc
+++ b/src/logics/UFLATheory.cc
@@ -2,12 +2,13 @@
 
 #include "ArithmeticEqualityRewriter.h"
 #include "ArrayHelpers.h"
-#include "DistinctRewriter.h"
 #include "LATheory.h"
 #include "OsmtInternalException.h"
-#include "Substitutor.h"
+#include "Rewritings.h"
 #include "TreeOps.h"
 
+using namespace opensmt::rewritings;
+
 PTRef UFLATheory::preprocessAfterSubstitutions(PTRef fla, PreprocessingContext const &) {
     fla = rewriteDistincts(getLogic(), fla);
     fla = rewriteDivMod<ArithLogic>(logic, fla);
diff --git a/src/logics/UFTheory.cc b/src/logics/UFTheory.cc
index 7b231b39e..b24a4cef9 100644
--- a/src/logics/UFTheory.cc
+++ b/src/logics/UFTheory.cc
@@ -1,6 +1,8 @@
 #include "Theory.h"
 #include "TreeOps.h"
-#include "DistinctRewriter.h"
+#include "Rewritings.h"
+
+using namespace opensmt::rewritings;
 
 PTRef UFTheory::preprocessBeforeSubstitutions(PTRef fla, PreprocessingContext const & context) {
     return context.perPartition ? fla : getLogic().mkAnd(fla, getLogic().learnEqTransitivity(fla));
diff --git a/src/rewriters/CMakeLists.txt b/src/rewriters/CMakeLists.txt
index 2b9f2087e..0570a93d9 100644
--- a/src/rewriters/CMakeLists.txt
+++ b/src/rewriters/CMakeLists.txt
@@ -1,12 +1,12 @@
 add_library(rewriters OBJECT "")
 
 target_sources(rewriters
-    PUBLIC "${CMAKE_CURRENT_SOURCE_DIR}/DistinctRewriter.cc"
+    PUBLIC "${CMAKE_CURRENT_SOURCE_DIR}/Rewritings.cc"
 )
 
 install(FILES
     Substitutor.h
     Rewriter.h
-    DivModRewriter.h
+    Rewritings.h
     DESTINATION ${INSTALL_HEADERS_DIR}
     )
diff --git a/src/rewriters/DistinctRewriter.cc b/src/rewriters/DistinctRewriter.cc
deleted file mode 100644
index 9e92240e8..000000000
--- a/src/rewriters/DistinctRewriter.cc
+++ /dev/null
@@ -1,18 +0,0 @@
-/*
- * Copyright (c) 2021-2022, Martin Blicha <martin.blicha@gmail.com>
- *
- *  SPDX-License-Identifier: MIT
- *
- */
-
-#include "DistinctRewriter.h"
-#include "TreeOps.h"
-
-PTRef rewriteDistinctsKeepTopLevel(Logic & logic, PTRef fla) {
-    vec<PTRef> topLevelConjuncts = ::topLevelConjuncts(logic, fla);
-    KeepTopLevelDistinctRewriter::TopLevelDistincts topLevelDistincts;
-    for (PTRef conj : topLevelConjuncts) {
-        if (logic.isDisequality(conj)) { topLevelDistincts.insert(conj); }
-    }
-    return KeepTopLevelDistinctRewriter(logic, std::move(topLevelDistincts)).rewrite(fla);
-}
diff --git a/src/rewriters/DistinctRewriter.h b/src/rewriters/DistinctRewriter.h
index 89d51e67b..1a6f7877a 100644
--- a/src/rewriters/DistinctRewriter.h
+++ b/src/rewriters/DistinctRewriter.h
@@ -73,10 +73,6 @@ class KeepTopLevelDistinctRewriter : public Rewriter<KeepTopLevelDistinctRewrite
         : Rewriter<KeepTopLevelDistinctRewriteConfig>(logic, config), config(logic, std::move(topLevelDistincts)) {}
 };
 
-inline PTRef rewriteDistincts(Logic & logic, PTRef fla) {
-    return DistinctRewriter(logic).rewrite(fla);
-}
 
-PTRef rewriteDistinctsKeepTopLevel(Logic & logic, PTRef fla);
 
 #endif // OPENSMT_DISTINCTREWRITER_H
diff --git a/src/rewriters/DivModRewriter.h b/src/rewriters/DivModRewriter.h
index c879dc20d..798058857 100644
--- a/src/rewriters/DivModRewriter.h
+++ b/src/rewriters/DivModRewriter.h
@@ -1,5 +1,5 @@
 /*
- * Copyright (c) 2021-2022, Martin Blicha <martin.blicha@gmail.com>
+ * Copyright (c) 2021-2024, Martin Blicha <martin.blicha@gmail.com>
  *
  *  SPDX-License-Identifier: MIT
  *
@@ -8,17 +8,10 @@
 #ifndef OPENSMT_DIVMODREWRITER_H
 #define OPENSMT_DIVMODREWRITER_H
 
-#include "Rewriter.h"
-
 #include "ArithLogic.h"
-#include "PTRef.h"
-
-#include "OsmtApiException.h"
 #include "OsmtInternalException.h"
-#include "TypeUtils.h"
+#include "Rewriter.h"
 
-#include <string>
-#include <unordered_map>
 
 class DivModConfig : public DefaultRewriterConfig {
     ArithLogic & logic;
@@ -64,7 +57,7 @@ class DivModConfig : public DefaultRewriterConfig {
     static std::string_view constexpr divPrefix = ".div";
     static std::string_view constexpr modPrefix = ".mod";
 
-    DivModConfig(ArithLogic & logic) : logic(logic) {}
+    explicit DivModConfig(ArithLogic & logic) : logic(logic) {}
 
     PTRef rewrite(PTRef term) override {
         SymRef symRef = logic.getSymRef(term);
@@ -125,7 +118,7 @@ class DivModRewriter : Rewriter<DivModConfig> {
     DivModConfig config;
 
 public:
-    DivModRewriter(ArithLogic & logic) : Rewriter<DivModConfig>(logic, config), logic(logic), config(logic) {}
+    explicit DivModRewriter(ArithLogic & logic) : Rewriter<DivModConfig>(logic, config), logic(logic), config(logic) {}
 
     PTRef rewrite(PTRef term) override {
         if (term == PTRef_Undef or not logic.hasSortBool(term)) {
@@ -139,9 +132,4 @@ class DivModRewriter : Rewriter<DivModConfig> {
     }
 };
 
-// Simple single-use version
-inline PTRef rewriteDivMod(ArithLogic & logic, PTRef root) {
-    return DivModRewriter(logic).rewrite(root);
-}
-
-#endif // OPENSMT_DIVMODEREWRITER_H
+#endif // OPENSMT_DIVMODREWRITER_H
diff --git a/src/rewriters/Rewritings.cc b/src/rewriters/Rewritings.cc
new file mode 100644
index 000000000..37d3d0a2c
--- /dev/null
+++ b/src/rewriters/Rewritings.cc
@@ -0,0 +1,43 @@
+/*
+ * Copyright (c) 2024 Martin Blicha <martin.blicha@gmail.com>
+ *
+ *  SPDX-License-Identifier: MIT
+ *
+ */
+
+#include "Rewritings.h"
+
+#include "DistinctRewriter.h"
+#include "DivModRewriter.h"
+#include "TreeOps.h"
+
+namespace opensmt::rewritings {
+
+    PTRef rewriteDistincts(Logic & logic, PTRef fla) {
+        return DistinctRewriter(logic).rewrite(fla);
+    }
+
+    PTRef rewriteDistinctsKeepTopLevel(Logic & logic, PTRef fla) {
+        vec<PTRef> topLevelConjuncts = ::topLevelConjuncts(logic, fla);
+        KeepTopLevelDistinctRewriter::TopLevelDistincts topLevelDistincts;
+        for (PTRef conj : topLevelConjuncts) {
+            if (logic.isDisequality(conj)) { topLevelDistincts.insert(conj); }
+        }
+        return KeepTopLevelDistinctRewriter(logic, std::move(topLevelDistincts)).rewrite(fla);
+    }
+
+    PTRef rewriteDivMod(ArithLogic & logic, PTRef term) {
+        return DivModRewriter(logic).rewrite(term);
+    }
+
+    std::optional<PTRef> tryGetOriginalDivModTerm(ArithLogic & logic, PTRef tr) {
+        if (not logic.isVar(tr)) return std::nullopt; // Only variables can match
+        auto symName = std::string_view(logic.getSymName(tr));
+        if (symName.compare(0, DivModConfig::divPrefix.size(), DivModConfig::divPrefix) == 0) {
+            return DivModConfig::getDivTermFor(logic, tr);
+        } else if (symName.compare(0, DivModConfig::modPrefix.size(), DivModConfig::modPrefix) == 0) {
+            return DivModConfig::getModTermFor(logic, tr);
+        }
+        return std::nullopt;
+    }
+}
\ No newline at end of file
diff --git a/src/rewriters/Rewritings.h b/src/rewriters/Rewritings.h
new file mode 100644
index 000000000..3443c867b
--- /dev/null
+++ b/src/rewriters/Rewritings.h
@@ -0,0 +1,28 @@
+/*
+ * Copyright (c) 2024 Martin Blicha <martin.blicha@gmail.com>
+ *
+ *  SPDX-License-Identifier: MIT
+ *
+ */
+
+#ifndef OPENSMT_REWRITINGS_H
+#define OPENSMT_REWRITINGS_H
+
+#include "ArithLogic.h"
+#include "PTRef.h"
+
+#include <optional>
+
+namespace opensmt::rewritings {
+
+    PTRef rewriteDistincts(Logic & logic, PTRef fla);
+
+    PTRef rewriteDistinctsKeepTopLevel(Logic & logic, PTRef fla);
+
+    PTRef rewriteDivMod(ArithLogic & logic, PTRef fla);
+
+    std::optional<PTRef> tryGetOriginalDivModTerm(ArithLogic & logic, PTRef term);
+
+} // opensmt::rewritings
+
+#endif // OPENSMT_REWRITINGS_H
diff --git a/test/unit/test_LIALogicMkTerms.cc b/test/unit/test_LIALogicMkTerms.cc
index 6bc4fd0c5..3b663c161 100644
--- a/test/unit/test_LIALogicMkTerms.cc
+++ b/test/unit/test_LIALogicMkTerms.cc
@@ -3,9 +3,9 @@
 //
 
 #include <gtest/gtest.h>
-#include <ArithLogic.h>
-#include "DivModRewriter.h"
+#include "ArithLogic.h"
 #include "IteHandler.h"
+#include "Rewritings.h"
 #include "TreeOps.h"
 
 #include <algorithm>
@@ -194,27 +194,10 @@ TEST_F(LIALogicMkTermsTest, test_EqualityNormalization_EqualityToConstant) {
 }
 
 TEST_F(LIALogicMkTermsTest, test_ReverseAuxRewrite) {
-
-    static constexpr std::initializer_list<std::string_view> prefixes = {IteHandler::itePrefix, DivModConfig::divPrefix, DivModConfig::modPrefix};
-
-
     auto hasAuxSymbols = [this](PTRef tr) {
-        class AuxSymbolMatcher {
-            ArithLogic const & logic;
-
-        public:
-            AuxSymbolMatcher(ArithLogic const & logic) : logic(logic) {}
-            bool operator()(PTRef tr) {
-                std::string_view const name = logic.getSymName(tr);
-                return std::any_of(prefixes.begin(), prefixes.end(), [&name](std::string_view const prefix) {
-                    return name.compare(0, prefix.size(), prefix) == 0;
-                });
-            };
-        };
-        auto predicate = AuxSymbolMatcher(logic);
-        auto config = TermCollectorConfig(predicate);
-        TermVisitor(logic, config).visit(tr);
-        return config.extractCollectedTerms().size() > 0;
+        auto auxiliaryVarsInTerm = matchingSubTerms(logic, tr, [&](PTRef subTerm) {
+            return opensmt::rewritings::tryGetOriginalDivModTerm(logic, subTerm).has_value(); });
+        return auxiliaryVarsInTerm.size() > 0;
     };
 
     PTRef a = logic.mkIntVar("a");
@@ -231,8 +214,7 @@ TEST_F(LIALogicMkTermsTest, test_ReverseAuxRewrite) {
     PTRef nested = logic.mkEq(logic.getTerm_IntZero(), logic.mkMod(ite, c));
 
     for (PTRef tr : {term, eq, nested}) {
-
-        PTRef termWithAux = DivModRewriter(logic).rewrite(IteHandler(logic).rewrite(tr));
+        PTRef termWithAux = opensmt::rewritings::rewriteDivMod(logic, IteHandler(logic).rewrite(tr));
         ASSERT_TRUE(hasAuxSymbols(termWithAux));
 
         PTRef termWithoutAux = logic.removeAuxVars(termWithAux);
diff --git a/test/unit/test_Rewriting.cc b/test/unit/test_Rewriting.cc
index afda50c45..b68f087fc 100644
--- a/test/unit/test_Rewriting.cc
+++ b/test/unit/test_Rewriting.cc
@@ -1,18 +1,22 @@
-//
-// Created by Martin Blicha on 17.05.20.
-//
+/*
+ * Copyright (c) 2020-2024 Martin Blicha <martin.blicha@gmail.com>
+ *
+ *  SPDX-License-Identifier: MIT
+ *
+ */
 
 #include <gtest/gtest.h>
-#include <ArithLogic.h>
-#include <BoolRewriting.h>
-#include <Logic.h>
-#include <ArithmeticEqualityRewriter.h>
-#include <DivModRewriter.h>
-#include <MainSolver.h>
-#include <DistinctRewriter.h>
+
+#include "ArithLogic.h"
+#include "BoolRewriting.h"
+#include "Logic.h"
+#include "ArithmeticEqualityRewriter.h"
+#include "MainSolver.h"
+#include "Rewritings.h"
 
 #include <algorithm>
 
+using namespace opensmt::rewritings;
 
 TEST(Rewriting_test, test_RewriteClassicConjunction)
 {
@@ -79,7 +83,7 @@ TEST(Rewriting_test, test_RewriteDivMod) {
     PTRef div = logic.mkIntDiv(x,two);
     PTRef mod = logic.mkMod(x,two);
     PTRef fla = logic.mkAnd(logic.mkEq(div, two), logic.mkEq(mod, logic.getTerm_IntZero()));
-    PTRef rewritten = DivModRewriter(logic).rewrite(fla);
+    PTRef rewritten = rewriteDivMod(logic, fla);
 //    std::cout << logic.printTerm(rewritten) << std::endl;
     SMTConfig config;
     MainSolver solver(logic, config, "test");
@@ -112,16 +116,16 @@ class RewriteDistinctTest : public ::testing::Test {
 TEST_F(RewriteDistinctTest, test_RewriteDistinct_TopLevel) {
     PTRef dist = logic.mkDistinct({x, y, z});
     PTRef fla = logic.mkAnd(b, dist); // dist is top-level distinct
-    EXPECT_NE(::rewriteDistincts(logic, fla), fla); // fla should be rewritten
-    EXPECT_EQ(::rewriteDistinctsKeepTopLevel(logic, fla), fla); // fla should be kept the same
+    EXPECT_NE(rewriteDistincts(logic, fla), fla); // fla should be rewritten
+    EXPECT_EQ(rewriteDistinctsKeepTopLevel(logic, fla), fla); // fla should be kept the same
 }
 
 TEST_F(RewriteDistinctTest, test_RewriteDistinct_Negated) {
     PTRef dist = logic.mkDistinct({x, y, z});
     PTRef fla = logic.mkNot(dist); // dist is not top-level distinct
-    PTRef rewritten1 = ::rewriteDistincts(logic, fla);
+    PTRef rewritten1 = rewriteDistincts(logic, fla);
     EXPECT_NE(rewritten1, fla); // fla should be rewritten
-    PTRef rewritten2 = ::rewriteDistinctsKeepTopLevel(logic, fla);
+    PTRef rewritten2 = rewriteDistinctsKeepTopLevel(logic, fla);
     EXPECT_NE(rewritten2, fla); // fla should be rewritten
     EXPECT_EQ(rewritten1, rewritten2);
     ASSERT_TRUE(logic.isNot(rewritten1));