diff --git a/src/muz/base/dl_rule_set.cpp b/src/muz/base/dl_rule_set.cpp
index 5114fdca4..80af80266 100644
--- a/src/muz/base/dl_rule_set.cpp
+++ b/src/muz/base/dl_rule_set.cpp
@@ -31,7 +31,7 @@ namespace datalog {
     rule_dependencies::rule_dependencies(const rule_dependencies & o, bool reversed):
         m_context(o.m_context) {
         if (reversed) {
-            for (auto & kv : o) { 
+            for (auto & kv : o) {
                 func_decl * pred = kv.m_key;
                 item_set & orig_items = *kv.get_value();
 
@@ -114,8 +114,8 @@ namespace datalog {
                 app* a = to_app(e);
                 d = a->get_decl();
                 if (m_context.is_predicate(d)) {
-                    // insert d and ensure the invariant 
-                    // that every predicate is present as 
+                    // insert d and ensure the invariant
+                    // that every predicate is present as
                     // a key in m_data
                     s.insert(d);
                     ensure_key(d);
@@ -148,7 +148,7 @@ namespace datalog {
             item_set& itms = *kv.get_value();
             set_intersection(itms, allowed);
         }
-        for (func_decl* f : to_remove) 
+        for (func_decl* f : to_remove)
             remove_m_data_entry(f);
     }
 
@@ -253,18 +253,18 @@ namespace datalog {
     //
     // -----------------------------------
 
-    rule_set::rule_set(context & ctx) 
-          : m_context(ctx), 
-            m_rule_manager(ctx.get_rule_manager()), 
-            m_rules(m_rule_manager), 
+    rule_set::rule_set(context & ctx)
+          : m_context(ctx),
+            m_rule_manager(ctx.get_rule_manager()),
+            m_rules(m_rule_manager),
             m_deps(ctx),
             m_stratifier(nullptr),
             m_refs(ctx.get_manager()) {
     }
 
-    rule_set::rule_set(const rule_set & other) 
-        : m_context(other.m_context), 
-          m_rule_manager(other.m_rule_manager), 
+    rule_set::rule_set(const rule_set & other)
+        : m_context(other.m_context),
+          m_rule_manager(other.m_rule_manager),
           m_rules(m_rule_manager),
           m_deps(other.m_context),
           m_stratifier(nullptr),
@@ -353,10 +353,27 @@ namespace datalog {
                 break;                                  \
             }                                           \
         }                                               \
-        
+
         DEL_VECTOR(*rules);
         DEL_VECTOR(m_rules);
-    }    
+    }
+
+    void rule_set::replace_rule(rule * r, rule * other) {
+        TRACE("dl", r->display(m_context, tout << "replace:"););
+        func_decl* d = r->get_decl();
+        rule_vector* rules = m_head2rules.find(d);
+#define REPLACE_VECTOR(_v)                              \
+        for (unsigned i = (_v).size(); i > 0; ) {       \
+            --i;                                        \
+            if ((_v)[i] == r) {                         \
+                (_v)[i] = other;                        \
+                break;                                  \
+            }                                           \
+        }                                               \
+
+        REPLACE_VECTOR(*rules);
+        REPLACE_VECTOR(m_rules);
+    }
 
     void rule_set::ensure_closed() {
         if (!is_closed()) {
@@ -365,7 +382,7 @@ namespace datalog {
     }
 
     bool rule_set::close() {
-        SASSERT(!is_closed()); //the rule_set is not already closed        
+        SASSERT(!is_closed()); //the rule_set is not already closed
         m_deps.populate(*this);
         m_stratifier = alloc(rule_stratifier, m_deps);
         if (!stratified_negation()) {
@@ -426,7 +443,7 @@ namespace datalog {
         inherit_predicates(src);
     }
 
-    const rule_vector & rule_set::get_predicate_rules(func_decl * pred) const { 
+    const rule_vector & rule_set::get_predicate_rules(func_decl * pred) const {
         decl2rules::obj_map_entry * e = m_head2rules.find_core(pred);
         if (!e) {
             return m_empty_rule_vector;
@@ -519,7 +536,7 @@ namespace datalog {
                 out << "\n";
                 non_empty = false;
             }
-            
+
             for (func_decl * first : *strat) {
                 const func_decl_set & deps = m_deps.get_deps(first);
                 for (func_decl * dep : deps) {
@@ -545,8 +562,8 @@ namespace datalog {
     unsigned rule_stratifier::get_predicate_strat(func_decl * pred) const {
         unsigned num;
         if (!m_pred_strat_nums.find(pred, num)) {
-            //the number of the predicate is not stored, therefore it did not appear 
-            //in the algorithm and therefore it does not depend on anything and nothing 
+            //the number of the predicate is not stored, therefore it did not appear
+            //in the algorithm and therefore it does not depend on anything and nothing
             //depends on it. So it is safe to assign zero strate to it, although it is
             //not strictly true.
             num = 0;
@@ -641,7 +658,7 @@ namespace datalog {
         }
 
 
-        // We put components whose indegree is zero to m_strats and assign its 
+        // We put components whose indegree is zero to m_strats and assign its
         // m_components entry to zero.
         unsigned comp_cnt = m_components.size();
         for (unsigned i = 0; i < comp_cnt; i++) {
@@ -680,7 +697,7 @@ namespace datalog {
             strats_index++;
         }
         //we have managed to topologicaly order all the components
-        SASSERT(std::find_if(m_components.begin(), m_components.end(), 
+        SASSERT(std::find_if(m_components.begin(), m_components.end(),
             std::bind1st(std::not_equal_to<item_set*>(), (item_set*)0)) == m_components.end());
 
         //reverse the strats array, so that the only the later components would depend on earlier ones
@@ -713,7 +730,7 @@ namespace datalog {
             }
             out << "\n";
         }
-        
+
     }
 
 };
diff --git a/src/muz/base/dl_rule_set.h b/src/muz/base/dl_rule_set.h
index 736dd8888..e870e369c 100644
--- a/src/muz/base/dl_rule_set.h
+++ b/src/muz/base/dl_rule_set.h
@@ -77,7 +77,7 @@ namespace datalog {
            \brief Number of predicates that depend on \c f.
          */
         unsigned out_degree(func_decl * f) const;
-        
+
         /**
            \brief If the rependency graph is acyclic, put all elements into \c res
              ordered so that elements can depend only on elements that are before them.
@@ -131,7 +131,7 @@ namespace datalog {
             it must exist for the whole lifetime of the \c stratifier object.
         */
         rule_stratifier(const rule_dependencies & deps)
-            : m_deps(deps), m_next_preorder(0) 
+            : m_deps(deps), m_next_preorder(0)
         {
             process();
         }
@@ -145,7 +145,7 @@ namespace datalog {
         const comp_vector & get_strats() const { return m_strats; }
 
         unsigned get_predicate_strat(func_decl * pred) const;
-        
+
         void display( std::ostream & out ) const;
     };
 
@@ -203,6 +203,10 @@ namespace datalog {
            \brief Remove rule \c r from the rule set.
         */
         void del_rule(rule * r);
+        /**
+           \brief Replace a rule \c r with the rule \c other
+        */
+        void replace_rule(rule * r, rule * other);
 
         /**
            \brief Add all rules from a different rule_set.
@@ -276,8 +280,7 @@ namespace datalog {
     inline std::ostream& operator<<(std::ostream& out, rule_set const& r) { r.display(out); return out; }
 
 
-    
+
 };
 
 #endif /* DL_RULE_SET_H_ */
-
diff --git a/src/muz/base/fp_params.pyg b/src/muz/base/fp_params.pyg
index 8cee99540..18eb85662 100644
--- a/src/muz/base/fp_params.pyg
+++ b/src/muz/base/fp_params.pyg
@@ -177,5 +177,6 @@ def_module_params('fp',
                           ('spacer.dump_threshold', DOUBLE, 5.0, 'Threshold in seconds on dumping benchmarks'),
                           ('spacer.gpdr', BOOL, False, 'Use GPDR solving strategy for non-linear CHC'),
                           ('spacer.gpdr.bfs', BOOL, True, 'Use BFS exploration strategy for expanding model search'),
+                          ('spacer.use_bg_invs', BOOL, False, 'Enable external background invariants'),
 
                           ))
diff --git a/src/muz/spacer/spacer_context.cpp b/src/muz/spacer/spacer_context.cpp
index f0e86f1a5..dd6656954 100644
--- a/src/muz/spacer/spacer_context.cpp
+++ b/src/muz/spacer/spacer_context.cpp
@@ -493,7 +493,8 @@ lemma::lemma (ast_manager &manager, expr * body, unsigned lvl) :
     m_pob(nullptr), m_ctp(nullptr),
     m_lvl(lvl), m_init_lvl(m_lvl),
     m_bumped(0), m_weakness(WEAKNESS_MAX),
-    m_external(false), m_blocked(false) {
+    m_external(false), m_blocked(false),
+    m_background(false) {
     SASSERT(m_body);
     normalize(m_body, m_body);
 }
@@ -505,7 +506,8 @@ lemma::lemma(pob_ref const &p) :
     m_pob(p), m_ctp(nullptr),
     m_lvl(p->level()), m_init_lvl(m_lvl),
     m_bumped(0), m_weakness(p->weakness()),
-    m_external(false), m_blocked(false) {
+    m_external(false), m_blocked(false),
+    m_background(false) {
     SASSERT(m_pob);
     m_pob->get_skolems(m_zks);
     add_binding(m_pob->get_binding());
@@ -519,8 +521,8 @@ lemma::lemma(pob_ref const &p, expr_ref_vector &cube, unsigned lvl) :
     m_pob(p), m_ctp(nullptr),
     m_lvl(p->level()), m_init_lvl(m_lvl),
     m_bumped(0), m_weakness(p->weakness()),
-    m_external(false), m_blocked(false)
-{
+    m_external(false), m_blocked(false),
+    m_background(false) {
     if (m_pob) {
         m_pob->get_skolems(m_zks);
         add_binding(m_pob->get_binding());
@@ -921,10 +923,10 @@ void pred_transformer::simplify_formulas()
 {m_frames.simplify_formulas ();}
 
 
-expr_ref pred_transformer::get_formulas(unsigned level) const
+expr_ref pred_transformer::get_formulas(unsigned level, bool bg) const
 {
     expr_ref_vector res(m);
-    m_frames.get_frame_geq_lemmas (level, res);
+    m_frames.get_frame_geq_lemmas (level, res, bg);
     return mk_and(res);
 }
 
@@ -935,6 +937,7 @@ bool pred_transformer::propagate_to_next_level (unsigned src_level)
 /// \brief adds a lemma to the solver and to child solvers
 void pred_transformer::add_lemma_core(lemma* lemma, bool ground_only)
 {
+    SASSERT(!lemma->is_background());
     unsigned lvl = lemma->level();
     expr* l = lemma->get_expr();
     SASSERT(!lemma->is_ground() || is_clause(m, l));
@@ -975,8 +978,9 @@ void pred_transformer::add_lemma_core(lemma* lemma, bool ground_only)
                                       next_level(lvl), ground_only); }
 }
 
-bool pred_transformer::add_lemma (expr *e, unsigned lvl) {
+bool pred_transformer::add_lemma (expr *e, unsigned lvl, bool bg) {
     lemma_ref lem = alloc(lemma, m, e, lvl);
+    lem->set_background(bg);
     return m_frames.add_lemma(lem.get());
 }
 
@@ -1217,15 +1221,18 @@ expr_ref pred_transformer::get_origin_summary (model &mdl,
 }
 
 
-void pred_transformer::add_cover(unsigned level, expr* property)
+void pred_transformer::add_cover(unsigned level, expr* property, bool bg)
 {
+    SASSERT(!bg || is_infty_level(level));
     // replace bound variables by local constants.
     expr_ref result(property, m), v(m), c(m);
     expr_substitution sub(m);
+    proof_ref pr(m);
+    pr = m.mk_asserted(m.mk_true());
     for (unsigned i = 0; i < sig_size(); ++i) {
         c = m.mk_const(pm.o2n(sig(i), 0));
         v = m.mk_var(i, sig(i)->get_range());
-        sub.insert(v, c);
+        sub.insert(v, c, pr);
     }
     scoped_ptr<expr_replacer> rep = mk_default_expr_replacer(m);
     rep->set_substitution(&sub);
@@ -1236,13 +1243,38 @@ void pred_transformer::add_cover(unsigned level, expr* property)
     expr_ref_vector lemmas(m);
     flatten_and(result, lemmas);
     for (unsigned i = 0, sz = lemmas.size(); i < sz; ++i) {
-        add_lemma(lemmas.get(i), level);
+        add_lemma(lemmas.get(i), level, bg);
     }
 }
 
 void pred_transformer::propagate_to_infinity (unsigned level)
 {m_frames.propagate_to_infinity (level);}
 
+// compute a conjunction of all background facts
+void pred_transformer::get_pred_bg_invs(expr_ref_vector& out) {
+    expr_ref inv(m), tmp1(m), tmp2(m);
+    ptr_vector<func_decl> preds;
+    for (auto kv : m_pt_rules) {
+        expr* tag = kv.m_value->tag();
+        datalog::rule const &r = kv.m_value->rule();
+        find_predecessors (r, preds);
+
+        for (unsigned i = 0, preds_sz = preds.size(); i < preds_sz; i++) {
+            func_decl* pre = preds[i];
+            pred_transformer &pt = ctx.get_pred_transformer(pre);
+            const lemma_ref_vector &invs = pt.get_bg_invs();
+            CTRACE("spacer", !invs.empty(),
+                   tout << "add-bg-invariant: " << mk_pp (pre, m) << "\n";);
+            for (auto inv : invs) {
+                // tag -> inv1 ...  tag -> invn
+                tmp1 = m.mk_implies(tag, inv->get_expr());
+                pm.formula_n2o(tmp1, tmp2, i);
+                out.push_back(tmp2);
+                TRACE("spacer", tout << tmp2 << "\n";);
+            }
+        }
+    }
+}
 
 
 /// \brief Returns true if the obligation is already blocked by current lemmas
@@ -1344,6 +1376,14 @@ lbool pred_transformer::is_reachable(pob& n, expr_ref_vector* core,
 
     expr_ref_vector post (m), reach_assumps (m);
     post.push_back (n.post ());
+    flatten_and(post);
+
+    // if equality propagation is disabled in arithmetic, expand
+    // equality literals into two inequalities to increase the space
+    // for interpolation
+    if (!ctx.use_eq_prop()) {
+        expand_literals(m, post);
+    }
 
     // populate reach_assumps
     if (n.level () > 0 && !m_all_init) {
@@ -1472,7 +1512,7 @@ bool pred_transformer::is_invariant(unsigned level, lemma* lem,
     expr_ref lemma_expr(m);
     lemma_expr = lem->get_expr();
 
-    expr_ref_vector conj(m), aux(m);
+    expr_ref_vector cand(m), aux(m), conj(m);
     expr_ref gnd_lemma(m);
 
 
@@ -1482,8 +1522,8 @@ bool pred_transformer::is_invariant(unsigned level, lemma* lem,
         lemma_expr = gnd_lemma.get();
     }
 
-    conj.push_back(mk_not(m, lemma_expr));
-    flatten_and (conj);
+    cand.push_back(mk_not(m, lemma_expr));
+    flatten_and (cand);
 
     prop_solver::scoped_level _sl(*m_solver, level);
     prop_solver::scoped_subset_core _sc (*m_solver, true);
@@ -1494,9 +1534,12 @@ bool pred_transformer::is_invariant(unsigned level, lemma* lem,
     if (ctx.use_ctp()) {mdl_ref_ptr = &mdl;}
     m_solver->set_core(core);
     m_solver->set_model(mdl_ref_ptr);
-    expr * bg = m_extend_lit.get ();
-    lbool r = m_solver->check_assumptions (conj, aux, m_transition_clause,
-                                          1, &bg, 1);
+
+    conj.push_back(m_extend_lit);
+    if (ctx.use_bg_invs()) get_pred_bg_invs(conj);
+
+    lbool r = m_solver->check_assumptions (cand, aux, m_transition_clause,
+                                           conj.size(), conj.c_ptr(), 1);
     if (r == l_false) {
         solver_level = m_solver->uses_level ();
         lem->reset_ctp();
@@ -1527,6 +1570,7 @@ bool pred_transformer::check_inductive(unsigned level, expr_ref_vector& state,
     m_solver->set_core(&core);
     m_solver->set_model (nullptr);
     expr_ref_vector aux (m);
+    if (ctx.use_bg_invs()) get_pred_bg_invs(conj);
     conj.push_back (m_extend_lit);
     lbool res = m_solver->check_assumptions (state, aux,
                                             m_transition_clause,
@@ -1941,14 +1985,27 @@ void pred_transformer::update_solver_with_rfs(prop_solver *solver,
 }
 
 /// pred_transformer::frames
-
-
 bool pred_transformer::frames::add_lemma(lemma *new_lemma)
 {
     TRACE("spacer", tout << "add-lemma: " << pp_level(new_lemma->level()) << " "
           << m_pt.head()->get_name() << " "
           << mk_pp(new_lemma->get_expr(), m_pt.get_ast_manager()) << "\n";);
 
+    if (new_lemma->is_background()) {
+        SASSERT (is_infty_level(new_lemma->level()));
+
+        for (auto &l : m_bg_invs) {
+            if (l->get_expr() == new_lemma->get_expr()) return false;
+        }
+        TRACE("spacer", tout << "add-external-lemma: "
+              << pp_level(new_lemma->level()) << " "
+              << m_pt.head()->get_name() << " "
+              << mk_pp(new_lemma->get_expr(), m_pt.get_ast_manager()) << "\n";);
+
+        m_bg_invs.push_back(new_lemma);
+        return true;
+    }
+
     unsigned i = 0;
     for (auto *old_lemma : m_lemmas) {
         if (old_lemma->get_expr() == new_lemma->get_expr()) {
@@ -2295,6 +2352,7 @@ void context::updt_params() {
     m_use_restarts = m_params.spacer_restarts();
     m_restart_initial_threshold = m_params.spacer_restart_initial_threshold();
     m_pdr_bfs = m_params.spacer_gpdr_bfs();
+    m_use_bg_invs = m_params.spacer_use_bg_invs();
 
     if (m_use_gpdr) {
         // set options to be compatible with GPDR
@@ -2423,36 +2481,38 @@ expr_ref context::get_cover_delta(int level, func_decl* p_orig, func_decl* p)
     if (m_rels.find(p, pt)) {
         return pt->get_cover_delta(p_orig, level);
     } else {
-        IF_VERBOSE(10, verbose_stream() << "did not find predicate " << p->get_name() << "\n";);
+        IF_VERBOSE(10, verbose_stream() << "did not find predicate "
+                   << p->get_name() << "\n";);
         return expr_ref(m.mk_true(), m);
     }
 }
 
-void context::add_cover(int level, func_decl* p, expr* property)
+void context::add_cover(int level, func_decl* p, expr* property, bool bg)
 {
+    scoped_proof _pf_(m);
+
     pred_transformer* pt = nullptr;
     if (!m_rels.find(p, pt)) {
         pt = alloc(pred_transformer, *this, get_manager(), p);
         m_rels.insert(p, pt);
-        IF_VERBOSE(10, verbose_stream() << "did not find predicate " << p->get_name() << "\n";);
+        IF_VERBOSE(10, verbose_stream() << "did not find predicate "
+                   << p->get_name() << "\n";);
     }
     unsigned lvl = (level == -1)?infty_level():((unsigned)level);
-    pt->add_cover(lvl, property);
+    pt->add_cover(lvl, property, bg);
 }
 
 void context::add_invariant (func_decl *p, expr *property)
-{add_cover (infty_level(), p, property);}
+{add_cover (infty_level(), p, property, true);}
 
-expr_ref context::get_reachable(func_decl *p)
-{
+expr_ref context::get_reachable(func_decl *p) {
     pred_transformer* pt = nullptr;
     if (!m_rels.find(p, pt))
     { return expr_ref(m.mk_false(), m); }
     return pt->get_reachable();
 }
 
-bool context::validate()
-{
+bool context::validate() {
     if (!m_validate_result) { return true; }
 
     std::stringstream msg;
@@ -2483,7 +2543,7 @@ bool context::validate()
         model_ref model;
         vector<relation_info> rs;
         model_converter_ref mc;
-        get_level_property(m_inductive_lvl, refs, rs);
+        get_level_property(m_inductive_lvl, refs, rs, use_bg_invs());
         inductive_property ex(m, mc, rs);
         ex.to_model(model);
         var_subst vs(m, false);
@@ -2624,13 +2684,13 @@ void context::init_lemma_generalizers()
 }
 
 void context::get_level_property(unsigned lvl, expr_ref_vector& res,
-                                 vector<relation_info>& rs) const {
+                                 vector<relation_info>& rs, bool with_bg) const {
     for (auto const& kv : m_rels) {
         pred_transformer* r = kv.m_value;
         if (r->head() == m_query_pred) {
             continue;
         }
-        expr_ref conj = r->get_formulas(lvl);
+        expr_ref conj = r->get_formulas(lvl, with_bg);
         m_pm.formula_n2o(0, false, conj);
         res.push_back(conj);
         ptr_vector<func_decl> sig(r->head()->get_arity(), r->sig());
@@ -2662,7 +2722,7 @@ lbool context::solve(unsigned from_lvl)
             IF_VERBOSE(1, {
                     expr_ref_vector refs(m);
                     vector<relation_info> rs;
-                    get_level_property(m_inductive_lvl, refs, rs);
+                    get_level_property(m_inductive_lvl, refs, rs, use_bg_invs());
                     model_converter_ref mc;
                     inductive_property ex(m, mc, rs);
                     verbose_stream() << ex.to_string();
@@ -2844,7 +2904,7 @@ model_ref context::get_model()
     model_ref model;
     expr_ref_vector refs(m);
     vector<relation_info> rs;
-    get_level_property(m_inductive_lvl, refs, rs);
+    get_level_property(m_inductive_lvl, refs, rs, use_bg_invs());
     inductive_property ex(m, const_cast<model_converter_ref&>(m_mc), rs);
     ex.to_model (model);
     return model;
@@ -2877,7 +2937,7 @@ expr_ref context::mk_unsat_answer() const
 {
     expr_ref_vector refs(m);
     vector<relation_info> rs;
-    get_level_property(m_inductive_lvl, refs, rs);
+    get_level_property(m_inductive_lvl, refs, rs, use_bg_invs());
     inductive_property ex(m, const_cast<model_converter_ref&>(m_mc), rs);
     return ex.to_expr();
 }
diff --git a/src/muz/spacer/spacer_context.h b/src/muz/spacer/spacer_context.h
index 48c27f96d..0d8b2daf6 100644
--- a/src/muz/spacer/spacer_context.h
+++ b/src/muz/spacer/spacer_context.h
@@ -128,8 +128,9 @@ class lemma {
     unsigned m_init_lvl;       // level at which lemma was created
     unsigned m_bumped:16;
     unsigned m_weakness:16;
-    unsigned m_external:1;
-    unsigned m_blocked:1;
+    unsigned m_external:1;    // external lemma from another solver
+    unsigned m_blocked:1;     // blocked by CTP
+    unsigned m_background:1;  // background assumed fact
 
     void mk_expr_core();
     void mk_cube_core();
@@ -163,6 +164,9 @@ public:
     void set_external(bool ext){m_external = ext;}
     bool external() { return m_external;}
 
+    void set_background(bool v) {m_background = v;}
+    bool is_background() {return m_background;}
+
     bool is_blocked() {return m_blocked;}
     void set_blocked(bool v) {m_blocked=v;}
 
@@ -222,6 +226,7 @@ class pred_transformer {
         pred_transformer &m_pt;            // parent pred_transformer
         lemma_ref_vector m_pinned_lemmas;  // all created lemmas
         lemma_ref_vector m_lemmas;         // active lemmas
+        lemma_ref_vector m_bg_invs;        // background (assumed) invariants
         unsigned m_size;                   // num of frames
 
         bool m_sorted;                     // true if m_lemmas is sorted by m_lt
@@ -230,7 +235,8 @@ class pred_transformer {
         void sort ();
 
     public:
-        frames (pred_transformer &pt) : m_pt (pt), m_size(0), m_sorted (true) {}
+        frames (pred_transformer &pt) : m_pt (pt),
+                                        m_size(0), m_sorted (true) {}
         ~frames() {}
         void simplify_formulas ();
 
@@ -245,17 +251,25 @@ class pred_transformer {
                 }
             }
         }
-        void get_frame_geq_lemmas (unsigned level, expr_ref_vector &out) const {
+        void get_frame_geq_lemmas (unsigned level, expr_ref_vector &out,
+                                   bool with_bg = false) const {
             for (auto &lemma : m_lemmas) {
                 if (lemma->level() >= level) {
                     out.push_back(lemma->get_expr());
                 }
             }
+            if (with_bg) {
+                for (auto &lemma : m_bg_invs)
+                    out.push_back(lemma->get_expr());
+            }
         }
 
-        unsigned size () const {return m_size;}
-        unsigned lemma_size () const {return m_lemmas.size ();}
-        void add_frame () {m_size++;}
+        const lemma_ref_vector& get_bg_invs() const {return m_bg_invs;}
+        unsigned size() const {return m_size;}
+        unsigned lemma_size() const {return m_lemmas.size ();}
+        unsigned bg_invs_size() const {return m_bg_invs.size();}
+
+        void add_frame() {m_size++;}
         void inherit_frames (frames &other) {
             for (auto &other_lemma : other.m_lemmas) {
                 lemma_ref new_lemma = alloc(lemma, m_pt.get_ast_manager(),
@@ -265,6 +279,7 @@ class pred_transformer {
                 add_lemma(new_lemma.get());
             }
             m_sorted = false;
+            m_bg_invs.append(other.m_bg_invs);
         }
 
         bool add_lemma (lemma *new_lemma);
@@ -418,6 +433,11 @@ class pred_transformer {
 
     app_ref mk_fresh_rf_tag ();
 
+    // get tagged formulae of all of the background invariants for all of the
+    // predecessors of the current transformer
+    void get_pred_bg_invs(expr_ref_vector &out);
+    const lemma_ref_vector &get_bg_invs() const {return m_frames.get_bg_invs();}
+
 public:
     pred_transformer(context& ctx, manager& pm, func_decl* head);
     ~pred_transformer() {}
@@ -448,7 +468,7 @@ public:
     }
     unsigned get_num_levels() const {return m_frames.size ();}
     expr_ref get_cover_delta(func_decl* p_orig, int level);
-    void     add_cover(unsigned level, expr* property);
+    void     add_cover(unsigned level, expr* property, bool bg = false);
     expr_ref get_reachable();
 
     std::ostream& display(std::ostream& strm) const;
@@ -484,7 +504,7 @@ public:
     bool propagate_to_next_level(unsigned level);
     void propagate_to_infinity(unsigned level);
     /// \brief  Add a lemma to the current context and all users
-    bool add_lemma(expr * lemma, unsigned lvl);
+    bool add_lemma(expr * e, unsigned lvl, bool bg);
     bool add_lemma(lemma* lem) {return m_frames.add_lemma(lem);}
     expr* get_reach_case_var (unsigned idx) const;
     bool has_rfs () const { return !m_reach_facts.empty () ;}
@@ -527,7 +547,7 @@ public:
     bool check_inductive(unsigned level, expr_ref_vector& state,
                          unsigned& assumes_level, unsigned weakness = UINT_MAX);
 
-    expr_ref get_formulas(unsigned level) const;
+    expr_ref get_formulas(unsigned level, bool bg = false) const;
 
     void simplify_formulas();
 
@@ -958,6 +978,7 @@ class context {
     bool                 m_simplify_formulas_pre;
     bool                 m_simplify_formulas_post;
     bool                 m_pdr_bfs;
+    bool                 m_use_bg_invs;
     unsigned             m_push_pob_max_depth;
     unsigned             m_max_level;
     unsigned             m_restart_initial_threshold;
@@ -992,7 +1013,8 @@ class context {
 
     // Generate inductive property
     void get_level_property(unsigned lvl, expr_ref_vector& res,
-                            vector<relation_info> & rs) const;
+                            vector<relation_info> & rs,
+                            bool with_bg = false) const;
 
 
     // Initialization
@@ -1027,18 +1049,20 @@ public:
 
 
     const fp_params &get_params() const { return m_params; }
-    bool use_native_mbp () {return m_use_native_mbp;}
-    bool use_ground_pob () {return m_ground_pob;}
-    bool use_instantiate () {return m_instantiate;}
-    bool weak_abs() {return m_weak_abs;}
-    bool use_qlemmas () {return m_use_qlemmas;}
-    bool use_euf_gen() {return m_use_euf_gen;}
-    bool simplify_pob() {return m_simplify_pob;}
-    bool use_ctp() {return m_use_ctp;}
-    bool use_inc_clause() {return m_use_inc_clause;}
-    unsigned blast_term_ite_inflation() {return m_blast_term_ite_inflation;}
-    bool elim_aux() {return m_elim_aux;}
-    bool reach_dnf() {return m_reach_dnf;}
+    bool use_eq_prop() const {return m_use_eq_prop;}
+    bool use_native_mbp() const {return m_use_native_mbp;}
+    bool use_ground_pob() const {return m_ground_pob;}
+    bool use_instantiate() const {return m_instantiate;}
+    bool weak_abs() const {return m_weak_abs;}
+    bool use_qlemmas() const {return m_use_qlemmas;}
+    bool use_euf_gen() const {return m_use_euf_gen;}
+    bool simplify_pob() const {return m_simplify_pob;}
+    bool use_ctp() const {return m_use_ctp;}
+    bool use_inc_clause() const {return m_use_inc_clause;}
+    unsigned blast_term_ite_inflation() const {return m_blast_term_ite_inflation;}
+    bool elim_aux() const {return m_elim_aux;}
+    bool reach_dnf() const {return m_reach_dnf;}
+    bool use_bg_invs() const {return m_use_bg_invs;}
 
     ast_manager&      get_ast_manager() const {return m;}
     manager&          get_manager() {return m_pm;}
@@ -1081,7 +1105,7 @@ public:
     unsigned get_num_levels(func_decl* p);
 
     expr_ref get_cover_delta(int level, func_decl* p_orig, func_decl* p);
-    void add_cover(int level, func_decl* pred, expr* property);
+    void add_cover(int level, func_decl* pred, expr* property, bool bg = false);
     expr_ref get_reachable (func_decl* p);
     void add_invariant (func_decl *pred, expr* property);
     model_ref get_model();
diff --git a/src/muz/spacer/spacer_prop_solver.cpp b/src/muz/spacer/spacer_prop_solver.cpp
index 004ea6754..4899ad692 100644
--- a/src/muz/spacer/spacer_prop_solver.cpp
+++ b/src/muz/spacer/spacer_prop_solver.cpp
@@ -94,6 +94,7 @@ void prop_solver::add_level()
 
 void prop_solver::ensure_level(unsigned lvl)
 {
+    if (is_infty_level(lvl)) return;
     while (lvl >= level_cnt()) {
         add_level();
     }
diff --git a/src/muz/spacer/spacer_util.h b/src/muz/spacer/spacer_util.h
index 8da574d0e..0328d8640 100644
--- a/src/muz/spacer/spacer_util.h
+++ b/src/muz/spacer/spacer_util.h
@@ -48,7 +48,8 @@ namespace spacer {
     }
 
     inline bool is_infty_level(unsigned lvl) {
-        return lvl == infty_level ();
+        // XXX: level is 16 bits in class pob
+        return lvl >= 65535;
     }
 
     inline unsigned next_level(unsigned lvl) {
diff --git a/src/muz/transforms/CMakeLists.txt b/src/muz/transforms/CMakeLists.txt
index e92aa1c2f..62272450c 100644
--- a/src/muz/transforms/CMakeLists.txt
+++ b/src/muz/transforms/CMakeLists.txt
@@ -25,6 +25,7 @@ z3_add_component(transforms
     dl_mk_array_eq_rewrite.cpp
     dl_mk_array_instantiation.cpp
     dl_mk_elim_term_ite.cpp
+    dl_mk_synchronize.cpp
   COMPONENT_DEPENDENCIES
     dataflow
     hilbert
diff --git a/src/muz/transforms/dl_mk_synchronize.cpp b/src/muz/transforms/dl_mk_synchronize.cpp
new file mode 100644
index 000000000..348c9b5de
--- /dev/null
+++ b/src/muz/transforms/dl_mk_synchronize.cpp
@@ -0,0 +1,376 @@
+/*++
+Copyright (c) 2017-2018 Saint-Petersburg State University
+
+Module Name:
+
+    dl_mk_synchronize.h
+
+Abstract:
+
+    Rule transformer that attempts to merge recursive iterations
+    relaxing the shape of the inductive invariant.
+
+Author:
+
+    Dmitry Mordvinov (dvvrd) 2017-05-24
+    Lidiia Chernigovskaia (LChernigovskaya) 2017-10-20
+
+Revision History:
+
+--*/
+#include "muz/transforms/dl_mk_synchronize.h"
+#include <algorithm>
+
+namespace datalog {
+
+    typedef mk_synchronize::item_set_vector item_set_vector;
+
+    mk_synchronize::mk_synchronize(context& ctx, unsigned priority):
+        rule_transformer::plugin(priority, false),
+        m_ctx(ctx),
+        m(ctx.get_manager()),
+        rm(ctx.get_rule_manager())
+    {}
+
+    bool mk_synchronize::is_recursive(rule &r, func_decl &decl) const {
+        func_decl *hdecl = r.get_head()->get_decl();
+        // AG: shouldn't decl appear in the body?
+        if (hdecl == &decl)  return true;
+        auto & strata = m_stratifier->get_strats();
+        unsigned num_of_stratum = m_stratifier->get_predicate_strat(hdecl);
+        return strata[num_of_stratum]->contains(&decl);
+    }
+
+    bool mk_synchronize::has_recursive_premise(app * app) const {
+        func_decl* app_decl = app->get_decl();
+        if (m_deps->get_deps(app_decl).contains(app_decl)) {
+            return true;
+        }
+        rule_stratifier::comp_vector const & strata = m_stratifier->get_strats();
+        unsigned num_of_stratum = m_stratifier->get_predicate_strat(app_decl);
+        return strata[num_of_stratum]->size() > 1;
+    }
+
+    item_set_vector mk_synchronize::add_merged_decls(ptr_vector<app> & apps) {
+        unsigned sz = apps.size();
+        item_set_vector merged_decls;
+        merged_decls.resize(sz);
+        auto & strata = m_stratifier->get_strats();
+        for (unsigned j = 0; j < sz; ++j) {
+            unsigned nos;
+            nos = m_stratifier->get_predicate_strat(apps[j]->get_decl());
+            merged_decls[j] = strata[nos];
+        }
+        return merged_decls;
+    }
+
+    void mk_synchronize::add_new_rel_symbols(unsigned idx,
+                                             item_set_vector const & decls,
+                                             ptr_vector<func_decl> & decls_buf,
+                                             bool & was_added) {
+        if (idx >= decls.size()) {
+            string_buffer<> buffer;
+            ptr_vector<sort> domain;
+            for (auto &d : decls_buf) {
+                buffer << d->get_name() << "!!";
+                domain.append(d->get_arity(), d->get_domain());
+            }
+
+            symbol new_name = symbol(buffer.c_str());
+
+            if (!m_cache.contains(new_name)) {
+                was_added = true;
+                func_decl* orig = decls_buf[0];
+                func_decl* product_pred = m_ctx.mk_fresh_head_predicate(new_name,
+                    symbol::null, domain.size(), domain.c_ptr(), orig);
+                m_cache.insert(new_name, product_pred);
+            }
+            return;
+        }
+
+        // -- compute Cartesian product of decls, and create a new
+        // -- predicate for each element of the product
+        for (auto &p : *decls[idx]) {
+            decls_buf[idx] = p;
+            add_new_rel_symbols(idx + 1, decls, decls_buf, was_added);
+        }
+    }
+
+    void mk_synchronize::replace_applications(rule & r, rule_set & rules,
+                                              ptr_vector<app> & apps) {
+        app_ref replacing = product_application(apps);
+
+        ptr_vector<app> new_tail;
+        svector<bool> new_tail_neg;
+        unsigned n = r.get_tail_size() - apps.size() + 1;
+        unsigned tail_idx = 0;
+        new_tail.resize(n);
+        new_tail_neg.resize(n);
+        new_tail[0] = replacing;
+        new_tail_neg[0] = false;
+
+        for (unsigned i = 0; i < r.get_positive_tail_size(); ++i) {
+            app* tail = r.get_tail(i);
+            if (!apps.contains(tail)) {
+                ++tail_idx;
+                new_tail[tail_idx] = tail;
+                new_tail_neg[tail_idx] = false;
+            }
+        }
+        for (unsigned i = r.get_positive_tail_size(); i < r.get_uninterpreted_tail_size(); ++i) {
+            ++tail_idx;
+            new_tail[tail_idx] = r.get_tail(i);
+            new_tail_neg[tail_idx] = true;
+        }
+        for (unsigned i = r.get_uninterpreted_tail_size(); i < r.get_tail_size(); ++i) {
+            ++tail_idx;
+            new_tail[tail_idx] = r.get_tail(i);
+            new_tail_neg[tail_idx] = false;
+        }
+
+        rule_ref new_rule(rm);
+        new_rule = rm.mk(r.get_head(), tail_idx + 1,
+            new_tail.c_ptr(), new_tail_neg.c_ptr(), symbol::null, false);
+        rules.replace_rule(&r, new_rule.get());
+    }
+
+    rule_ref mk_synchronize::rename_bound_vars_in_rule(rule * r,
+                                                       unsigned & var_idx) {
+        // AG: shift all variables in a rule so that lowest var index is var_idx?
+        // AG: update var_idx in the process?
+        ptr_vector<sort> sorts;
+        r->get_vars(m, sorts);
+        expr_ref_vector revsub(m);
+        revsub.resize(sorts.size());
+        for (unsigned i = 0; i < sorts.size(); ++i) {
+            if (sorts[i]) {
+                revsub[i] = m.mk_var(var_idx++, sorts[i]);
+            }
+        }
+
+        rule_ref new_rule(rm);
+        new_rule = rm.mk(r);
+        rm.substitute(new_rule, revsub.size(), revsub.c_ptr());
+        return new_rule;
+    }
+
+    vector<rule_ref_vector> mk_synchronize::rename_bound_vars(item_set_vector const & heads,
+                                                              rule_set & rules) {
+        // AG: is every item_set in heads corresponds to rules that are merged?
+        // AG: why are bound variables renamed in the first place?
+        // AG: the data structure seems too complex
+        vector<rule_ref_vector> result;
+        unsigned var_idx = 0;
+        for (auto item : heads) {
+            rule_ref_vector dst_vector(rm);
+            for (auto *head : *item) {
+                for (auto *r : rules.get_predicate_rules(head)) {
+                    rule_ref new_rule = rename_bound_vars_in_rule(r, var_idx);
+                    dst_vector.push_back(new_rule.get());
+                }
+            }
+            result.push_back(dst_vector);
+        }
+        return result;
+    }
+
+    void mk_synchronize::add_rec_tail(vector< ptr_vector<app> > & recursive_calls,
+                                      app_ref_vector & new_tail,
+                                      svector<bool> & new_tail_neg,
+                                      unsigned & tail_idx) {
+        unsigned max_sz = 0;
+        for (auto &rc : recursive_calls)
+            max_sz= std::max(rc.size(), max_sz);
+
+        unsigned n = recursive_calls.size();
+        ptr_vector<app> merged_recursive_calls;
+
+        for (unsigned j = 0; j < max_sz; ++j) {
+            merged_recursive_calls.reset();
+            merged_recursive_calls.resize(n);
+            for (unsigned i = 0; i < n; ++i) {
+                unsigned sz = recursive_calls[i].size();
+                merged_recursive_calls[i] =
+                    j < sz ? recursive_calls[i][j] : recursive_calls[i][sz - 1];
+            }
+            ++tail_idx;
+            new_tail[tail_idx] = product_application(merged_recursive_calls);
+            new_tail_neg[tail_idx] = false;
+        }
+    }
+
+    void mk_synchronize::add_non_rec_tail(rule & r, app_ref_vector & new_tail,
+                                          svector<bool> & new_tail_neg,
+                                          unsigned & tail_idx) {
+        for (unsigned i = 0, sz = r.get_positive_tail_size(); i < sz; ++i) {
+            app* tail = r.get_tail(i);
+            if (!is_recursive(r, *tail)) {
+                ++tail_idx;
+                new_tail[tail_idx] = tail;
+                new_tail_neg[tail_idx] = false;
+            }
+        }
+        for (unsigned i = r.get_positive_tail_size(),
+                 sz = r.get_uninterpreted_tail_size() ; i < sz; ++i) {
+            ++tail_idx;
+            new_tail[tail_idx] = r.get_tail(i);
+            new_tail_neg[tail_idx] = true;
+        }
+        for (unsigned i = r.get_uninterpreted_tail_size(),
+                 sz = r.get_tail_size(); i < sz; ++i) {
+            ++tail_idx;
+            new_tail[tail_idx] = r.get_tail(i);
+            new_tail_neg[tail_idx] = r.is_neg_tail(i);
+        }
+    }
+
+    app_ref mk_synchronize::product_application(ptr_vector<app> const &apps) {
+        unsigned args_num = 0;
+        string_buffer<> buffer;
+
+        // AG: factor out into mk_name
+        for (auto *app : apps) {
+            buffer << app->get_decl()->get_name() << "!!";
+            args_num += app->get_num_args();
+        }
+
+        symbol name = symbol(buffer.c_str());
+        SASSERT(m_cache.contains(name));
+        func_decl * pred = m_cache[name];
+
+        ptr_vector<expr> args;
+        args.resize(args_num);
+        unsigned idx = 0;
+        for (auto *a : apps) {
+            for (unsigned i = 0, sz = a->get_num_args(); i < sz; ++i, ++idx)
+                args[idx] = a->get_arg(i);
+        }
+
+        return app_ref(m.mk_app(pred, args_num, args.c_ptr()), m);
+    }
+
+    rule_ref mk_synchronize::product_rule(rule_ref_vector const & rules) {
+        unsigned n = rules.size();
+
+        string_buffer<> buffer;
+        bool first_rule = true;
+        for (auto it = rules.begin(); it != rules.end(); ++it, first_rule = false) {
+            if (!first_rule) {
+                buffer << "+";
+            }
+            buffer << (*it)->name();
+        }
+
+        ptr_vector<app> heads;
+        heads.resize(n);
+        for (unsigned i = 0; i < n; ++i) {
+            heads[i] = rules[i]->get_head();
+        }
+        app_ref product_head = product_application(heads);
+        unsigned product_tail_length = 0;
+        bool has_recursion = false;
+        vector< ptr_vector<app> > recursive_calls;
+        recursive_calls.resize(n);
+        for (unsigned i = 0; i < n; ++i) {
+            rule& rule = *rules[i];
+            product_tail_length += rule.get_tail_size();
+            for (unsigned j = 0; j < rule.get_positive_tail_size(); ++j) {
+                app* tail = rule.get_tail(j);
+                if (is_recursive(rule, *tail)) {
+                    has_recursion = true;
+                    recursive_calls[i].push_back(tail);
+                }
+            }
+            if (recursive_calls[i].empty()) {
+                recursive_calls[i].push_back(rule.get_head());
+            }
+        }
+
+        app_ref_vector new_tail(m);
+        svector<bool> new_tail_neg;
+        new_tail.resize(product_tail_length);
+        new_tail_neg.resize(product_tail_length);
+        unsigned tail_idx = -1;
+        if (has_recursion) {
+            add_rec_tail(recursive_calls, new_tail, new_tail_neg, tail_idx);
+        }
+
+        for (rule_vector::const_iterator it = rules.begin(); it != rules.end(); ++it) {
+            rule& rule = **it;
+            add_non_rec_tail(rule, new_tail, new_tail_neg, tail_idx);
+        }
+
+        rule_ref new_rule(rm);
+        new_rule = rm.mk(product_head, tail_idx + 1,
+            new_tail.c_ptr(), new_tail_neg.c_ptr(), symbol(buffer.c_str()), false);
+        rm.fix_unbound_vars(new_rule, false);
+        return new_rule;
+    }
+
+    void mk_synchronize::merge_rules(unsigned idx, rule_ref_vector & buf,
+                                     vector<rule_ref_vector> const & merged_rules,
+                                     rule_set & all_rules) {
+        if (idx >= merged_rules.size()) {
+            rule_ref product = product_rule(buf);
+            all_rules.add_rule(product.get());
+            return;
+        }
+
+        for (auto *r : merged_rules[idx]) {
+            buf[idx] = r;
+            merge_rules(idx + 1, buf, merged_rules, all_rules);
+        }
+    }
+
+    void mk_synchronize::merge_applications(rule & r, rule_set & rules) {
+        ptr_vector<app> non_recursive_preds;
+        obj_hashtable<app> apps;
+        for (unsigned i = 0; i < r.get_positive_tail_size(); ++i) {
+            app* t = r.get_tail(i);
+            if (!is_recursive(r, *t) && has_recursive_premise(t)) {
+                apps.insert(t);
+            }
+        }
+        if (apps.size() < 2) return;
+        for (auto *a : apps) non_recursive_preds.push_back(a);
+
+        item_set_vector merged_decls = add_merged_decls(non_recursive_preds);
+
+        unsigned n = non_recursive_preds.size();
+        ptr_vector<func_decl> decls_buf;
+        decls_buf.resize(n);
+        bool was_added = false;
+        add_new_rel_symbols(0, merged_decls, decls_buf, was_added);
+        if (was_added){
+            rule_ref_vector rules_buf(rm);
+            rules_buf.resize(n);
+            vector<rule_ref_vector> renamed_rules = rename_bound_vars(merged_decls, rules);
+            merge_rules(0, rules_buf, renamed_rules, rules);
+        }
+
+        replace_applications(r, rules, non_recursive_preds);
+        m_deps->populate(rules);
+        m_stratifier = alloc(rule_stratifier, *m_deps);
+    }
+
+    rule_set * mk_synchronize::operator()(rule_set const & source) {
+        rule_set* rules = alloc(rule_set, m_ctx);
+        rules->inherit_predicates(source);
+
+        for (auto *r : source) { rules->add_rule(r); }
+
+        m_deps = alloc(rule_dependencies, m_ctx);
+        m_deps->populate(*rules);
+        m_stratifier = alloc(rule_stratifier, *m_deps);
+
+        unsigned current_rule = 0;
+        while (current_rule < rules->get_num_rules()) {
+            rule *r = rules->get_rule(current_rule);
+            merge_applications(*r, *rules);
+            ++current_rule;
+        }
+
+        return rules;
+    }
+
+};
diff --git a/src/muz/transforms/dl_mk_synchronize.h b/src/muz/transforms/dl_mk_synchronize.h
new file mode 100644
index 000000000..6f4b3ca40
--- /dev/null
+++ b/src/muz/transforms/dl_mk_synchronize.h
@@ -0,0 +1,134 @@
+/*++
+Copyright (c) 2017-2018 Saint-Petersburg State University
+
+Module Name:
+
+    dl_mk_synchronize.h
+
+Abstract:
+
+    Rule transformer that attempts to merge recursive iterations
+    relaxing the shape of the inductive invariant.
+
+Example:
+
+    Q(z)  :- A(x), B(y), phi1(x,y,z).
+    A(x)  :- A(x'), phi2(x,x').
+    A(x)  :- phi3(x).
+    B(y)  :- C(y'), phi4(y,y').
+    C(y)  :- B(y'), phi5(y,y').
+    B(y)  :- phi6(y).
+
+    Transformed clauses:
+
+    Q(z)    :- AB(x,y), phi1(x,y,z).
+    AB(x,y) :- AC(x',y'), phi2(x,x'), phi4(y,y').
+    AC(x,y) :- AB(x',y'), phi2(x,x'), phi5(y,y').
+    AB(x,y) :- AC(x, y'), phi3(x), phi4(y,y').
+    AC(x,y) :- AB(x, y'), phi3(x), phi5(y,y').
+    AB(x,y) :- AB(x',y), phi2(x,x'), phi6(y).
+    AB(x,y) :- phi3(x), phi6(y).
+
+Author:
+
+    Dmitry Mordvinov (dvvrd) 2017-05-24
+    Lidiia Chernigovskaia (LChernigovskaya) 2017-10-20
+
+Revision History:
+
+--*/
+#ifndef DL_MK_SYNCHRONIZE_H_
+#define DL_MK_SYNCHRONIZE_H_
+
+#include"muz/base/dl_context.h"
+#include"muz/base/dl_rule_set.h"
+#include"util/uint_set.h"
+#include"muz/base/dl_rule_transformer.h"
+#include"muz/transforms/dl_mk_rule_inliner.h"
+
+namespace datalog {
+
+    /**
+       \brief Implements a synchronous product transformation.
+    */
+    class mk_synchronize : public rule_transformer::plugin {
+    public:
+        typedef ptr_vector<rule_stratifier::item_set> item_set_vector;
+    private:
+        context&        m_ctx;
+        ast_manager&    m;
+        rule_manager&   rm;
+
+        scoped_ptr<rule_dependencies> m_deps;
+        scoped_ptr<rule_stratifier> m_stratifier;
+
+        // symbol table that maps new predicate names to corresponding
+        // func_decl
+        map<symbol, func_decl*, symbol_hash_proc, symbol_eq_proc> m_cache;
+
+        /// returns true if decl is recursive in the given rule
+        /// requires that decl appears in the tail of r
+        bool is_recursive(rule &r, func_decl &decl) const;
+        bool is_recursive(rule &r, expr &e) const {
+            SASSERT(is_app(&e));
+            return is_app(&e) && is_recursive(r, *to_app(&e)->get_decl());
+        }
+
+        /// returns true if the top-level predicate of app is recursive
+        bool has_recursive_premise(app * app) const;
+
+        item_set_vector add_merged_decls(ptr_vector<app> & apps);
+
+        /**
+            Compute Cartesian product of decls and create a new
+            predicate for each element. For example, if decls is
+
+            ( (a, b), (c, d) ) )
+
+            create new predicates: a!!c, a!!d, b!!c, and b!!d
+        */
+        void add_new_rel_symbols(unsigned idx, item_set_vector const & decls,
+                                 ptr_vector<func_decl> & buf, bool & was_added);
+
+        /**
+           Convert vector of predicate apps into a single app. For example,
+           (Foo a) (Bar b) becomes (Foo!!Bar a b)
+         */
+        app_ref product_application(ptr_vector<app> const & apps);
+
+        /**
+            Replace a given rule by a rule in which conjunction of
+            predicates is replaced by a single product predicate
+         */
+        void replace_applications(rule & r, rule_set & rules,
+                                  ptr_vector<app> & apps);
+
+        rule_ref rename_bound_vars_in_rule(rule * r, unsigned & var_idx);
+        vector<rule_ref_vector> rename_bound_vars(item_set_vector const & heads,
+                                                  rule_set & rules);
+
+        void add_rec_tail(vector< ptr_vector<app> > & recursive_calls,
+                          app_ref_vector & new_tail,
+                          svector<bool> & new_tail_neg, unsigned & tail_idx);
+        void add_non_rec_tail(rule & r, app_ref_vector & new_tail,
+                              svector<bool> & new_tail_neg,
+                              unsigned & tail_idx);
+
+        rule_ref product_rule(rule_ref_vector const & rules);
+
+        void merge_rules(unsigned idx, rule_ref_vector & buf,
+            vector<rule_ref_vector> const & merged_rules, rule_set & all_rules);
+        void merge_applications(rule & r, rule_set & rules);
+
+    public:
+        /**
+           \brief Create synchronous product transformer.
+         */
+        mk_synchronize(context & ctx, unsigned priority = 22500);
+
+        rule_set * operator()(rule_set const & source);
+    };
+
+};
+
+#endif /* DL_MK_SYNCHRONIZE_H_ */