diff --git a/src/cprover/chc_db.cpp b/src/cprover/chc_db.cpp
new file mode 100644
index 00000000000..e2b71200827
--- /dev/null
+++ b/src/cprover/chc_db.cpp
@@ -0,0 +1,80 @@
+//
+// Created by Yakir Vizel on 5/27/24.
+//
+
+#include "chc_db.h"
+
+#include <iostream>
+
+chc_dbt::chc_sett chc_dbt::m_empty_set;
+std::unordered_set<exprt, irep_hash> chc_grapht::m_expr_empty_set;
+
+void chc_dbt::reset_indices()
+{
+  m_body_idx.clear();
+  m_head_idx.clear();
+}
+
+void chc_dbt::build_indices()
+{
+  reset_indices();
+
+  for (std::size_t i = 0; i < m_clauses.size(); i++)
+  {
+    auto & r = m_clauses[i];
+    if (!can_cast_expr<function_application_exprt>(*r.head()))
+    {
+      continue;
+    }
+    exprt func = to_function_application_expr(*r.head()).function();
+    m_head_idx[func].insert(i);
+
+    std::vector<symbol_exprt> use;
+    r.used_relations(*this,std::back_inserter(use));
+    for (auto & symb : use)
+    {
+      m_body_idx[symb].insert(i);
+    }
+  }
+}
+
+void chc_grapht::build_graph()
+{
+  m_db.build_indices();
+
+  for (auto & sp : m_db.get_state_preds())
+  {
+    std::unordered_set<exprt, irep_hash> outgoing;
+    const chc_dbt::chc_sett &uses = m_db.use(sp);
+    for (auto idx: uses) {
+      const horn_clauset & r = m_db.get_clause(idx);
+      const exprt * head = r.head();
+      if (can_cast_expr<function_application_exprt>(*head))
+      {
+        outgoing.insert(to_function_application_expr(*head).function());
+      }
+    }
+    m_outgoing.insert(std::make_pair(sp, outgoing));
+
+    std::unordered_set<exprt, irep_hash> incoming;
+    const chc_dbt::chc_sett &defs = m_db.def(sp);
+    chc_dbt::is_state_pred isStatePred(m_db);
+    for (auto idx : defs) {
+      const horn_clauset & r = m_db.get_clause(idx);
+      std::set<symbol_exprt> symbols = find_symbols(*r.body());
+      for (auto & s : symbols)
+        if (isStatePred(s))
+          incoming.insert(s);
+    }
+    m_incoming.insert(std::make_pair(sp, incoming));
+  }
+
+  for (auto & sp : m_db.get_state_preds()) {
+    std::string name = as_string(sp.get_identifier());
+
+    if (name.find("SInitial") != std::string::npos && incoming(sp).size() == 0) {
+      m_entry = &sp;
+      break;
+    }
+  }
+}
diff --git a/src/cprover/chc_db.h b/src/cprover/chc_db.h
new file mode 100644
index 00000000000..3e888d2b2d4
--- /dev/null
+++ b/src/cprover/chc_db.h
@@ -0,0 +1,266 @@
+//
+// Created by Yakir Vizel on 5/27/24.
+//
+
+#ifndef CBMC_CHC_DB_H
+#define CBMC_CHC_DB_H
+
+#include <util/mathematical_expr.h>
+#include <util/std_expr.h>
+#include <util/find_symbols.h>
+#include <language_util.h>
+
+#include <vector>
+#include <map>
+#include <set>
+#include <functional>
+
+class chc_dbt;
+
+/*
+ * A horn clause.
+ * This class is simply a wrapper around a forall_exprt with a few utilities:
+ * 1. Getting the body of a clause
+ * 2. Getting the head of a clause
+ * 3. Checking if a clause is a fact or a query
+ * 4. Getting used relations (the predicates) or function applications
+ *    (their instantiations) in a clause.
+ */
+class horn_clauset
+{
+  forall_exprt m_chc;
+
+public:
+  horn_clauset(forall_exprt f) : m_chc(f) {}
+
+  horn_clauset(std::vector<symbol_exprt> & vars, exprt clause) : m_chc(vars, clause) {
+
+  }
+
+  const forall_exprt & get_chc() const
+  {
+    return m_chc;
+  }
+
+  const exprt* body() const {
+    if (can_cast_expr<implies_exprt>(m_chc.where()))
+    {
+      return &to_implies_expr(m_chc.where()).op0();
+    }
+    return &m_chc.where();
+  }
+
+  const exprt* head() const {
+    if (can_cast_expr<implies_exprt>(m_chc.where()))
+    {
+      return &to_implies_expr(m_chc.where()).op1();
+    }
+    return nullptr;
+  }
+
+  bool is_fact() const {
+    auto b = body();
+    bool not_fact = false;
+    b->visit_pre(
+      [&not_fact](const exprt &expr)  {
+        if(can_cast_expr<function_application_exprt>(expr))
+        {
+          not_fact = true;
+        }
+      });
+    return !not_fact;
+  }
+
+  bool is_query() const {
+    if (can_cast_expr<implies_exprt>(m_chc.where()))
+    {
+      auto h = head();
+      bool res = true;
+      h->visit_pre(
+        [&res](const exprt &expr) {
+          if(can_cast_expr<function_application_exprt>(expr))
+            res = false;
+      });
+      return res;
+    }
+    return false;
+  }
+
+  bool operator==(const horn_clauset &other) const
+  {
+    return m_chc == other.m_chc;
+  }
+
+  bool operator!=(const horn_clauset &other) const
+  {
+    return !(*this==other);
+  }
+
+  bool operator<(const horn_clauset &other) const
+  {
+    return m_chc < other.m_chc;
+  }
+
+  template <typename OutputIterator>
+  void used_relations(chc_dbt &db, OutputIterator out) const;
+  template <typename OutputIterator>
+  void used_func_app(chc_dbt &db, OutputIterator out) const;
+};
+
+/*
+ * A database of CHCs.
+ * Uninterpreted relations need to be registered.
+ */
+class chc_dbt
+{
+  friend class horn_clauset;
+public:
+  struct is_state_pred : public std::__unary_function<exprt, bool> {
+    const chc_dbt &m_db;
+    is_state_pred(const chc_dbt &db) : m_db(db) {}
+
+    bool operator()(symbol_exprt state) { return m_db.has_state_pred(state); }
+  };
+
+  typedef std::unordered_set<std::size_t> chc_sett;
+
+private:
+  using chcst = std::vector<horn_clauset>;
+  chcst m_clauses;
+
+  std::unordered_set<symbol_exprt, irep_hash> m_state_preds;
+
+  typedef std::map<exprt, chc_sett> chc_indext;
+  chc_indext m_body_idx;
+  chc_indext m_head_idx;
+
+  // representing the empty set
+  static chc_sett m_empty_set;
+
+public:
+  chc_dbt() {}
+
+  void add_state_pred(const symbol_exprt & state) { m_state_preds.insert(state); }
+  const std::unordered_set<symbol_exprt, irep_hash> &get_state_preds() { return m_state_preds; }
+  bool has_state_pred(const symbol_exprt & state) const { return m_state_preds.count(state) > 0; }
+
+  void build_indices();
+  void reset_indices();
+
+  const chc_sett & use(const exprt & state) const {
+    auto it = m_body_idx.find(state);
+    if (it == m_body_idx.end())
+      return m_empty_set;
+    return it->second;
+  }
+
+  const chc_sett & def(const exprt & state) const {
+    auto it = m_head_idx.find(state);
+    if (it == m_head_idx.end())
+      return m_empty_set;
+    return it->second;
+  }
+
+  void add_clause(const forall_exprt & f)
+  {
+    if (f.is_true())
+      return;
+    for (auto & c : m_clauses) {
+      if (c.get_chc()==f) return;
+    }
+    m_clauses.push_back(horn_clauset(f));
+    reset_indices();
+  }
+
+  [[nodiscard]] const horn_clauset & get_clause(std::size_t idx) const
+  {
+    INVARIANT(idx < m_clauses.size(), "Index in range");
+    return m_clauses[idx];
+  }
+
+  chcst::iterator begin() { return m_clauses.begin(); }
+  chcst::iterator end() { return m_clauses.end(); }
+  chcst::const_iterator begin() const { return m_clauses.begin(); }
+  chcst::const_iterator end() const { return m_clauses.end(); }
+};
+
+template <typename OutputIterator>
+void horn_clauset::used_relations(chc_dbt &db, OutputIterator out) const
+{
+  const exprt *body = this->body();
+  if (body == nullptr) return;
+  std::set<symbol_exprt> symbols = find_symbols(*body);
+
+  chc_dbt::is_state_pred filter(db);
+  for (auto & symb : symbols) {
+    if (filter(symb)) {
+      *out = symb;
+    }
+  }
+}
+
+template <typename OutputIterator>
+void horn_clauset::used_func_app(chc_dbt &db, OutputIterator out) const
+{
+  const exprt *body = this->body();
+  if (body == nullptr) return;
+
+  std::unordered_set<function_application_exprt, irep_hash> funcs;
+  body->visit_pre([&funcs](const exprt &expr) {
+                     if (can_cast_expr<function_application_exprt>(expr))
+                     {
+                       const function_application_exprt & f = to_function_application_expr(expr);
+                       funcs.insert(f);
+                     }
+                   });
+
+  chc_dbt::is_state_pred filter(db);
+  for (auto & f : funcs) {
+    if (filter(to_symbol_expr(f.function()))) {
+      *out = f;
+    }
+  }
+}
+
+/*
+ * The CHC dependency graph.
+ * Uninterpreted relations are vertices, dependency is based on clauses:
+ * relations in the body have an edge to the relation in the head.
+ */
+class chc_grapht
+{
+  chc_dbt & m_db;
+  typedef std::map<exprt, std::unordered_set<exprt, irep_hash>> grapht;
+  grapht m_incoming;
+  grapht m_outgoing;
+  const symbol_exprt *m_entry;
+
+  // representing the empty set
+  static std::unordered_set<exprt, irep_hash> m_expr_empty_set;
+
+public:
+  chc_grapht(chc_dbt & db) : m_db(db), m_entry(nullptr) {}
+
+  void build_graph();
+
+  bool has_entry() const { return m_entry != nullptr; }
+  const symbol_exprt *entry() const {
+    INVARIANT(has_entry(), "Entry must exist.");
+    return m_entry; }
+
+  const std::unordered_set<exprt, irep_hash> &outgoing(const symbol_exprt &state) const {
+    auto it = m_outgoing.find(state);
+    if (it == m_outgoing.end())
+      return m_expr_empty_set;
+    return it->second;
+  }
+
+  const std::unordered_set<exprt, irep_hash> &incoming(const symbol_exprt &state) const {
+    auto it = m_incoming.find(state);
+    if (it == m_incoming.end())
+      return m_expr_empty_set;
+    return it->second;
+  }
+};
+
+#endif //CBMC_CHC_DB_H
diff --git a/src/cprover/chc_large_step.h b/src/cprover/chc_large_step.h
new file mode 100644
index 00000000000..143c0fc33ea
--- /dev/null
+++ b/src/cprover/chc_large_step.h
@@ -0,0 +1,212 @@
+//
+// Created by Yakir Vizel on 7/23/24.
+//
+
+#ifndef CBMC_CHC_LARGE_STEP_H
+#define CBMC_CHC_LARGE_STEP_H
+
+#include "chc_wto.h"
+#include <util/substitute_symbols.h>
+#include <util/format_expr.h>
+
+/*
+ * Traverses the clauses in order and resolving all predicates (symbols)
+ * that are not a head (e.g. a head of a loop).
+ * This is similar to variable elimination in SAT.
+ */
+class resolution_visitort : public wto_element_visitort
+{
+private:
+  chc_dbt & m_db;
+  chc_dbt m_new_db;
+  std::unordered_map<std::size_t, std::vector<horn_clauset>> m_def;
+  std::unordered_set<std::size_t> m_heads;
+  bool m_verbose;
+
+public:
+  resolution_visitort(chc_dbt & db) : m_db(db), m_verbose(false) {}
+
+  chc_dbt &giveme_new_db() { return m_new_db; }
+
+  virtual void visit(const wto_singletont & s)
+  {
+    const symbol_exprt* symb = s.get();
+    eliminate(symb);
+  }
+
+  virtual void visit(const wto_componentt & comp)
+  {
+    const symbol_exprt* head = comp.head();
+    m_heads.insert(head->hash());
+    std::string str = head->get_identifier().c_str();
+    std::cout << "Head: " << str << "\n";
+    for (auto it = comp.begin(); it != comp.end(); it++)
+    {
+      it->get()->accept(this);
+    }
+    eliminate(head);
+  }
+
+  void populate_new_db()
+  {
+    std::vector<symbol_exprt> rels;
+    for (auto &clause : m_db)
+    {
+      if(clause.is_query())
+      {
+        clause.used_relations(m_db, std::back_inserter(rels));
+      }
+    }
+
+    std::set<std::size_t > preds_hash(m_heads.begin(), m_heads.end());
+    for (auto p : rels) {
+      preds_hash.insert(p.hash());
+    }
+
+    for (auto it : preds_hash)
+    {
+      auto c = m_def.find(it);
+      INVARIANT(c != m_def.end(), "No clauses");
+      for (auto clause : c->second)
+        m_new_db.add_clause(clause.get_chc());
+    }
+
+    for (auto &clause : m_db)
+    {
+      if(clause.is_query())
+      {
+        m_new_db.add_clause(clause.get_chc());
+      }
+    }
+  }
+
+private:
+  void eliminate(const symbol_exprt *symb)
+  {
+    for (auto idx : m_db.def(*symb))
+    {
+      auto & clause = m_db.get_clause(idx);
+      std::vector<symbol_exprt> use;
+
+      clause.used_relations(m_db,std::back_inserter(use));
+      if (use.size() > 1) {
+        throw incorrect_goto_program_exceptiont("Non-linear CHCs not supported yet");
+      }
+
+      if (clause.is_fact())
+      {
+        m_heads.insert(symb->hash());
+        std::vector<horn_clauset> def_chcs;
+        def_chcs.push_back(clause.get_chc());
+        m_def.insert(std::make_pair(symb->hash(), def_chcs));
+      }
+
+      for (auto & p : use)
+      {
+        auto it = m_def.find(p.hash());
+        std::vector<horn_clauset> def_chcs;
+        if (it == m_def.end() || m_heads.find(p.hash()) != m_heads.end())
+        {
+          def_chcs.push_back(clause);
+        }
+        else
+        {
+          for (auto cls_it = it->second.begin(); cls_it != it->second.end(); cls_it++)
+          {
+            forall_exprt resolvent = resolve_clauses((*cls_it), clause);
+            if (m_verbose)
+              std::cout << "Result:\n" << format(resolvent) << "\n";
+            def_chcs.push_back(resolvent);
+          }
+        }
+        auto def_it = m_def.find(symb->hash());
+        if (def_it == m_def.end())
+          m_def.insert(std::make_pair(symb->hash(), def_chcs));
+        else
+        {
+          auto & vec = def_it->second;
+          vec.insert(vec.end(), def_chcs.begin(), def_chcs.end());
+        }
+      }
+    }
+  }
+
+  forall_exprt resolve_clauses(const horn_clauset & c1, const horn_clauset & c2)
+  {
+    const exprt &body1 = *c1.body();
+    const exprt &head1 = *c1.head();
+    const exprt &body2 = *c2.body();
+    const exprt &head2 = *c2.head();
+
+    std::vector<function_application_exprt> use2;
+    c2.used_func_app(m_db,std::back_inserter(use2));
+
+    INVARIANT(use2.size() == 1, "Only handling linear case");
+    if (use2.size() != 1)
+      throw analysis_exceptiont("Resolution not possible");
+
+    function_application_exprt & body2_pred = use2[0];
+
+    const function_application_exprt *head1_pred = nullptr;
+    if (can_cast_expr<function_application_exprt>(*c1.head()))
+    {
+      head1_pred = &to_function_application_expr(head1);
+    }
+    if (head1_pred == nullptr)
+      throw analysis_exceptiont("Resolution not possible");
+
+    if (m_verbose)
+      std::cout << "Resolving: \n" << format(c1.get_chc()) << "\nAnd: \n"
+                << format(c2.get_chc()) << "\n";
+
+    std::set<symbol_exprt> all_vars(c1.get_chc().variables().begin(), c1.get_chc().variables().end());
+    all_vars.insert(c2.get_chc().variables().begin(), c2.get_chc().variables().end());
+
+    const function_application_exprt *body1_pred = nullptr;
+    exprt::operandst body_ops;
+    if (body1.id() == ID_and)
+    {
+      body1_pred = &to_function_application_expr(to_and_expr(body1).op0());
+      body_ops.push_back(to_and_expr(body1).op1());
+    }
+    else
+    {
+      body1_pred = &to_function_application_expr(body1);
+    }
+    exprt transformed_body = (can_cast_expr<and_exprt>(body2)) ? to_and_expr(body2).op1() : true_exprt();
+    exprt transformed_head = head2;
+
+    INVARIANT(head1_pred->arguments().size() == 1, "Only one argument to predicate is assumes");
+    const exprt &head_arg = head1_pred->arguments().at(0);
+    const symbol_exprt & body_arg = to_symbol_expr(body2_pred.arguments().at(0));
+
+    if ((head_arg.id() != ID_symbol) ||
+       (to_symbol_expr(head_arg).get_identifier() != body_arg.get_identifier()))
+    {
+      std::map<irep_idt, exprt> subs;
+      subs.insert(std::make_pair(body_arg.get_identifier(), head_arg));
+
+      if(!transformed_body.is_true())
+      {
+        std::optional<exprt> s = substitute_symbols(subs, transformed_body);
+        if(s.has_value())
+          transformed_body = std::move(s.value());
+      }
+
+      std::optional<exprt> s = substitute_symbols(subs, transformed_head);
+      if (s.has_value())
+      {
+        transformed_head = std::move(s.value());
+      }
+    }
+
+    body_ops.push_back(transformed_body);
+   transformed_body = and_exprt(*body1_pred, std::move(and_exprt(body_ops)));
+
+    forall_exprt f(std::vector<symbol_exprt>(all_vars.begin(), all_vars.end()),
+                   implies_exprt(std::move(transformed_body), std::move(transformed_head)));
+    return f;
+  }
+};
+
+#endif //CBMC_CHC_LARGE_STEP_H
diff --git a/src/cprover/chc_wto.h b/src/cprover/chc_wto.h
new file mode 100644
index 00000000000..3b9ed31e2c4
--- /dev/null
+++ b/src/cprover/chc_wto.h
@@ -0,0 +1,301 @@
+//
+// Created by Yakir Vizel on 5/28/24.
+//
+
+#ifndef CBMC_CHC_WTO_H
+#define CBMC_CHC_WTO_H
+
+#include "chc_db.h"
+#include <invariant.h>
+
+#include <optional>
+#include <unordered_map>
+#include <vector>
+#include <deque>
+#include <iostream>
+
+class wto_singletont;
+class wto_componentt;
+
+class wto_element_visitort
+{
+public:
+
+  virtual void visit(const wto_singletont &) = 0;
+  virtual void visit(const wto_componentt &) = 0;
+
+  virtual ~wto_element_visitort() {}
+};
+
+class wto_elementt
+{
+public:
+  virtual void accept(wto_element_visitort *) = 0;
+
+  virtual ~wto_elementt() {}
+};
+
+class wto_singletont : public wto_elementt
+{
+private:
+  const symbol_exprt* m_singleton;
+
+public:
+  wto_singletont(const symbol_exprt *e) : m_singleton(e) {}
+
+  const symbol_exprt* get() const { return m_singleton; }
+
+  void accept(wto_element_visitort *v) override { v->visit(*this); }
+};
+
+class wto_componentt : public wto_elementt
+{
+
+public:
+  typedef std::shared_ptr<wto_elementt> wto_element_ptr;
+  typedef std::deque<wto_element_ptr> wto_components_t;
+
+private:
+  const symbol_exprt *m_head;
+  wto_components_t m_components;
+
+public:
+  wto_componentt(const symbol_exprt *head, wto_components_t components)
+    : m_head(head), m_components(components) {}
+
+  typename wto_components_t::iterator begin() {
+    return m_components.begin();
+  }
+
+  typename wto_components_t::iterator end() { return m_components.end(); }
+
+  typename wto_components_t::const_iterator begin() const {
+    return m_components.begin();
+  }
+
+  typename wto_components_t::const_iterator end() const {
+    return m_components.end();
+  }
+
+  const symbol_exprt* head() const { return m_head; }
+
+  void accept(wto_element_visitort *v) override { v->visit(*this); }
+};
+
+class chc_wtot
+{
+private:
+  // A helper class to extend an unsigned number with +oo;
+  class inf_numt
+  {
+    std::optional<unsigned> m_n;
+
+  public:
+    // +oo
+    inf_numt() : m_n(std::nullopt) { }
+    inf_numt(unsigned n) : m_n(n) { }
+    inf_numt(const inf_numt &o) : m_n(o.m_n) { }
+
+    inf_numt &operator=(inf_numt o)
+    {
+      m_n = o.m_n;
+      return *this;
+    }
+
+    bool is_plus_infinite() const { return m_n == std::nullopt; }
+    bool is_finite() const { return !is_plus_infinite(); }
+
+    unsigned number() const
+    {
+      INVARIANT(is_finite(), "Cannot call number() on infinite");
+      return *m_n;
+    }
+
+    bool operator==(inf_numt o) const
+    {
+      if(is_plus_infinite() && o.is_plus_infinite())
+        return true;
+
+      if(is_plus_infinite() || o.is_plus_infinite())
+        return false;
+
+      return (number() == o.number());
+    }
+
+    bool operator<=(inf_numt o) const
+    {
+      if(is_plus_infinite() && o.is_plus_infinite())
+        return true;
+
+      if(is_plus_infinite())
+        return false;
+
+      if(o.is_plus_infinite())
+        return true;
+
+      return (number() <= o.number());
+    }
+  };
+
+  typedef std::shared_ptr<wto_elementt> wto_element_ptr;
+  typedef std::deque<wto_element_ptr> partition_t;
+  typedef std::unordered_map<std::size_t , std::vector<wto_componentt>>
+    nested_components_t;
+
+  chc_grapht & m_g;
+
+  std::unordered_map<std::size_t, inf_numt> m_dfn;
+  std::vector<const symbol_exprt*> m_stack;
+  unsigned m_cur_dfn_num;
+
+  std::deque<wto_element_ptr> m_partition;
+  nested_components_t m_nested_comp;
+
+private:
+  // helper to avoid initializing all vertices to zero
+  inf_numt get_dfn(const symbol_exprt* v) const {
+    auto it = m_dfn.find(v->hash());
+    if (it != m_dfn.end())
+      return it->second;
+    return 0;
+  }
+
+  std::deque<wto_element_ptr> component(const symbol_exprt* v) {
+    std::deque<wto_element_ptr> partition;
+    for (auto & target : m_g.outgoing(*v)) {
+      const symbol_exprt* t = (&to_symbol_expr(target));
+      if (get_dfn(t) == 0)
+        visit(t, partition);
+    }
+    return partition;
+  }
+
+  inf_numt visit(const symbol_exprt* v, std::deque<wto_element_ptr> &partition) {
+    std::string name = as_string(v->get_identifier());
+    m_stack.push_back(v);
+    m_dfn[v->hash()] = m_cur_dfn_num++;
+    auto head = get_dfn(v);
+    bool loop = false;
+    for (auto & target : m_g.outgoing(*v)) {
+      const symbol_exprt* t = (&to_symbol_expr(target));
+      auto min = get_dfn(t);
+      if (min == 0)
+        min = visit(t, partition);
+      if (min <= head) {
+        head = min;
+        loop = true;
+      }
+    }
+
+    if (head == get_dfn(v)) { // v is the head of a component
+      m_dfn[v->hash()] = inf_numt();
+      auto element = m_stack.back();
+      m_stack.pop_back();
+      if (loop) {
+        while (!(element == v)) {
+          m_dfn[element->hash()] = 0; // reset
+          element = m_stack.back();
+          m_stack.pop_back();
+        }
+        partition.push_front(std::static_pointer_cast<wto_elementt>(
+          std::make_shared<wto_componentt>(v, component(v))));
+      } else {
+        partition.push_front(std::static_pointer_cast<wto_elementt>(
+          std::make_shared<wto_singletont>(v)));
+      }
+    }
+    return head;
+  }
+
+  class nested_components_visitor : public wto_element_visitort
+  {
+    std::vector<wto_componentt> m_nested_components;
+    nested_components_t &m_nested_components_table;
+
+  public:
+    nested_components_visitor(nested_components_t &t)
+      : wto_element_visitort(), m_nested_components_table(t) {}
+
+    virtual void visit(const wto_singletont &s) override {
+      m_nested_components_table[s.get()->hash()] = m_nested_components;
+    }
+
+    virtual void visit(const wto_componentt &c) override {
+      m_nested_components.push_back(c);
+      m_nested_components_table[c.head()->hash()] = m_nested_components;
+      for (auto &e : c) {
+        e->accept(this);
+      }
+      m_nested_components.pop_back();
+    }
+  };
+
+  // build a map from graph vertex to nested components in the wto
+  void build_nested_components() {
+    nested_components_visitor vis(m_nested_comp);
+    for (auto c : m_partition) {
+      c->accept(&vis);
+    }
+  }
+
+public:
+  chc_wtot(chc_grapht & g) : m_g(g), m_cur_dfn_num(0) {}
+
+  void build_wto() {
+    if (!m_g.has_entry())
+    {
+      throw incorrect_goto_program_exceptiont("No entry point to CHC");
+    }
+    visit(m_g.entry(), m_partition);
+    build_nested_components();
+    // cleanup
+    m_stack.clear();
+    m_dfn.clear();
+  }
+
+  partition_t::iterator begin() { return m_partition.begin(); }
+  partition_t::iterator end() { return m_partition.end(); }
+  partition_t::const_iterator begin() const { return m_partition.begin(); }
+  partition_t::const_iterator end() const { return m_partition.end(); }
+
+  std::vector<wto_componentt>::iterator nested_comp_begin(symbol_exprt* p) {
+    return m_nested_comp[p->hash()].begin();
+  }
+  std::vector<wto_componentt>::iterator nested_comp_end(symbol_exprt* p) {
+    return m_nested_comp[p->hash()].end();
+  }
+  std::vector<wto_componentt>::const_iterator nested_comp_begin(symbol_exprt* p) const {
+    auto it = m_nested_comp.find(p->hash());
+    INVARIANT(it != m_nested_comp.end(), "No nested component");
+    return it->second.begin();
+  }
+  std::vector<wto_componentt>::const_iterator nested_comp_end(symbol_exprt* p) const {
+    auto it = m_nested_comp.find(p->hash());
+    INVARIANT(it != m_nested_comp.end(), "No nested component");
+    return it->second.end();
+  }
+};
+
+class simple_visitort : public wto_element_visitort
+{
+  virtual void visit(const wto_singletont & s)
+  {
+    const symbol_exprt* symb = s.get();
+    std::string str = as_string(symb->get_identifier());
+    std::cout  << str << " ";
+  }
+
+  virtual void visit(const wto_componentt & comp)
+  {
+    const symbol_exprt* head = comp.head();
+    std::string str = head->get_identifier().c_str();
+    std::cout << "(" << str << " ";
+    for (auto it = comp.begin(); it != comp.end(); it++)
+    {
+      it->get()->accept(this);
+    }
+    std::cout << ")" << " ";
+  }
+};
+
+#endif //CBMC_CHC_WTO_H
diff --git a/src/cprover/cprover_parse_options.cpp b/src/cprover/cprover_parse_options.cpp
index c5993023c0b..35dc1435e01 100644
--- a/src/cprover/cprover_parse_options.cpp
+++ b/src/cprover/cprover_parse_options.cpp
@@ -277,6 +277,7 @@ int cprover_parse_optionst::main()
 
     solver_options.trace = cmdline.isset("trace");
     solver_options.verbose = cmdline.isset("verbose");
