diff --git a/README.md b/README.md
index 3bea344273..173cf29878 100644
--- a/README.md
+++ b/README.md
@@ -19,7 +19,7 @@ For a brief overview of the architecture, see [SMT-COMP'24 Z3-Noodler descriptio
 
 ### Dependencies
 
-1) The [Mata](https://github.com/VeriFIT/mata/) library for efficient handling of finite automata. Minimum required version of `mata` is `v1.6.10`.
+1) The [Mata](https://github.com/VeriFIT/mata/) library for efficient handling of finite automata. Minimum required version of `mata` is `v1.7.6`.
     ```shell
     git clone 'https://github.com/VeriFIT/mata.git'
     cd mata
diff --git a/src/smt/theory_str_noodler/formula.cpp b/src/smt/theory_str_noodler/formula.cpp
index 9d7ae7030c..3e5f408ea7 100644
--- a/src/smt/theory_str_noodler/formula.cpp
+++ b/src/smt/theory_str_noodler/formula.cpp
@@ -190,7 +190,7 @@ namespace smt::noodler {
     }
 
     std::set<BasicTerm> Predicate::get_side_vars(const Predicate::EquationSideType side) const {
-        assert(is_eq_or_ineq());
+        assert(is_two_sided());
         std::set<BasicTerm> vars;
         std::vector<BasicTerm> side_terms;
         switch (side) {
@@ -221,7 +221,7 @@ namespace smt::noodler {
     }
 
     bool Predicate::mult_occurr_var_side(const Predicate::EquationSideType side) const {
-        assert(is_eq_or_ineq());
+        assert(is_two_sided());
         const auto terms_begin{ get_side(side).cbegin() };
         const auto terms_end{ get_side(side).cend() };
         for (auto term_iter{ terms_begin }; term_iter < terms_end; ++term_iter) {
@@ -262,40 +262,39 @@ namespace smt::noodler {
     }
 
     std::string Predicate::to_string() const {
+
+        // joining BasicTerm in the given vector with str
+        auto join = [&](const std::vector<BasicTerm>& vec, const std::string& str) -> std::string {
+            if(vec.empty()) return "";
+            std::string ret = vec[0].to_string();
+            for(size_t i = 1; i < vec.size(); i++) {
+                ret += str + vec[i].to_string();
+            }
+            return ret;
+        };
+
         switch (type) {
             case PredicateType::Equation: {
-                std::string result{ "Equation:" };
-                for (const auto& item: get_left_side()) {
-                    result += " " + item.to_string();
-                }
-                result += " =";
-                for (const auto& item: get_right_side()) {
-                    result += " " + item.to_string();
-                }
+                std::string result{ "Equation: " };
+                result += join(get_left_side(), " ") + " = " + join(get_right_side(), " ");
                 return result;
             }
 
             case PredicateType::Inequation: {
-                std::string result{ "Inequation:" };
-                for (const auto& item: get_left_side()) {
-                    result += " " + item.to_string();
-                }
-                result += " !=";
-                for (const auto& item: get_right_side()) {
-                    result += " " + item.to_string();
-                }
+                std::string result{ "Inequation: " };
+                result += join(get_left_side(), " ") + " != " + join(get_right_side(), " ");
                 return result;
             }
 
             case PredicateType::NotContains: {
-                std::string result{ "Notcontains " };
-                for (const auto& item: params[0]) {
-                    result += " " + item.to_string();
-                }
-                result += " ,";
-                for (const auto& item: params[1]) {
-                    result += " " + item.to_string();
-                }
+                std::string result{ "Notcontains: " };
+                result += join(params[0], " ") + " , " + join(params[1], " ");
+                return result;
+            }
+
+            case PredicateType::Transducer: {
+                std::string result{ "Transducer: " };
+                result += join(params[0], " ") + " , " + join(params[1], " ");
                 return result;
             }
         }
@@ -305,16 +304,40 @@ namespace smt::noodler {
 
     bool Predicate::equals(const Predicate &other) const {
         if (type == other.type) {
+            if(is_transducer()) {
+                if(!(params[0] == other.params[0] && params[1] == other.params[1])) {
+                    return false;
+                }
+                // check if transducers are the same pointers
+                return transducer == other.transducer;
+            }
+            if (is_two_sided()) {
+                return params[0] == other.params[0] && params[1] == other.params[1];
+            }
+            return params == other.params;
+        }
+        return false;
+    }
+
+    bool Predicate::strong_equals(const Predicate& other) const {
+        if (type == other.type) {
+            if(is_transducer()) {
+                if(!(params[0] == other.params[0] && params[1] == other.params[1])) {
+                    return false;
+                }
+                // check if transducers are the same pointers
+                return transducer->is_identical(*other.get_transducer());
+            }
             if (is_two_sided()) {
                 return params[0] == other.params[0] && params[1] == other.params[1];
             }
-            return true;
+            return params == other.params;
         }
         return false;
     }
 
     const std::vector<BasicTerm> &Predicate::get_side(const Predicate::EquationSideType side) const {
-        assert(is_eq_or_ineq());
+        assert(is_two_sided());
         switch (side) {
             case EquationSideType::Left:
                 return params[0];
@@ -329,7 +352,7 @@ namespace smt::noodler {
     }
 
     std::vector<BasicTerm> &Predicate::get_side(const Predicate::EquationSideType side) {
-        assert(is_eq_or_ineq());
+        assert(is_two_sided());
         switch (side) {
             case EquationSideType::Left:
                 return params[0];
diff --git a/src/smt/theory_str_noodler/formula.h b/src/smt/theory_str_noodler/formula.h
index 4e196ce0cd..d327472f2e 100644
--- a/src/smt/theory_str_noodler/formula.h
+++ b/src/smt/theory_str_noodler/formula.h
@@ -24,6 +24,7 @@
 #include <map>
 #include <unordered_set>
 #include <iostream>
+#include <mata/nft/nft.hh>
 
 #include "util/zstring.h"
 #include "ast/ast.h"
@@ -35,6 +36,7 @@ namespace smt::noodler {
         Equation,
         Inequation,
         NotContains,
+        Transducer, 
     };
 
     [[nodiscard]] static std::string to_string(PredicateType predicate_type) {
@@ -45,6 +47,8 @@ namespace smt::noodler {
                 return "Inequation";
             case PredicateType::NotContains:
                 return "Notcontains";
+            case PredicateType::Transducer:
+                return "Transducer";
         }
 
         throw std::runtime_error("Unhandled predicate type passed to to_string().");
@@ -290,7 +294,7 @@ namespace smt::noodler {
         };
 
         Predicate() : type(PredicateType::Equation) {}
-        explicit Predicate(const PredicateType type): type(type) {
+        explicit Predicate(const PredicateType type): type(type), params(), transducer() {
             if (is_equation() || is_inequation()) {
                 params.resize(2);
                 params.emplace_back();
@@ -300,15 +304,25 @@ namespace smt::noodler {
 
         explicit Predicate(const PredicateType type, std::vector<std::vector<BasicTerm>> par):
             type(type),
-            params(par)
+            params(par),
+            transducer()
             { }
 
+        explicit Predicate(const PredicateType type, std::vector<std::vector<BasicTerm>> par, std::shared_ptr<mata::nft::Nft> trans) : 
+            type(type),
+            params(par),
+            transducer(trans) {
+            assert(type == PredicateType::Transducer);
+            assert(trans->num_of_levels == 2);
+        }
+
         [[nodiscard]] PredicateType get_type() const { return type; }
         [[nodiscard]] bool is_equation() const { return type == PredicateType::Equation; }
         [[nodiscard]] bool is_inequation() const { return type == PredicateType::Inequation; }
         [[nodiscard]] bool is_not_cont() const { return type == PredicateType::NotContains; }
         [[nodiscard]] bool is_eq_or_ineq() const { return is_equation() || is_inequation(); }
-        [[nodiscard]] bool is_two_sided() const { return is_equation() || is_inequation() || is_not_cont(); }
+        [[nodiscard]] bool is_transducer() const { return is(PredicateType::Transducer); }
+        [[nodiscard]] bool is_two_sided() const { return is_equation() || is_inequation() || is_not_cont() || is_transducer(); }
         [[nodiscard]] bool is_predicate() const { return !is_eq_or_ineq(); }
         [[nodiscard]] bool is(const PredicateType predicate_type) const { return predicate_type == this->type; }
 
@@ -364,7 +378,7 @@ namespace smt::noodler {
         }
 
         std::set<BasicTerm> get_left_set() const {
-            assert(is_eq_or_ineq());
+            assert(is_two_sided());
             std::set<BasicTerm> ret;
             for(const BasicTerm& t : this->params[0])
                 ret.insert(t);
@@ -372,7 +386,7 @@ namespace smt::noodler {
         }
 
         std::set<BasicTerm> get_right_set() const {
-            assert(is_eq_or_ineq());
+            assert(is_two_sided());
             std::set<BasicTerm> ret;
             for(const BasicTerm& t : this->params[1])
                 ret.insert(t);
@@ -413,6 +427,7 @@ namespace smt::noodler {
                 return LenNode(LenFormulaType::PLUS, ops);
             };
 
+            assert(is_eq_or_ineq());
             LenNode left = plus_chain(this->params[0]);
             LenNode right = plus_chain(this->params[1]);
             LenNode eq = LenNode(LenFormulaType::EQ, {left, right});
@@ -429,7 +444,12 @@ namespace smt::noodler {
         [[nodiscard]] const std::vector<BasicTerm>& get_side(EquationSideType side) const;
 
         [[nodiscard]] Predicate get_switched_sides_predicate() const {
-            assert(is_eq_or_ineq());
+            assert(is_two_sided());
+            // for transducers we need to invert tapes, i.e., T(x,y) iff T^{-1}(y,x)
+            if(is_transducer()) {
+                auto nft_inverse = std::make_shared<mata::nft::Nft>(mata::nft::invert_levels(*transducer));
+                return Predicate{ PredicateType::Transducer, { get_right_side(), get_left_side() }, nft_inverse };
+            }
             return Predicate{ type, { get_right_side(), get_left_side() } };
         }
 
@@ -479,6 +499,7 @@ namespace smt::noodler {
                 modif = modif || r;
             }
             res = Predicate(this->type, new_params);
+            res.transducer = this->transducer;
             return modif;
         }
 
@@ -530,29 +551,47 @@ namespace smt::noodler {
 
         [[nodiscard]] bool equals(const Predicate& other) const;
 
+        /**
+         * @brief Strong equality. For the case of transducer predicates the transducers
+         * are compared for identity (not just the indentity of pointers). It is 
+         * necessary for the inclusion graph handling where we require get_switched_side
+         * (get_swithch_side(x)) == x (which is not true for pointer comparison).
+         * 
+         * @param other Other predicate
+         * @return true Is strongly equal
+         */
+        bool strong_equals(const Predicate& other) const;
+
         [[nodiscard]] std::string to_string() const;
 
         struct HashFunction {
             size_t operator()(const Predicate& predicate) const {
                 size_t res{};
                 size_t row_hash = std::hash<PredicateType>()(predicate.type);
-                for (const auto& term: predicate.get_left_side()) {
-                    size_t col_hash = BasicTerm::HashFunction()(term) << 1;
-                    res ^= col_hash;
-                }
-                for (const auto& term: predicate.get_right_side()) {
-                    size_t col_hash = BasicTerm::HashFunction()(term) << 1;
-                    res ^= col_hash;
+                for(const auto& pr : predicate.get_params()) {
+                    for(const BasicTerm& term : pr) {
+                        size_t col_hash = BasicTerm::HashFunction()(term) << 1;
+                        res ^= col_hash;
+                    }
                 }
                 return row_hash ^ res;
             }
         };
 
-        // TODO: Additional operations.
+        /**
+         * @brief Get the transducer shared pointer (for the transducer predicates only).
+         * 
+         * @return std::shared_ptr<mata::nft::Nft> Transducer
+         */
+        const std::shared_ptr<mata::nft::Nft>& get_transducer() const {
+            assert(is_transducer());
+            return transducer;
+        }
 
     private:
         PredicateType type;
         std::vector<std::vector<BasicTerm>> params;
+        std::shared_ptr<mata::nft::Nft> transducer; // transducer for the case of PredicateType::Transducer
 
         // TODO: Add additional attributes such as cost, etc.
     }; // Class Predicate.
@@ -578,9 +617,14 @@ namespace smt::noodler {
         if (lhs.get_params() < rhs.get_params()) {
             return true;
         }
+        // For transducer predicates we compare pointers (assuming linear memory model)
+        if (lhs.is_transducer()) {
+            // compare pointers
+            return lhs.get_transducer() < rhs.get_transducer();
+        }
         return false;
     }
-    static bool operator>(const Predicate& lhs, const Predicate& rhs) { return !(lhs < rhs); }
+    static bool operator>(const Predicate& lhs, const Predicate& rhs) { return !(lhs < rhs) && lhs != rhs; }
 
     //----------------------------------------------------------------------------------------------------------------------------------
 
diff --git a/src/smt/theory_str_noodler/formula_preprocess.cpp b/src/smt/theory_str_noodler/formula_preprocess.cpp
index 18608f3724..40f6ec4acc 100644
--- a/src/smt/theory_str_noodler/formula_preprocess.cpp
+++ b/src/smt/theory_str_noodler/formula_preprocess.cpp
@@ -187,7 +187,7 @@ namespace smt::noodler {
     void FormulaVar::remove_predicate(size_t index) {
         std::set<BasicTerm> items = this->predicates[index].get_set();
 
-        const auto& filter = [&index](const VarNode& n) { return n.eq_index == index; };
+        const auto& filter = [&index](const VarNode& n) { return n.pred_index == index; };
         for(const BasicTerm& v : items) {
             std::set<VarNode>& occurr = this->varmap[v];
             remove_if(occurr, filter);
@@ -367,10 +367,10 @@ namespace smt::noodler {
             std::set<VarNode> occurrs = this->formula.get_var_occurr(left_var);
             if(occurrs.size() == 1) {
                 Predicate reg_pred;
-                if(this->formula.is_side_regular(this->formula.get_predicate(occurrs.begin()->eq_index), reg_pred)) {
-                    worklist.emplace_back(occurrs.begin()->eq_index, reg_pred);
+                if(this->formula.is_side_regular(this->formula.get_predicate(occurrs.begin()->pred_index), reg_pred)) {
+                    worklist.emplace_back(occurrs.begin()->pred_index, reg_pred);
                     // update dependency
-                    map_set_insert(this->dependency, occurrs.begin()->eq_index, pr.first);
+                    map_set_insert(this->dependency, occurrs.begin()->pred_index, pr.first);
                 }
             }
         }
@@ -625,7 +625,7 @@ namespace smt::noodler {
             // Get all occurrences of t
             std::set<VarNode> occurrs = this->formula.get_var_occurr(t);
             // Get predicate of a first equation containing t; and side containing t
-            Predicate act_pred = this->formula.get_predicate(occurrs.begin()->eq_index);
+            Predicate act_pred = this->formula.get_predicate(occurrs.begin()->pred_index);
             Concat side = occurrs.begin()->position > 0 ? act_pred.get_right_side() : act_pred.get_left_side();
 
             int start = std::abs(occurrs.begin()->position) - 1;
@@ -635,7 +635,7 @@ namespace smt::noodler {
                 for(const VarNode& vn : occurrs) {
                     vns.insert({
                         side[i],
-                        vn.eq_index,
+                        vn.pred_index,
                         FormulaVar::increment_side_index(vn.position, i-start)
                     });
                 }
@@ -728,7 +728,7 @@ namespace smt::noodler {
         for(const BasicTerm& t : eps_set) {
             std::set<VarNode> nds = get_formula().get_var_occurr(t);
             std::transform(nds.begin(), nds.end(), std::back_inserter(worklist),
-                [](const VarNode& n){ return n.eq_index ; });
+                [](const VarNode& n){ return n.pred_index ; });
         }
 
         while(!worklist.empty()) {
@@ -757,7 +757,7 @@ namespace smt::noodler {
                 eps_set.insert(t);
                 std::set<VarNode> nds = get_formula().get_var_occurr(t);
                 std::transform(nds.begin(), nds.end(), std::back_inserter(worklist),
-                    [](const VarNode& n){ return n.eq_index ; });
+                    [](const VarNode& n){ return n.pred_index ; });
             }
         }
 
diff --git a/src/smt/theory_str_noodler/formula_preprocess.h b/src/smt/theory_str_noodler/formula_preprocess.h
index 56fe051469..a00db8a524 100644
--- a/src/smt/theory_str_noodler/formula_preprocess.h
+++ b/src/smt/theory_str_noodler/formula_preprocess.h
@@ -196,33 +196,33 @@ namespace smt::noodler {
      */
     struct VarNode {
         BasicTerm term;
-        size_t eq_index;
+        size_t pred_index;
         int position;
 
-        VarNode(BasicTerm term, const size_t eq_index, const int position): term{ std::move(term) }, eq_index{ eq_index }, position{ position } {}
+        VarNode(BasicTerm term, const size_t eq_index, const int position): term{ std::move(term) }, pred_index{ eq_index }, position{ position } {}
         VarNode(const VarNode& other) = default;
         VarNode(VarNode &&) = default;
 
         VarNode& operator=(const VarNode&) = default;
 
         bool operator==(const VarNode& other) const {
-            return term == other.term && eq_index == other.eq_index && position == other.position;
+            return term == other.term && pred_index == other.pred_index && position == other.position;
         }
 
         std::string to_string() const {
             std::string ret;
-            ret += "( " + term.to_string() + ";" + std::to_string(eq_index) + ";" + std::to_string(position) + ")";
+            ret += "( " + term.to_string() + ";" + std::to_string(pred_index) + ";" + std::to_string(position) + ")";
             return ret;
         };
     };
 
     inline bool operator<(const VarNode& lhs, const VarNode& rhs) {
         if(lhs.position == rhs.position) {
-            if(lhs.eq_index == rhs.eq_index) {
+            if(lhs.pred_index == rhs.pred_index) {
                 if(lhs.term == rhs.term) return false;
                 return lhs.term < rhs.term;
             }
-            return lhs.eq_index < rhs.eq_index;
+            return lhs.pred_index < rhs.pred_index;
         }
         return lhs.position < rhs.position;
     }
diff --git a/src/smt/theory_str_noodler/inclusion_graph.cc b/src/smt/theory_str_noodler/inclusion_graph.cc
index ca6a3ea299..5ccf5d68e2 100644
--- a/src/smt/theory_str_noodler/inclusion_graph.cc
+++ b/src/smt/theory_str_noodler/inclusion_graph.cc
@@ -23,25 +23,34 @@ namespace {
      * @return String representation of @p node.
      */
     std::string conv_node_to_string(const std::shared_ptr<GraphNode>& node) {
+        // joining BasicTerm in the given vector with str
+        auto join = [&](const std::vector<BasicTerm>& vec, const std::string& str) -> std::string {
+            if(vec.empty()) return "";
+            std::string ret = vec[0].to_string();
+            for(size_t i = 1; i < vec.size(); i++) {
+                ret += str + vec[i].to_string();
+            }
+            return ret;
+        };
+
         auto& predicate{ node->get_predicate() };
         std::string result{};
         switch (predicate.get_type()) {
             case PredicateType::NotContains: {
                 util::throw_error("Decision procedure can handle only equations and disequations");
             }
+ 
+            case PredicateType::Transducer: {
+                std::string left_side = join(predicate.get_left_side(), " ");
+                std::string right_side = join(predicate.get_right_side(), " ");
+                result = "T(" + left_side + ", " + right_side + ")";
+                break;
+            }
+
             case PredicateType::Equation:
             case PredicateType::Inequation: {
-                std::string left_side{};
-                for (auto& item : predicate.get_left_side()) {
-                    if (!left_side.empty()) { left_side += " "; }
-                    left_side += item.to_string();
-                }
-
-                std::string right_side{};
-                for (auto& item : predicate.get_right_side()) {
-                    if (!right_side.empty()) { right_side += " "; }
-                    right_side += item.to_string();
-                }
+                std::string left_side = join(predicate.get_left_side(), " ");
+                std::string right_side = join(predicate.get_right_side(), " ");
                 result = left_side;
                 if (predicate.get_type() == PredicateType::Inequation) {
                     result += " !";
@@ -158,7 +167,7 @@ Graph smt::noodler::Graph::create_simplified_splitting_graph(const Formula& form
     // Add all nodes which are not already present in direct and switched form.
     for (const auto& predicate: formula.get_predicates()) {
         // we skip trivial equations of the form x = x
-        if(predicate.get_left_side() == predicate.get_right_side()) {
+        if(!predicate.is_transducer() && predicate.get_left_side() == predicate.get_right_side()) {
             continue;
         }
         graph.add_node(predicate);
@@ -180,16 +189,11 @@ Graph smt::noodler::Graph::create_simplified_splitting_graph(const Formula& form
 
             if (!have_same_var(source_left_side, target_right_side)) {
                 continue;
-            } else if (source_left_side == target_right_side) {
+            } else if (source_predicate.strong_equals(target_predicate.get_switched_sides_predicate())) {
                 // Have same var and sides are equal.
-
-                if (source_right_side == target_left_side) { // In the same equation.
-                    if (!source_predicate.mult_occurr_var_side(Predicate::EquationSideType::Left)) {
-                        // Does not have multiple occurrences of one var. Hence, cannot have an edge.
-                        continue;
-                    }
-                } else {
-                    // In different equation.
+                if (!source_predicate.mult_occurr_var_side      (Predicate::EquationSideType::Left)) {
+                    // Does not have multiple occurrences of one var. Hence, cannot have an edge.
+                    continue;
                 }
             } else {
                 // Have same var and sides are not equal, automatically add a new edge.
diff --git a/src/smt/theory_str_noodler/inclusion_graph.h b/src/smt/theory_str_noodler/inclusion_graph.h
index 195804305a..e7f0c7dfd4 100644
--- a/src/smt/theory_str_noodler/inclusion_graph.h
+++ b/src/smt/theory_str_noodler/inclusion_graph.h
@@ -28,7 +28,7 @@ namespace smt::noodler {
         };
 
         [[nodiscard]] bool equals(const GraphNode& other) const {
-            return this->node_predicate == other.node_predicate;
+            return this->node_predicate.strong_equals(other.node_predicate);
         }
 
     private:
@@ -152,7 +152,7 @@ namespace smt::noodler {
         }
 
         std::shared_ptr<GraphNode> get_node(const Predicate& predicate) {
-            auto node = std::find_if(nodes.begin(), nodes.end(), [&predicate](const std::shared_ptr<GraphNode> &el){ return (el->get_predicate() == predicate);});
+            auto node = std::find_if(nodes.begin(), nodes.end(), [&predicate](const std::shared_ptr<GraphNode> &el){ return (el->get_predicate().strong_equals(predicate));});
             if (node == nodes.end()) { return nullptr; }
             return *node;
         }
diff --git a/src/smt/theory_str_noodler/regex.cpp b/src/smt/theory_str_noodler/regex.cpp
index 9a3758744c..e465327f09 100644
--- a/src/smt/theory_str_noodler/regex.cpp
+++ b/src/smt/theory_str_noodler/regex.cpp
@@ -707,4 +707,79 @@ namespace smt::noodler::regex {
             throw regex_model_fail();
         }
     }
+
+    void gather_transducer_constraints(app* const ex, ast_manager& m, const seq_util& m_util_s, obj_map<expr, expr*>& pred_replace, std::map<BasicTerm, expr_ref>& var_name, mata::Alphabet* mata_alph, std::vector<Predicate>& transducer_preds) {
+        if(m_util_s.str.is_string(ex) || util::is_variable(ex)) { // Handle string literals.
+            return;
+        }
+
+        if(!m_util_s.str.is_concat(ex)) {
+            expr* rpl = pred_replace.find(ex); // dies if it is not found
+            // so-far we handle just replace_all
+            expr * a1 = nullptr, *a2 = nullptr, *a3 = nullptr;
+            if (m_util_s.str.is_replace_all(ex, a1, a2, a3)) {
+                zstring find, replace;
+                if(!m_util_s.str.is_string(a2, find) || !m_util_s.str.is_string(a3, replace)) {
+                    util::throw_error("only replace_all with concrete find&replace is supported");
+                }
+
+                // recursively call on nested parameters
+                gather_transducer_constraints(to_app(a1), m, m_util_s, pred_replace, var_name, mata_alph, transducer_preds);
+                // collect and replace replace_all argument with a concatenation of basic terms
+                std::vector<BasicTerm> side {};
+                util::collect_terms(to_app(a1), m, m_util_s, pred_replace, var_name, side);
+
+                // result of the replace_all
+                std::string var = to_app(rpl)->get_decl()->get_name().str();
+                BasicTerm bvar(BasicTermType::Variable, var);
+
+                // transducer corresponding to replace_all
+                mata::nft::Nft nft = mata::nft::strings::replace_reluctant_literal(util::get_mata_word_zstring(find), util::get_mata_word_zstring(replace), mata_alph);
+
+                // TODO: switch sides?
+                Predicate rpl_all(PredicateType::Transducer, { {bvar}, side }, std::make_shared<mata::nft::Nft>(nft));
+                transducer_preds.push_back(rpl_all);
+
+            // replace_re_all
+            } else if (m_util_s.str.is_replace_re_all(ex, a1, a2, a3)) {
+                zstring replace;
+                if(!m_util_s.str.is_string(a3, replace)) {
+                    util::throw_error("only replace_re_all with concrete find&replace is supported");
+                }
+
+                // construct NFA corresponding to the regex find
+                auto ov = mata_alph->get_alphabet_symbols();
+                std::set<mata::Symbol> syms(ov.begin(), ov.end());
+                Alphabet alph(syms);
+                mata::nfa::Nfa find_nfa = conv_to_nfa(to_app(a2), m_util_s, m, alph);
+
+                // recursively call on nested parameters
+                gather_transducer_constraints(to_app(a1), m, m_util_s, pred_replace, var_name, mata_alph, transducer_preds);
+                // collect and replace replace_all argument with a concatenation of basic terms
+                std::vector<BasicTerm> side {};
+                util::collect_terms(to_app(a1), m, m_util_s, pred_replace, var_name, side);
+
+                // result of the replace_all
+                std::string var = to_app(rpl)->get_decl()->get_name().str();
+                BasicTerm bvar(BasicTermType::Variable, var);
+
+                // transducer corresponding to replace_all
+                mata::nft::Nft nft = mata::nft::strings::replace_reluctant_regex(find_nfa, util::get_mata_word_zstring(replace), mata_alph);
+
+                // TODO: switch sides?
+                Predicate rpl_all(PredicateType::Transducer, { {bvar}, side }, std::make_shared<mata::nft::Nft>(nft));
+                transducer_preds.push_back(rpl_all);
+            }
+            // TODO: handle replace_re_all
+            return;
+        }
+
+        SASSERT(ex->get_num_args() == 2);
+        app *a_x = to_app(ex->get_arg(0));
+        app *a_y = to_app(ex->get_arg(1));
+        gather_transducer_constraints(a_x, m, m_util_s, pred_replace, var_name, mata_alph, transducer_preds);
+        gather_transducer_constraints(a_y, m, m_util_s, pred_replace, var_name, mata_alph,transducer_preds);
+
+    }
+
 }
diff --git a/src/smt/theory_str_noodler/regex.h b/src/smt/theory_str_noodler/regex.h
index f1c279d390..5d8429508a 100644
--- a/src/smt/theory_str_noodler/regex.h
+++ b/src/smt/theory_str_noodler/regex.h
@@ -156,6 +156,22 @@ namespace smt::noodler::regex {
      * @throws regex_model_fail if the model cannot be found (either regex represents empty language, or it contains intersection/complement/string variables, which this function currently cannot handle)
      */
     zstring get_model_from_regex(const app *regex, const seq_util& m_util_s);
+
+    /**
+     * @brief Gather transducer constraint (replace_all, replace_re_all) from a concatenation. Recursively applies also on 
+     * nested calls of replace_all, replace_re_all.
+     * 
+     * @param ex Concatenation of string terms.
+     * @param m AST manager
+     * @param m_util_s Seq util for AST.
+     * @param pred_replace Replacement of predicate and functions
+     * @param var_name Mapping of BasicTerm variables to z3 variables
+     * @param mata_alph Mata alphabet containing symbols from the current instance
+     * @param[out] transducer_preds Newly created transducer constraints
+     */
+    void gather_transducer_constraints(app* const ex, ast_manager& m, const seq_util& m_util_s, obj_map<expr, expr*>& pred_replace, 
+        std::map<BasicTerm, expr_ref>& var_name, mata::Alphabet* mata_alph, std::vector<Predicate>& transducer_preds);
+
 }
 
 #endif
diff --git a/src/smt/theory_str_noodler/theory_str_noodler.cpp b/src/smt/theory_str_noodler/theory_str_noodler.cpp
index 25daa48520..8d1e435197 100644
--- a/src/smt/theory_str_noodler/theory_str_noodler.cpp
+++ b/src/smt/theory_str_noodler/theory_str_noodler.cpp
@@ -156,7 +156,7 @@ namespace smt::noodler {
 
     void theory_str_noodler::string_theory_propagation(expr *expr, bool init, bool neg, bool var_lengths) {
         STRACE("str", tout << __LINE__ << " enter " << __FUNCTION__ << std::endl;);
-        STRACE("str", tout << mk_pp(expr, get_manager()) << std::endl;);
+        STRACE("str-propagation", tout << mk_pp(expr, get_manager()) << std::endl;);
 
         context &ctx = get_context();
 
@@ -399,11 +399,11 @@ namespace smt::noodler {
         } else if (m_util_s.str.is_replace(n)) { // str.replace
             handle_replace(n);
         } else if(m_util_s.str.is_replace_all(n)) { // str.replace_all
-            util::throw_error("str.replace_all is not supported");
+            handle_replace_all(n);
         } else if(m_util_s.str.is_replace_re(n)) { // str.replace_re
             handle_replace_re(n);
         } else if(m_util_s.str.is_replace_re_all(n)) { // str.replace_re_all
-            util::throw_error("str.replace_re_all is not supported");
+            handle_replace_re_all(n);
         } else if (m_util_s.str.is_is_digit(n)) { // str.is_digit
             handle_is_digit(n);
         } else if (
@@ -1502,6 +1502,54 @@ namespace smt::noodler {
         }
     }
 
+    /**
+     * @brief Handle replace_all. Just store the instance. It is solved using transducer 
+     * constraints in the final_check.
+     * 
+     * @param e replace_all
+     */
+    void theory_str_noodler::handle_replace_all(expr *e) {
+        STRACE("str", tout << "handle-replace-all: " << mk_pp(e, m) << '\n';);
+        if (axiomatized_persist_terms.contains(e))
+            return;
+
+        axiomatized_persist_terms.insert(e);
+
+        ast_manager &m = get_manager();
+        expr *s = nullptr, *i = nullptr, *l = nullptr;
+        VERIFY(m_util_s.str.is_replace_all(e, s, i, l));
+
+        expr_ref v = mk_str_var_fresh("replace_all");
+        // create equation for propagating length constraints
+        // tmp = replace_all(...) => |tmp| = |replace_all(...)|
+        add_axiom({mk_eq(v, e, false)});
+        this->predicate_replace.insert(e, v.get());  
+    }
+
+    /**
+     * @brief Handle replace_re_all. Just store the instance. It is solved using transducer 
+     * constraints in the final_check.
+     * 
+     * @param e replace_re_all
+     */
+    void theory_str_noodler::handle_replace_re_all(expr *e) {
+        STRACE("str", tout << "handle-replace-re-all: " << mk_pp(e, m) << '\n';);
+        if (axiomatized_persist_terms.contains(e))
+            return;
+
+        axiomatized_persist_terms.insert(e);
+
+        ast_manager &m = get_manager();
+        expr *s = nullptr, *i = nullptr, *l = nullptr;
+        VERIFY(m_util_s.str.is_replace_re_all(e, s, i, l));
+
+        expr_ref v = mk_str_var_fresh("replace_all");
+        // create equation for propagating length constraints
+        // tmp = replace_all(...) => |tmp| = |replace_all(...)|
+        add_axiom({mk_eq(v, e, false)});
+        this->predicate_replace.insert(e, v.get());  
+    }
+
     expr_ref theory_str_noodler::mk_concat(expr* e1, expr* e2) {
         return expr_ref(m_util_s.str.mk_concat(e1, e2), m);
     }
diff --git a/src/smt/theory_str_noodler/theory_str_noodler.h b/src/smt/theory_str_noodler/theory_str_noodler.h
index b8e9a6afbd..9b281ca152 100644
--- a/src/smt/theory_str_noodler/theory_str_noodler.h
+++ b/src/smt/theory_str_noodler/theory_str_noodler.h
@@ -334,6 +334,8 @@ namespace smt::noodler {
         void handle_conversion(expr *e);
         void handle_lex_leq(expr *e);
         void handle_lex_lt(expr *e);
+        void handle_replace_all(expr *e);
+        void handle_replace_re_all(expr *e);
 
         // methods for assigning boolean values to predicates
         void assign_not_contains(expr *e);
@@ -397,10 +399,27 @@ namespace smt::noodler {
         @return Instance of predicate
         */
         Predicate conv_eq_pred(app* expr);
+
+        /**
+         * @brief Check if the given equation is a temporary equations that was added 
+         * among axioms during axiomatization in handle_replace_all. These equalities
+         * are there due to length axioms inferring and proper handling of variable 
+         * substitution. We want to discard them as they make the instances artificially harder: 
+         * x = replace_all(...) || x = y --> we might get in final_check x = y && tmp = replace_all(...)
+         * in final_check we include only those transducer constraints that are present in remaining 
+         * constraints (ignoring tmp = replace_all(...)).
+         * 
+         * @param ex Equation
+         * @return true <-> is temporary transducer constraint
+         */
+        bool is_tmp_transducer_eq(app* const ex);
+
         /**
          * @brief Creates noodler formula containing relevant word equations and disequations
+         * 
+         * @param alph Set of symbols of the current instance (for transducer constraints)
          */
-        Formula get_word_formula_from_relevant();
+        Formula get_formula_from_relevant(const std::set<mata::Symbol>& alph);
         /**
          * @brief Get all symbols used in relevant word (dis)equations and memberships
          */
diff --git a/src/smt/theory_str_noodler/theory_str_noodler_final_check.cpp b/src/smt/theory_str_noodler/theory_str_noodler_final_check.cpp
index 149aadee57..b675254471 100644
--- a/src/smt/theory_str_noodler/theory_str_noodler_final_check.cpp
+++ b/src/smt/theory_str_noodler/theory_str_noodler_final_check.cpp
@@ -152,16 +152,22 @@ namespace smt::noodler {
             }
         }
 
+        // Gather symbols from relevant (dis)equations and from regular expressions of relevant memberships
+        std::set<mata::Symbol> symbols_in_formula = get_symbols_from_relevant();
+
         // Gather relevant word (dis)equations to noodler formula
-        Formula instance = get_word_formula_from_relevant();
+        Formula instance = get_formula_from_relevant(symbols_in_formula);
         STRACE("str",
+            tout << std::endl;
             for(const auto& f : instance.get_predicates()) {
                 tout << f.to_string() << std::endl;
             }
         );
+        // decison procedure for transducer constraints is not implemented yet
+        if(instance.contains_pred_type(PredicateType::Transducer)) {
+            util::throw_error("transducer constraints are not supported");
+        }
 
-        // Gather symbols from relevant (dis)equations and from regular expressions of relevant memberships
-        std::set<mata::Symbol> symbols_in_formula = get_symbols_from_relevant();
         // For the case that it is possible we have to_int/from_int, we keep digits (0-9) as explicit symbols, so that they are not represented by dummy_symbol and it is easier to handle to_int/from_int
         if (!m_conversion_todo.empty()) {
             for (mata::Symbol s = 48; s <= 57; ++s) {
@@ -476,16 +482,45 @@ namespace smt::noodler {
         return Predicate(ptype, std::vector<std::vector<BasicTerm>>{left, right});
     }
 
-    Formula theory_str_noodler::get_word_formula_from_relevant() {
+    bool theory_str_noodler::is_tmp_transducer_eq(app* const ex) {
+        if (this->m_util_s.str.is_replace_all(ex->get_arg(0)) || this->m_util_s.str.is_replace_re_all(ex->get_arg(0))) {
+            expr* rpl = this->predicate_replace.find(ex->get_arg(0));
+            return rpl->hash() == ex->get_arg(1)->hash();
+        }
+        if (this->m_util_s.str.is_replace_all(ex->get_arg(1)) || this->m_util_s.str.is_replace_re_all(ex->get_arg(1))) {
+            expr* rpl = this->predicate_replace.find(ex->get_arg(1));
+            return rpl->hash() == ex->get_arg(0)->hash();
+        }
+        return false;
+    }
+
+    Formula theory_str_noodler::get_formula_from_relevant(const std::set<mata::Symbol>& alph) {
         Formula instance;
+        std::vector<Predicate> transducer_pred {};
+        // create mata alphabet for transducer constraints
+        mata::EnumAlphabet mata_alph{};
+        for(const mata::Symbol& symb : alph) {
+            mata_alph.add_new_symbol(symb);
+        }
 
         for (const auto &we: this->m_word_eq_todo_rel) {
+            // ignore trivial equations obtained from axiomatization of 
+            // transducer constraints, e.g., tmp = replace_all(...)
+            if(is_tmp_transducer_eq(ctx.mk_eq_atom(we.first, we.second))) {
+                continue;
+            }
             Predicate inst = this->conv_eq_pred(ctx.mk_eq_atom(we.first, we.second));
+            // gather transducer constraints occurring in the concatenation
+            regex::gather_transducer_constraints(to_app(we.first), m, this->m_util_s, this->predicate_replace, this->var_name, &mata_alph, transducer_pred);
+            regex::gather_transducer_constraints(to_app(we.second), m, this->m_util_s, this->predicate_replace, this->var_name, &mata_alph, transducer_pred);
             instance.add_predicate(inst);
         }
 
         for (const auto& wd : this->m_word_diseq_todo_rel) {
             Predicate inst = this->conv_eq_pred(m.mk_not(ctx.mk_eq_atom(wd.first, wd.second)));
+            // gather transducer constraints occurring in the concatenation
+            regex::gather_transducer_constraints(to_app(wd.first), m, this->m_util_s, this->predicate_replace, this->var_name, &mata_alph, transducer_pred);
+            regex::gather_transducer_constraints(to_app(wd.second), m, this->m_util_s, this->predicate_replace, this->var_name, &mata_alph, transducer_pred);
             instance.add_predicate(inst);
         }
 
@@ -494,10 +529,18 @@ namespace smt::noodler {
             std::vector<BasicTerm> left, right;
             util::collect_terms(to_app(not_contains.first), m, this->m_util_s, this->predicate_replace, this->var_name, left);
             util::collect_terms(to_app(not_contains.second), m, this->m_util_s, this->predicate_replace, this->var_name, right);
+            // gather transducer constraints occurring in the concatenation
+            regex::gather_transducer_constraints(to_app(not_contains.first), m, this->m_util_s, this->predicate_replace, this->var_name, &mata_alph, transducer_pred);
+            regex::gather_transducer_constraints(to_app(not_contains.second), m, this->m_util_s, this->predicate_replace, this->var_name, &mata_alph, transducer_pred);
             Predicate inst(PredicateType::NotContains, std::vector<Concat>{left, right});
             instance.add_predicate(inst);
         }
 
+        // add all transducer predicates
+        for(const auto& p : transducer_pred) {
+            instance.add_predicate(p);
+        }
+
         return instance;
     }
 
@@ -506,6 +549,11 @@ namespace smt::noodler {
         std::set<mata::Symbol> symbols_in_formula{util::get_dummy_symbol()};
 
         for (const auto &word_equation: m_word_eq_todo_rel) {
+            // ignore trivial equations obtained from axiomatization of 
+            // transducer constraints, e.g., tmp = replace_all(...)
+            if(is_tmp_transducer_eq(ctx.mk_eq_atom(word_equation.first, word_equation.second))) {
+                continue;
+            }
             regex::extract_symbols(word_equation.first, m_util_s, symbols_in_formula);
             regex::extract_symbols(word_equation.second, m_util_s, symbols_in_formula);
         }
diff --git a/src/smt/theory_str_noodler/util.cc b/src/smt/theory_str_noodler/util.cc
index fe3a6d9024..35819ae5ae 100644
--- a/src/smt/theory_str_noodler/util.cc
+++ b/src/smt/theory_str_noodler/util.cc
@@ -268,6 +268,14 @@ namespace smt::noodler::util {
 
         return true;
     }
+
+    mata::Word get_mata_word_zstring(const zstring& word) {
+        mata::Word ret{};
+        for(size_t i = 0; i < word.length(); i++) {
+            ret.push_back(word[i]);
+        }
+        return ret;
+    }
 }
 
 template <typename T>
diff --git a/src/smt/theory_str_noodler/util.h b/src/smt/theory_str_noodler/util.h
index 8b495a5d57..6310c27122 100644
--- a/src/smt/theory_str_noodler/util.h
+++ b/src/smt/theory_str_noodler/util.h
@@ -11,6 +11,8 @@
 #include <unordered_map>
 #include <unordered_set>
 #include <vector>
+#include <mata/nft/nft.hh>
+#include <mata/nft/strings.hh>
 
 #include "smt/params/smt_params.h"
 #include "ast/arith_decl_plugin.h"
@@ -146,6 +148,14 @@ namespace smt::noodler::util {
      * @return boolean indicating whether we can split the @p word to @p automata (true if we can)
      */
     bool split_word_to_automata(const zstring& word, const std::vector<std::shared_ptr<mata::nfa::Nfa>>& automata, std::vector<zstring>& words);
+
+    /**
+     * @brief Convert zstring to mata::Word
+     * 
+     * @param word zstring
+     * @return mata::Word 
+     */
+    mata::Word get_mata_word_zstring(const zstring& word);
 }
 
 size_t bin_search_leftmost(const std::vector<mata::nfa::State>& haystack, mata::nfa::State needle);
diff --git a/src/test/noodler/CMakeLists.txt b/src/test/noodler/CMakeLists.txt
index a422e9d444..3a2bd23cda 100644
--- a/src/test/noodler/CMakeLists.txt
+++ b/src/test/noodler/CMakeLists.txt
@@ -20,6 +20,7 @@ if (Catch2_FOUND)
             decision-procedure.cpp
             parikh.cc
             util.cc
+            formula.cpp
     )
 
     find_library(LIBMATA mata)
diff --git a/src/test/noodler/formula-preprocess.cpp b/src/test/noodler/formula-preprocess.cpp
index f72d63ace1..fd9991468f 100644
--- a/src/test/noodler/formula-preprocess.cpp
+++ b/src/test/noodler/formula-preprocess.cpp
@@ -5,6 +5,7 @@
 #include <smt/theory_str_noodler/formula_preprocess.h>
 #include <smt/theory_str_noodler/theory_str_noodler.h>
 #include <mata/parser/re2parser.hh>
+#include <mata/nft/nft.hh>
 
 using namespace smt::noodler;
 
@@ -273,33 +274,63 @@ TEST_CASE( "Propagate variables", "[noodler]" ) {
         {b, regex_to_nfa("b")},
     });
 
+    mata::nft::Nft nft{2};
+    nft.initial = {0};
+    nft.final = {1};
+    nft.insert_word_by_parts(0, { {'a'}, {'b'} } , 1);
+    auto nft_ptr = std::make_shared<mata::nft::Nft>(nft);
+
     Predicate eq1(PredicateType::Equation, std::vector<std::vector<BasicTerm>>({ std::vector<BasicTerm>({a, x3, x4}), std::vector<BasicTerm>({b, x1, x2}) })  );
     Predicate ieq1(PredicateType::Inequation, std::vector<std::vector<BasicTerm>>({ std::vector<BasicTerm>({x1, x1}), std::vector<BasicTerm>({x3, x2}) })  );
     Predicate eq2(PredicateType::Equation, std::vector<std::vector<BasicTerm>>({ std::vector<BasicTerm>({x1}), std::vector<BasicTerm>({x2}) })  );
     Predicate eq3(PredicateType::Equation, std::vector<std::vector<BasicTerm>>({ std::vector<BasicTerm>({x1}), std::vector<BasicTerm>({x3}) })  );
-    Formula conj;
-    conj.add_predicate(eq1);
-    conj.add_predicate(ieq1);
-    conj.add_predicate(eq2);
-    conj.add_predicate(eq3);
-    FormulaPreprocessor prep(conj, aut_ass, {}, {}, {});
+    Predicate tr1(PredicateType::Transducer, std::vector<std::vector<BasicTerm>>({ std::vector<BasicTerm>({x1}), std::vector<BasicTerm>({x3}) }), nft_ptr );
+    Predicate tr2(PredicateType::Transducer, std::vector<std::vector<BasicTerm>>({ std::vector<BasicTerm>({x1}), std::vector<BasicTerm>({x1}) }), nft_ptr );
 
-    prep.propagate_variables();
-    prep.clean_varmap();
-    INFO(prep.to_string());
+    SECTION("(In)equations") {
+        Formula conj;
+        conj.add_predicate(eq1);
+        conj.add_predicate(ieq1);
+        conj.add_predicate(eq2);
+        conj.add_predicate(eq3);
+        FormulaPreprocessor prep(conj, aut_ass, {}, {}, {});
 
-    Formula res_conj;
-    res_conj.add_predicate(Predicate(PredicateType::Equation, std::vector<std::vector<BasicTerm>>({ std::vector<BasicTerm>({a, x1, x4}), std::vector<BasicTerm>({b, x1, x1}) })));
-    res_conj.add_predicate(Predicate(PredicateType::Inequation, std::vector<std::vector<BasicTerm>>({ std::vector<BasicTerm>({x1, x1}), std::vector<BasicTerm>({x1, x1}) })));
-    FormulaPreprocessor prep_res(res_conj, aut_ass, {}, {}, {});
+        prep.propagate_variables();
+        prep.clean_varmap();
+        INFO(prep.to_string());
 
-    AutAssignment ret = prep.get_aut_assignment();
-    CHECK(mata::nfa::are_equivalent(*ret.at(x1), regex_to_nfa("")));
-    CHECK(mata::nfa::are_equivalent(*ret.at(x2), regex_to_nfa("(a|b)*")));
-    CHECK(mata::nfa::are_equivalent(*ret.at(x3), regex_to_nfa("(b|c)*")));
-    CHECK(prep.get_formula().get_varmap() == prep_res.get_formula().get_varmap());
-    CHECK(prep.get_formula().get_predicates_set() == prep_res.get_formula().get_predicates_set());
-    CHECK(prep.get_dependency() == Dependency({{0, {2,3}}, {1, {2,3}}, {3, {2}}}));
+        Formula res_conj;
+        res_conj.add_predicate(Predicate(PredicateType::Equation, std::vector<std::vector<BasicTerm>>({ std::vector<BasicTerm>({a, x1, x4}), std::vector<BasicTerm>({b, x1, x1}) })));
+        res_conj.add_predicate(Predicate(PredicateType::Inequation, std::vector<std::vector<BasicTerm>>({ std::vector<BasicTerm>({x1, x1}), std::vector<BasicTerm>({x1, x1}) })));
+        FormulaPreprocessor prep_res(res_conj, aut_ass, {}, {}, {});
+
+        AutAssignment ret = prep.get_aut_assignment();
+        CHECK(mata::nfa::are_equivalent(*ret.at(x1), regex_to_nfa("")));
+        CHECK(mata::nfa::are_equivalent(*ret.at(x2), regex_to_nfa("(a|b)*")));
+        CHECK(mata::nfa::are_equivalent(*ret.at(x3), regex_to_nfa("(b|c)*")));
+        CHECK(prep.get_formula().get_varmap() == prep_res.get_formula().get_varmap());
+        CHECK(prep.get_formula().get_predicates_set() == prep_res.get_formula().get_predicates_set());
+        CHECK(prep.get_dependency() == Dependency({{0, {2,3}}, {1, {2,3}}, {3, {2}}}));
+    }
+
+    SECTION("Transducers") {
+        Formula conj;
+        conj.add_predicate(tr1);
+        conj.add_predicate(eq3);
+        FormulaPreprocessor prep(conj, aut_ass, {}, {}, {});
+
+        prep.propagate_variables();
+        prep.clean_varmap();
+        INFO(prep.to_string());
+
+        Formula res_conj;
+        res_conj.add_predicate(tr2);
+        FormulaPreprocessor prep_res(res_conj, aut_ass, {}, {}, {});
+
+        CHECK(prep.get_formula().get_varmap() == prep_res.get_formula().get_varmap());
+        CHECK(prep.get_modified_formula() == res_conj);
+    }
+    
 }
 
 TEST_CASE( "Remove duplicates", "[noodler]" ) {
@@ -323,24 +354,34 @@ TEST_CASE( "Remove duplicates", "[noodler]" ) {
         {a, regex_to_nfa("a")},
         {b, regex_to_nfa("b")},
     });
+    mata::nft::Nft nft{2};
+    nft.initial = {0};
+    nft.final = {1};
+    nft.insert_word_by_parts(0, { {'a'}, {'b'} } , 1);
+    auto nft_ptr = std::make_shared<mata::nft::Nft>(nft);
 
     Predicate eq1(PredicateType::Equation, std::vector<std::vector<BasicTerm>>({ std::vector<BasicTerm>({a, x3, x4}), std::vector<BasicTerm>({b, x1, x2}) })  );
     Predicate eq2(PredicateType::Equation, std::vector<std::vector<BasicTerm>>({ std::vector<BasicTerm>({a, x3, x4}), std::vector<BasicTerm>({b, x1, x2}) })  );
     Predicate eq3(PredicateType::Equation, std::vector<std::vector<BasicTerm>>({ std::vector<BasicTerm>({x1}), std::vector<BasicTerm>({x3}) })  );
     Predicate ieq1(PredicateType::Inequation, std::vector<std::vector<BasicTerm>>({ std::vector<BasicTerm>({x1}), std::vector<BasicTerm>({x3}) })  );
     Predicate ieq2(PredicateType::Inequation, std::vector<std::vector<BasicTerm>>({ std::vector<BasicTerm>({x1}), std::vector<BasicTerm>({x3}) })  );
+    Predicate tr1(PredicateType::Transducer, std::vector<std::vector<BasicTerm>>({ std::vector<BasicTerm>({x1}), std::vector<BasicTerm>({x3}) }), nft_ptr );
+    Predicate tr2(PredicateType::Transducer, std::vector<std::vector<BasicTerm>>({ std::vector<BasicTerm>({x1}), std::vector<BasicTerm>({x3}) }), nft_ptr  );
     Formula conj;
     conj.add_predicate(eq1);
     conj.add_predicate(eq3);
     conj.add_predicate(ieq1);
+    conj.add_predicate(tr1);
     conj.add_predicate(eq2);
     conj.add_predicate(ieq2);
+    conj.add_predicate(tr2);
     FormulaPreprocessor prep(conj, aut_ass, {}, {}, {});
 
     Formula res_conj;
     res_conj.add_predicate(eq1);
     res_conj.add_predicate(eq3);
     res_conj.add_predicate(ieq1);
+    res_conj.add_predicate(tr1);
     FormulaPreprocessor prep_res(res_conj, aut_ass, {}, {}, {});
 
     INFO(prep.to_string());
@@ -374,6 +415,8 @@ TEST_CASE( "Sublists", "[noodler]" ) {
 
     Predicate eq1(PredicateType::Equation, std::vector<std::vector<BasicTerm>>({ std::vector<BasicTerm>({a, x3, x4, b}), std::vector<BasicTerm>({x1, x1, x2}) })  );
     Predicate eq2(PredicateType::Equation, std::vector<std::vector<BasicTerm>>({ std::vector<BasicTerm>({b, x3, x4, b}), std::vector<BasicTerm>({x2, x1, x2}) })  );
+    // transducer itself is not important for this case
+    Predicate tr2(PredicateType::Equation, std::vector<std::vector<BasicTerm>>({ std::vector<BasicTerm>({b, x3, x4, b}), std::vector<BasicTerm>({x2, x1, x2}) })  );
     Predicate eq3(PredicateType::Equation, std::vector<std::vector<BasicTerm>>({ std::vector<BasicTerm>({x5, x1, x2, x3}), std::vector<BasicTerm>({x4, x1, x2}) })  );
     Predicate eq4(PredicateType::Inequation, std::vector<std::vector<BasicTerm>>({ std::vector<BasicTerm>({x5, x1, x2, x3}), std::vector<BasicTerm>({x4, a, b}) })  );
 
@@ -387,6 +430,16 @@ TEST_CASE( "Sublists", "[noodler]" ) {
         CHECK(res == std::map<Concat, unsigned>({ {std::vector<BasicTerm>({x3, x4, b}), 2}  }));
     }
 
+    SECTION("sub1 with transducers") {
+        Formula conj;
+        conj.add_predicate(eq1);
+        conj.add_predicate(tr2);
+        FormulaPreprocessor prep(conj, aut_ass, {}, {}, {});
+        std::map<Concat, unsigned> res;
+        prep.get_regular_sublists(res);
+        CHECK(res == std::map<Concat, unsigned>({ {std::vector<BasicTerm>({x3, x4, b}), 2}  }));
+    }
+
     SECTION("sub2") {
         Formula conj;
         std::map<Concat, unsigned> res;
@@ -430,11 +483,17 @@ TEST_CASE( "Reduce regular", "[noodler]" ) {
         {b, regex_to_nfa("b")},
     });
 
+    mata::nft::Nft nft{2, {0}, {1}};
+    nft.insert_word_by_parts(0, { {'a'}, {'b'} } , 1);
+    auto nft_ptr = std::make_shared<mata::nft::Nft>(nft);
+
     Predicate eq1(PredicateType::Inequation, std::vector<std::vector<BasicTerm>>({ std::vector<BasicTerm>({a, x3, x4, b}), std::vector<BasicTerm>({x1, x1, x2}) })  );
     Predicate eq2(PredicateType::Equation, std::vector<std::vector<BasicTerm>>({ std::vector<BasicTerm>({x2, x1, x2}), std::vector<BasicTerm>({b, x3, x4, b}) })  );
     Predicate eq3(PredicateType::Equation, std::vector<std::vector<BasicTerm>>({ std::vector<BasicTerm>({x5, x1, x2, x3}), std::vector<BasicTerm>({x4, x1, x2}) })  );
     Predicate eq4(PredicateType::Equation, std::vector<std::vector<BasicTerm>>({ std::vector<BasicTerm>({x5, x1, x2, x3}), std::vector<BasicTerm>({x4, a, b}) })  );
+    Predicate tr4(PredicateType::Transducer, std::vector<std::vector<BasicTerm>>({ std::vector<BasicTerm>({x5, x1, x2, x3}), std::vector<BasicTerm>({x4, a, b}) }), nft_ptr  );
 
+    
     SECTION("basic") {
         Formula conj;
         conj.add_predicate(eq1);
@@ -491,6 +550,24 @@ TEST_CASE( "Reduce regular", "[noodler]" ) {
         CHECK(prep.get_dependency().empty());
         CHECK(prep.get_flat_dependency().empty());
     }
+
+    SECTION("transducers") {
+        Formula conj;
+        conj.add_predicate(tr4);
+        FormulaPreprocessor prep(conj, aut_ass, {x2}, {}, {});
+        prep.reduce_regular_sequence(1);
+        AutAssignment ret = prep.get_aut_assignment();
+
+        tmp0 = BasicTerm{BasicTermType::Variable, "regular_seq!n5"};
+        tmp1 = BasicTerm{BasicTermType::Variable, "regular_seq!n6"};
+        CHECK(mata::nfa::are_equivalent(*ret.at(tmp0), regex_to_nfa("b*ab")));
+        CHECK(mata::nfa::are_equivalent(*ret.at(tmp1), regex_to_nfa("(a|b)*a*")));
+        CHECK(prep.get_formula().get_predicates_set() == std::set<Predicate>({
+            Predicate(PredicateType::Equation, std::vector<std::vector<BasicTerm>>({ std::vector<BasicTerm>({tmp0}), std::vector<BasicTerm>({x4, a, b}) })),
+            Predicate(PredicateType::Transducer, std::vector<std::vector<BasicTerm>>({ std::vector<BasicTerm>({tmp1}), std::vector<BasicTerm>({tmp0}) }), nft_ptr ),
+            Predicate(PredicateType::Equation, std::vector<std::vector<BasicTerm>>({ std::vector<BasicTerm>({tmp1 }), std::vector<BasicTerm>({x5, x1, x2, x3}) })  )
+        }));
+    }
 }
 
 TEST_CASE( "Propagate eps", "[noodler]" ) {
@@ -515,11 +592,16 @@ TEST_CASE( "Propagate eps", "[noodler]" ) {
         {eps, regex_to_nfa("")},
     });
 
+    mata::nft::Nft nft{2, {0}, {1}};
+    nft.insert_word_by_parts(0, { {'a'}, {'b'} } , 1);
+    auto nft_ptr = std::make_shared<mata::nft::Nft>(nft);
+
     Predicate eq1(PredicateType::Equation, std::vector<std::vector<BasicTerm>>({ std::vector<BasicTerm>({eps}), std::vector<BasicTerm>({x1, x2}) })  );
     Predicate eq2(PredicateType::Equation, std::vector<std::vector<BasicTerm>>({ std::vector<BasicTerm>({x2, x1, x2}), std::vector<BasicTerm>({x3, x4}) })  );
     Predicate eq3(PredicateType::Equation, std::vector<std::vector<BasicTerm>>({ std::vector<BasicTerm>({x3, b, x4}), std::vector<BasicTerm>({x5, x1}) })  );
     Predicate eq4(PredicateType::Equation, std::vector<std::vector<BasicTerm>>({ std::vector<BasicTerm>({b, x1}), std::vector<BasicTerm>({eps}) })  );
     Predicate ieq1(PredicateType::Inequation, std::vector<std::vector<BasicTerm>>({ std::vector<BasicTerm>({x1}), std::vector<BasicTerm>({eps}) })  );
+    Predicate tr4(PredicateType::Transducer, std::vector<std::vector<BasicTerm>>({ std::vector<BasicTerm>({x5, x1}), std::vector<BasicTerm>({x2}) }), nft_ptr  );
 
     SECTION("basic") {
         Formula conj;
@@ -553,6 +635,20 @@ TEST_CASE( "Propagate eps", "[noodler]" ) {
         }));
         CHECK(prep.get_dependency() == Dependency({{0, {0}}}));
     }
+
+    SECTION("transducer constraint") {
+        Formula conj;
+        conj.add_predicate(eq1);
+        conj.add_predicate(tr4);
+        FormulaPreprocessor prep(conj, aut_ass, {}, {}, {});
+        prep.propagate_eps();
+        AutAssignment ret = prep.get_aut_assignment();
+        CHECK(mata::nfa::are_equivalent(*ret.at(x1), regex_to_nfa("")));
+        CHECK(mata::nfa::are_equivalent(*ret.at(x2), regex_to_nfa("")));
+        CHECK(prep.get_formula().get_predicates_set() == std::set<Predicate>({
+            Predicate(PredicateType::Transducer, std::vector<std::vector<BasicTerm>>({ std::vector<BasicTerm>({x5}), std::vector<BasicTerm>() }), nft_ptr ),
+        }));
+    }
 }
 
 TEST_CASE( "Separate eqs", "[noodler]" ) {
diff --git a/src/test/noodler/formula.cpp b/src/test/noodler/formula.cpp
new file mode 100644
index 0000000000..9d236be21f
--- /dev/null
+++ b/src/test/noodler/formula.cpp
@@ -0,0 +1,90 @@
+#include <iostream>
+#include <unordered_set>
+
+#include <catch2/catch_test_macros.hpp>
+#include <mata/nfa/nfa.hh>
+#include <mata/nft/nft.hh>
+
+#include "smt/theory_str_noodler/formula.h"
+
+using namespace smt::noodler;
+
+
+TEST_CASE( "Transducer predicate", "[noodler]" ) {
+
+    // two-tape transducer by default
+    mata::nft::Nft nft{2};
+    nft.initial = {0};
+    nft.final = {1};
+    nft.insert_word_by_parts(0, { {'a'}, {'b'} } , 1);
+    CHECK(nft.delta.num_of_states() == 3);
+    CHECK(nft.is_tuple_in_lang({ {'a'}, {'b'} }));
+
+    BasicTerm x {BasicTermType::Variable, "x"};
+    BasicTerm y {BasicTermType::Variable, "x"};
+
+    SECTION("Switched predicate") {
+         // transducer implementing inversion relation
+        mata::nft::Nft nft_inv = mata::nft::invert_levels(nft);
+        CHECK(nft_inv.is_tuple_in_lang({ {'b'}, {'a'} }));
+        CHECK(!nft_inv.is_tuple_in_lang({ {'a'}, {'b'} }));
+
+        Predicate pred_trans { PredicateType::Transducer, { { x }, { y } }, std::make_shared<mata::nft::Nft>(nft) };
+        Predicate pred_trans_switch = pred_trans.get_switched_sides_predicate();
+
+        // result
+        Predicate switch_res { PredicateType::Transducer, { { y }, { x } }, std::make_shared<mata::nft::Nft>(nft_inv) };
+        CHECK(pred_trans_switch.strong_equals(switch_res));
+    }
+
+    SECTION("Comparison") {
+        mata::nft::Nft nft_other{2};
+        nft_other.initial = {0};
+        nft_other.final = {1};
+        nft_other.insert_word_by_parts(0, { {'c'}, {'d'} } , 1);
+
+        
+        Predicate p1 { PredicateType::Transducer, { { x }, { y } }, std::make_shared<mata::nft::Nft>(nft) };
+        Predicate p2 { PredicateType::Transducer, { { x }, { y } }, std::make_shared<mata::nft::Nft>(nft_other) };
+        Predicate p3 { PredicateType::Transducer, { { x }, { y } }, p1.get_transducer() };
+        CHECK(p1 != p2);
+        CHECK(!(p1 < p1));
+        CHECK(p1 == p1);
+        CHECK(p1.strong_equals(p1));
+        CHECK(p1.strong_equals(p3));
+        CHECK(!(p1 < p3));
+        CHECK(!(p3 < p1));
+
+        std::set<Predicate> st{};
+        st.insert(p1);
+        st.insert(p2);
+        st.insert(p3);
+        CHECK(st.size() == 2);
+
+        std::unordered_set<Predicate> st_un{};
+        st_un.insert(p1);
+        st_un.insert(p2);
+        st_un.insert(p3);
+        CHECK(st_un.size() == 2);
+    }
+
+    SECTION("Replace") {
+        mata::nft::Nft nft_other{2};
+        nft_other.initial = {0};
+        nft_other.final = {1};
+        nft_other.insert_word_by_parts(0, { {'c'}, {'d'} } , 1);
+        auto nft_ptr = std::make_shared<mata::nft::Nft>(nft);
+
+        
+        Predicate p1 { PredicateType::Transducer, { { x }, { y } }, nft_ptr };
+        Predicate pres { PredicateType::Transducer, { { x }, { x } }, nft_ptr };
+
+        Formula f{};
+        f.add_predicate(p1);
+        f.replace({x}, {y});
+
+        Formula fres {};
+        fres.add_predicate(pres);
+        CHECK(f == fres);
+    }
+}
diff --git a/src/test/noodler/inclusion-graph-node.cc b/src/test/noodler/inclusion-graph-node.cc
index 13e9573ca1..822a8234a7 100644
--- a/src/test/noodler/inclusion-graph-node.cc
+++ b/src/test/noodler/inclusion-graph-node.cc
@@ -2,6 +2,7 @@
 
 #include <catch2/catch_test_macros.hpp>
 #include <mata/nfa/nfa.hh>
+#include <mata/nft/nft.hh>
 
 #include "smt/theory_str_noodler/inclusion_graph.h"
 
@@ -360,3 +361,93 @@ TEST_CASE("print_to_dot()") {
     graph.print_to_dot(stream);
     CHECK(!stream.str().empty());
 }
+
+TEST_CASE("Inclusion graph with transducers", "[noodler]") {
+    Graph graph;
+    Formula formula;
+
+    BasicTerm u{ BasicTermType::Variable, "u" };
+    BasicTerm v{ BasicTermType::Variable, "v" };
+    BasicTerm x{ BasicTermType::Variable, "x" };
+    BasicTerm y{ BasicTermType::Variable, "y" };
+    BasicTerm z{ BasicTermType::Variable, "z" };
+
+    mata::nft::Nft nft1{2};
+    nft1.initial = {0};
+    nft1.final = {1};
+    nft1.insert_word_by_parts(0, { {'a'}, {'b'} } , 1);
+
+    mata::nft::Nft nft2{2};
+    nft2.initial = {0};
+    nft2.final = {1};
+    nft2.insert_word_by_parts(0, { {'c'}, {'d'} } , 1);
+
+
+    SECTION("T(x,y) && S(zz,yu)") {
+        Predicate p1{ PredicateType::Transducer, { { x }, { y } }, std::make_shared<mata::nft::Nft>(nft1) };
+        Predicate p2{ PredicateType::Transducer, { { z, z }, { y, u } }, std::make_shared<mata::nft::Nft>(nft2) };
+
+        Formula formula;
+        formula.add_predicate(p1);
+        formula.add_predicate(p2);
+        graph = Graph::create_inclusion_graph(formula);
+
+        CHECK(graph.get_nodes().size() == 2);
+        CHECK(graph.get_num_of_edges() == 1);
+        CHECK(!graph.is_cyclic());
+    }
+
+    SECTION("x=y && T(zz,yu)") {
+        Predicate p1{ PredicateType::Equation, { { x }, { y } } };
+        Predicate p2{ PredicateType::Transducer, { { z, z }, { y, u } }, std::make_shared<mata::nft::Nft>(nft2) };
+
+        Formula formula;
+        formula.add_predicate(p1);
+        formula.add_predicate(p2);
+        graph = Graph::create_inclusion_graph(formula);
+
+        CHECK(graph.get_nodes().size() == 2);
+        CHECK(graph.get_num_of_edges() == 1);
+        CHECK(!graph.is_cyclic());
+    }
+
+    SECTION("T(x,x)") {
+        Predicate p1{ PredicateType::Transducer, { { x }, { x } }, std::make_shared<mata::nft::Nft>(nft2) };
+
+        Formula formula;
+        formula.add_predicate(p1);
+        graph = Graph::create_inclusion_graph(formula);
+
+        CHECK(graph.get_nodes().size() == 2);
+        CHECK(graph.get_num_of_edges() == 2);
+        CHECK(graph.is_cyclic());
+    }
+
+    SECTION("T(x,y) && x=y") {
+        Predicate p1{ PredicateType::Transducer, { { x }, { y } }, std::make_shared<mata::nft::Nft>(nft2) };
+        Predicate p2{ PredicateType::Equation, { { x }, { y } } };
+
+        Formula formula;
+        formula.add_predicate(p1);
+        formula.add_predicate(p2);
+        graph = Graph::create_inclusion_graph(formula);
+
+        CHECK(graph.get_nodes().size() == 4);
+        CHECK(graph.get_num_of_edges() == 8);
+        CHECK(graph.is_cyclic());
+    }
+
+    SECTION("T(x,y) && x=z") {
+        Predicate p1{ PredicateType::Transducer, { { x }, { y } }, std::make_shared<mata::nft::Nft>(nft2) };
+        Predicate p2{ PredicateType::Equation, { { x }, { z } } };
+
+        Formula formula;
+        formula.add_predicate(p1);
+        formula.add_predicate(p2);
+        graph = Graph::create_inclusion_graph(formula);
+
+        CHECK(graph.get_nodes().size() == 2);
+        CHECK(graph.get_num_of_edges() == 1);
+        CHECK(!graph.is_cyclic());
+    }
+}