+    solver_options.large_step = cmdline.isset("large-step");
 
     // solve
     auto result = state_encoding_solver(
diff --git a/src/cprover/cprover_parse_options.h b/src/cprover/cprover_parse_options.h
index 3204b20ef6b..a41d9820ae3 100644
--- a/src/cprover/cprover_parse_options.h
+++ b/src/cprover/cprover_parse_options.h
@@ -25,8 +25,10 @@ Author: Daniel Kroening, dkr@amazon.com
   "(show-goto-functions)(show-loops)(show-properties)"                         \
   "(show-functions-with-loops)"                                                \
   "(validate-goto-model)"                                                      \
+  "(large-step)"                                                               \
   "(verbose)"
 
+
 class cprover_parse_optionst
 {
 public:
diff --git a/src/cprover/cutpoint_graph.cpp b/src/cprover/cutpoint_graph.cpp
new file mode 100644
index 00000000000..4fa0d784211
--- /dev/null
+++ b/src/cprover/cutpoint_graph.cpp
@@ -0,0 +1,230 @@
+//
+// Created by Yakir Vizel on 5/1/24.
+//
+
+#include "cutpoint_graph.h"
+#include "language_util.h"
+
+#include <iostream>
+#include <fstream>
+
+cutpoint_grapht::~cutpoint_grapht() {
+  m_edges.clear();
+  m_cps.clear();
+  m_insts.clear();
+}
+
+void cutpoint_grapht::run(const goto_functiont & goto_function)
+{
+  compute_cutpoints(goto_function);
+  compute_fwd_reach(goto_function);
+  compute_bwd_reach(goto_function);
+  compute_edges(goto_function);
+
+  to_dot(goto_function, "cp.dot");
+}
+
+void cutpoint_grapht::to_dot(const goto_functiont & f, std::string filename)
+{
+  std::ofstream out;
+  out.open(filename);
+  out << "digraph G {\n";
+  out << "color=black\nfontsize=20" << '\n';
+
+  const namespacet ns(m_goto_model.symbol_table);
+
+  for (auto cp : m_cps)
+  {
+    cp->to_dot(out, ns);
+  }
+
+  for (auto edge : m_edges)
+  {
+    out << "Node_" << edge->source().id();
+    out << " -> ";
+    out << "Node_" << edge->target().id();
+    std::string label;
+    for (auto inst : *edge)
+    {
+      std::string code;
+      if (inst->is_assign())
+      {
+        code = from_expr(ns, goto_functionst::entry_point(), inst->code());
+      }
+      label += inst->to_string() +": " + code + "\n";
+    }
+    out << "[fontsize=22,label=\"" << label << "\"];\n";
+  }
+
+
+  out << "}\n";
+
+  out.close();
+}
+
+cutpoint_edge_ptr cutpoint_grapht::get_edge(const cutpointt &s, const cutpointt &d)
+{
+  for (auto it = s.succ_begin (), end = s.succ_end (); it != end; ++it)
+  {
+    cutpoint_edge_ptr edg = *it;
+    if (&(edg->target ()) == &d) return edg;
+  }
+
+  return nullptr;
+}
+
+const cutpoint_edge_ptr
+cutpoint_grapht::getEdge(const cutpointt &s, const cutpointt &d) const
+{
+  for (auto it = s.succ_begin (), end = s.succ_end (); it != end; ++it)
+  {
+    cutpoint_edge_ptr edg = *it;
+    if (&(edg->target ()) == &d) return edg;
+  }
+
+  return nullptr;
+}
+
+void cutpoint_grapht::compute_edges(const goto_functiont &goto_function)
+{
+  forall_goto_program_instructions(it, goto_function.body)
+  {
+    if (is_cutpoint(*it))
+    {
+      std::vector<bool> & reach = m_fwd[&(*it)];
+      cutpointt & cp = get_cutpoint(*it);
+
+      for (std::size_t r = 0; r < reach.size(); r++)
+      {
+        if (reach[r] == true)
+        {
+          cutpoint_edge_ptr edg = create_edge(cp, *m_cps[r]);
+          edg->push_back(&(*it));
+        }
+      }
+    }
+    else
+    {
+      std::vector<bool> & breach = m_bwd[&(*it)];
+      std::vector<bool> & freach = m_fwd[&(*it)];
+
+      for (int i = 0; i < breach.size(); i++)
+      {
+        if (breach[i] == false) continue;
+        for (int j = 0; j < freach.size(); j++) {
+          if (freach[j] == false) continue;
+          cutpoint_edge_ptr edge = get_edge(*m_cps[i], *m_cps[j]);
+          edge->push_back(&(*it));
+        }
+      }
+    }
+  }
+}
+
+void cutpoint_grapht::compute_cutpoints(const goto_functiont &goto_function)
+{
+  m_cps.clear();
+
+  std::map<const goto_programt::instructiont*, std::size_t> cp_map;
+
+  forall_goto_program_instructions(it, goto_function.body)
+  {
+    if (cp_map.find(&*it) != cp_map.end()) continue;
+
+    // entry
+    if (it->incoming_edges.empty())
+    {
+      auto i = cp_map.find(&*it);
+      if (i == cp_map.end())
+        cp_map.insert(std::make_pair(&*it, cp_map.size()));
+    }
+
+    // exit
+    if (it->is_end_function())
+    {
+      auto i = cp_map.find(&*it);
+      if (i == cp_map.end())
+        cp_map.insert(std::make_pair(&*it, cp_map.size()));
+    }
+
+    for (auto in : it->incoming_edges)
+    {
+      auto & inst = *in;
+      if (inst.is_backwards_goto())
+      {
+        auto i = cp_map.find(&*it);
+        if (i == cp_map.end())
+          cp_map.insert(std::make_pair(&*it, cp_map.size()));
+      }
+    }
+  }
+
+  forall_goto_program_instructions(it, goto_function.body)
+  {
+    auto i = cp_map.find(&*it);
+    if (i == cp_map.end()) continue;
+    auto inst = i->first;
+    if (is_cutpoint(*inst)) continue;
+
+    m_cps.push_back(std::make_shared<cutpointt>(*this, m_cps.size(), *inst));
+    m_insts.insert(std::make_pair(inst, m_cps.back()));
+  }
+}
+
+void cutpoint_grapht::compute_fwd_reach(const goto_functiont &goto_function)
+{
+
+  for (auto it = goto_function.body.instructions.rbegin(); it != goto_function.body.instructions.rend();)
+  {
+    auto itf = (++it).base();
+    auto succs = goto_function.body.get_successors(itf);
+    //if (succs.empty()) continue;
+    auto inst = &*itf;
+    m_fwd.insert(std::make_pair(inst, reachabilityt()));
+    reachabilityt &r = m_fwd [inst];
+    for (auto succ : succs)
+    {
+      if (is_cutpoint(*succ))
+        r.set(get_cutpoint(*succ).id());
+      else
+        r |= m_fwd[&*succ];
+
+    }
+  }
+}
+
+void cutpoint_grapht::compute_bwd_reach(const goto_functiont &goto_function)
+{
+  forall_goto_program_instructions(it, goto_function.body)
+  {
+    auto inst = &*it;
+    m_bwd.insert(std::make_pair(inst, reachabilityt()));
+    reachabilityt &r = m_bwd[inst];
+    for(auto pred : it->incoming_edges)
+    {
+      if(pred->is_backwards_goto())
+        continue;
+      if(is_cutpoint(*pred))
+        r.set(get_cutpoint(*pred).id());
+      else
+        r |= m_bwd[&*pred];
+
+    }
+  }
+
+  for (auto & cp : m_cps)
+  {
+    auto & inst = cp->inst();
+    reachabilityt &r = m_bwd [&inst];
+
+    for (auto pred : inst.incoming_edges)
+    {
+      if (! pred->is_backwards_goto()) continue;
+      if (is_cutpoint(*pred))
+        r.set(get_cutpoint(*pred).id());
+      else
+        r |= m_bwd[&*pred];
+    }
+  }
+}
+
diff --git a/src/cprover/cutpoint_graph.h b/src/cprover/cutpoint_graph.h
new file mode 100644
index 00000000000..a54a5255653
--- /dev/null
+++ b/src/cprover/cutpoint_graph.h
@@ -0,0 +1,166 @@
+//
+// Created by Yakir Vizel on 5/1/24.
+//
+
+#ifndef CBMC_CUTPOINT_GRAPH_H
+#define CBMC_CUTPOINT_GRAPH_H
+
+#include "goto_model.h"
+#include <vector>
+
+/**
+ * A cut-point graph over goto programs.
+ * The cut-points are:
+ * 1. Entry node
+ * 2. Exit node
+ * 3. Every node that has a back-edge - namely, a loop head.
+ */
+
+class cutpoint_grapht;
+class cutpointt;
+
+class cutpoint_edget
+{
+  friend class cutpoint_grapht;
+
+  cutpointt & m_src;
+  cutpointt & m_dst;
+
+  typedef std::vector<const goto_programt::instructiont *> inst_vect;
+  inst_vect m_insts;
+
+  cutpointt &source() { return m_src; }
+  cutpointt &target() { return m_dst; }
+public:
+  cutpoint_edget(cutpointt & s, cutpointt & d) : m_src(s), m_dst(d) {}
+
+  const cutpoint_grapht & graph() const;
+
+  const cutpointt &source() const { return m_src; }
+  const cutpointt &target() const { return m_dst; }
+
+  void push_back(const goto_programt::instructiont * inst)
+  {
+    m_insts.push_back(inst);
+  }
+
+  typedef inst_vect::iterator iterator;
+  typedef inst_vect::const_iterator const_iterator;
+
+  iterator begin() { return m_insts.begin(); }
+  iterator end() { return m_insts.end(); }
+  const_iterator begin() const { return m_insts.begin(); }
+  const_iterator end() const { return m_insts.end(); }
+};
+
+typedef std::shared_ptr<cutpoint_edget> cutpoint_edge_ptr;
+
+class cutpointt
+{
+  const cutpoint_grapht &m_graph;
+  std::size_t m_id;
+  const goto_programt::instructiont & m_inst;
+
+  typedef std::vector<cutpoint_edge_ptr> edge_vect;
+  edge_vect m_succ;
+
+public:
+  cutpointt(const cutpoint_grapht &p, std::size_t id, const goto_programt::instructiont &inst)
+    : m_graph(p), m_id(id), m_inst(inst) {}
+
+  const cutpoint_grapht &graph() const { return m_graph; }
+  std::size_t id() const { return m_id; }
+  const goto_programt::instructiont &inst() const { return m_inst; }
+
+  void add_succ(cutpoint_edge_ptr & edg) { m_succ.push_back(edg); }
+
+  typedef edge_vect::const_iterator const_iterator;
+  typedef edge_vect::const_reverse_iterator const_reverse_iterator;
+
+  const_iterator succ_begin() const { return m_succ.begin(); }
+  const_iterator succ_end() const { return m_succ.end(); }
+
+  void to_dot(std::ostream & out, const namespacet & ns)
+  {
+    out << "Node_" << m_id << " [shape=Mrecord,fontsize=22,label=\"";
+    out << m_inst.to_string() << "\"];\n";
+  }
+};
+
+class cutpoint_grapht
+{
+  const goto_modelt & m_goto_model;
+
+  typedef std::shared_ptr<cutpointt> cutpoint_ptr;
+  typedef std::vector<cutpoint_ptr> cutpoint_vect;
+
+  typedef std::vector<cutpoint_edge_ptr> edge_vect;
+
+  cutpoint_vect m_cps;
+  edge_vect m_edges;
+
+  class reachabilityt : public std::vector<bool> {
+  public:
+    void set(std::size_t index) {
+      if (index >= size()) resize(index+1, false);
+      (*this)[index] = true;
+    }
+
+    reachabilityt & operator|=(const reachabilityt & other) {
+      if (this->size() < other.size())
+        this->resize(other.size(), false);
+      for (std::size_t i = 0; i < other.size(); i++)
+        (*this)[i] = (*this)[i] || other[i];
+      return *this;
+    }
+  };
+
+  typedef std::map<const goto_programt::instructiont*, reachabilityt>
+    inst_bool_mapt;
+
+  inst_bool_mapt m_fwd;
+  inst_bool_mapt m_bwd;
+
+  std::map<const goto_programt::instructiont*, std::shared_ptr<cutpointt>> m_insts;
+
+  cutpoint_edge_ptr create_edge(cutpointt &s, cutpointt &d) {
+    m_edges.push_back(std::make_shared<cutpoint_edget>(s, d));
+
+    cutpoint_edge_ptr edg = m_edges.back();
+
+    s.add_succ(edg);
+    return edg;
+  }
+
+  void compute_cutpoints(const goto_functiont & goto_function);
+  void compute_fwd_reach(const goto_functiont & goto_function);
+  void compute_bwd_reach(const goto_functiont & goto_function);
+  void compute_edges(const goto_functiont & goto_function);
+
+  void to_dot(const goto_functiont & f, std::string filename);
+
+public:
+  cutpoint_grapht(const goto_modelt & goto_model) : m_goto_model(goto_model) {}
+  ~cutpoint_grapht();
+
+  void run(const goto_functiont & goto_function);
+
+  bool is_cutpoint(const goto_programt::instructiont & inst) const
+  {
+    return m_insts.count(&inst) > 0;
+  }
+
+  cutpointt &get_cutpoint(const goto_programt::instructiont & inst) const {
+    INVARIANT(is_cutpoint(inst), "Function should be called with a cutpoint");
+    return *(m_insts.find(&inst)->second);
+  }
+
+  cutpoint_edge_ptr get_edge(const cutpointt &s, const cutpointt &d);
+  const cutpoint_edge_ptr getEdge(const cutpointt &s, const cutpointt &d) const;
+};
+
+inline const cutpoint_grapht &cutpoint_edget::graph() const { return m_src.graph(); }
+
+
+
+#endif //CBMC_CUTPOINT_GRAPH_H
diff --git a/src/cprover/state_encoding.cpp b/src/cprover/state_encoding.cpp
index 56ef744c049..ad0ee44d9c4 100644
--- a/src/cprover/state_encoding.cpp
+++ b/src/cprover/state_encoding.cpp
@@ -26,6 +26,8 @@ Author: Daniel Kroening, dkr@amazon.com
 #include "state_encoding_targets.h"
 #include "variable_encoding.h"
 
+#include "chc_large_step.h"
+
 #include <algorithm>
 #include <iostream>
 
@@ -1233,6 +1235,56 @@ void variable_encoding(
   }
 }
 
+void large_step_encoding(const container_encoding_targett & small_step_container,
+                         container_encoding_targett & large_step_container)
+{
+  chc_dbt db;
+  for (auto & clause : small_step_container.constraints) {
+    if (!can_cast_expr<forall_exprt>(clause))
+    {
+      throw incorrect_goto_program_exceptiont("Not forall");
+    }
+    const forall_exprt& forall = to_forall_expr(clause);
+    db.add_clause(forall);
+
+    // For now add every function application as uninterpreted predicate.
+    std::set<symbol_exprt> symbols;
+    forall.visit_pre([&symbols](const exprt &expr) {
+                       if (can_cast_expr<function_application_exprt>(expr))
+                       {
+                         symbol_exprt s = to_symbol_expr(to_function_application_expr(expr).function());
+                         symbols.insert(s);
+                       }
+                     });
+
+    for (auto & s : symbols)
+    {
+      db.add_state_pred(s);
+    }
+  }
+  chc_grapht chc_g(db);
+  chc_g.build_graph();
+
+  chc_wtot wto(chc_g);
+  wto.build_wto();
+
+  resolution_visitort rv(db);
+  for (auto it = wto.begin(); it != wto.end(); it++)
+  {
+    auto x = (*it);
+    x->accept(&rv);
+  }
+
+  rv.populate_new_db();
+
+  container_encoding_targett container2;
+  std::vector<horn_clauset> all2;
+  for (auto & ce : rv.giveme_new_db())
+  {
+    large_step_container << ce.get_chc();
+  }
+}
+
 solver_resultt state_encoding_solver(
   const goto_modelt &goto_model,
   bool program_is_inlined,
@@ -1254,5 +1306,14 @@ solver_resultt state_encoding_solver(
   }
 #endif
 
+  if (solver_options.large_step) {
+    container_encoding_targett large_step_container;
+    large_step_encoding(container, large_step_container);
+
+    std::cout << "Solving large-step\n";
+    return solver(large_step_container.constraints, solver_options, ns);
+  }
+
+  std::cout << "Solving small-step\n";
   return solver(container.constraints, solver_options, ns);
 }