diff --git a/examples/ml/ml_example.ml b/examples/ml/ml_example.ml
index eb64f8ee8..5b4e6e9ed 100644
--- a/examples/ml/ml_example.ml
+++ b/examples/ml/ml_example.ml
@@ -65,8 +65,7 @@ let  model_converter_test ( ctx : context ) =
 	| None -> raise (TestFailedException "")
 	| Some (m) -> 
 	  Printf.printf "Solver says: %s\n" (string_of_status q) ;
-	  Printf.printf "Model: \n%s\n" (Model.to_string m) ;
-	  Printf.printf "Converted Model: \n%s\n" (Model.to_string (convert_model ar 0 m))
+	  Printf.printf "Model: \n%s\n" (Model.to_string m) 
   )
 
 (**
@@ -330,12 +329,14 @@ let _ =
 	let ss = (Symbol.mk_string ctx "mySymbol") in
 	let bs = (Boolean.mk_sort ctx) in
 	let ints = (Integer.mk_sort ctx) in
-	let rs = (Real.mk_sort ctx) in
+        let rs = (Real.mk_sort ctx) in
+	let v = (Arithmetic.Integer.mk_numeral_i ctx 8000000000) in
 	Printf.printf "int symbol: %s\n" (Symbol.to_string is);
 	Printf.printf "string symbol: %s\n" (Symbol.to_string ss);
 	Printf.printf "bool sort: %s\n" (Sort.to_string bs);
 	Printf.printf "int sort: %s\n" (Sort.to_string ints);
 	Printf.printf "real sort: %s\n" (Sort.to_string rs);
+	Printf.printf "integer: %s\n" (Expr.to_string v);
 	basic_tests ctx ;
 	quantifier_example1 ctx ;
 	fpa_example ctx ;
diff --git a/src/api/ml/z3.ml b/src/api/ml/z3.ml
index a676f8c43..25b437bc4 100644
--- a/src/api/ml/z3.ml
+++ b/src/api/ml/z3.ml
@@ -43,6 +43,14 @@ let mk_list f n =
   in
   mk_list' 0 []
 
+let check_int32 v = v = Int32.to_int (Int32.of_int v)
+
+let mk_int_expr ctx v ty = 
+   if not (check_int32 v) then
+      Z3native.mk_numeral ctx (string_of_int v) ty
+   else
+      Z3native.mk_int ctx v ty
+    
 let mk_context (settings:(string * string) list) =
   let cfg = Z3native.mk_config () in
   let f e = Z3native.set_param_value cfg (fst e) (snd e) in
@@ -531,7 +539,7 @@ end = struct
   let mk_fresh_const (ctx:context) (prefix:string) (range:Sort.sort) = Z3native.mk_fresh_const ctx prefix range
   let mk_app (ctx:context) (f:FuncDecl.func_decl) (args:expr list) = expr_of_func_app ctx f args
   let mk_numeral_string (ctx:context) (v:string) (ty:Sort.sort) = Z3native.mk_numeral ctx v ty
-  let mk_numeral_int (ctx:context) (v:int) (ty:Sort.sort) = Z3native.mk_int ctx v ty
+  let mk_numeral_int (ctx:context) (v:int) (ty:Sort.sort) = mk_int_expr ctx v ty
   let equal (a:expr) (b:expr) = AST.equal a b
   let compare (a:expr) (b:expr) = AST.compare a b
 end
@@ -1036,7 +1044,7 @@ struct
     let mk_mod = Z3native.mk_mod
     let mk_rem = Z3native.mk_rem
     let mk_numeral_s (ctx:context) (v:string) = Z3native.mk_numeral ctx v (mk_sort ctx)
-    let mk_numeral_i (ctx:context) (v:int) = Z3native.mk_int ctx v (mk_sort ctx)
+    let mk_numeral_i (ctx:context) (v:int) = mk_int_expr ctx v (mk_sort ctx)
     let mk_int2real = Z3native.mk_int2real
     let mk_int2bv = Z3native.mk_int2bv
   end
@@ -1061,11 +1069,13 @@ struct
     let mk_numeral_nd (ctx:context) (num:int) (den:int) =
       if den = 0 then
         raise (Error "Denominator is zero")
+      else if not (check_int32 num) || not (check_int32 den) then
+        raise (Error "numerals don't fit in 32 bits")
       else
         Z3native.mk_real ctx num den
 
     let mk_numeral_s (ctx:context) (v:string) = Z3native.mk_numeral ctx v (mk_sort ctx)
-    let mk_numeral_i (ctx:context) (v:int) = Z3native.mk_int ctx v (mk_sort ctx)
+    let mk_numeral_i (ctx:context) (v:int) = mk_int_expr ctx v (mk_sort ctx)
     let mk_is_integer = Z3native.mk_is_int
     let mk_real2int = Z3native.mk_real2int
 
@@ -1155,11 +1165,6 @@ struct
   let is_bv_xor3 (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) = OP_XOR3)
   let get_size (x:Sort.sort) = Z3native.get_bv_sort_size (Sort.gc x) x
 
-  let get_int (x:expr) =
-    match Z3native.get_numeral_int (Expr.gc x) x with
-    | true, v -> v
-    | false, _ -> raise (Error "Conversion failed.")
-
   let numeral_to_string (x:expr) = Z3native.get_numeral_string (Expr.gc x) x
   let mk_const (ctx:context) (name:Symbol.symbol) (size:int) =
     Expr.mk_const ctx name (mk_sort ctx size)
diff --git a/src/api/ml/z3.mli b/src/api/ml/z3.mli
index 9b424b508..f67966a0f 100644
--- a/src/api/ml/z3.mli
+++ b/src/api/ml/z3.mli
@@ -1152,9 +1152,6 @@ sig
     (** Create a new integer sort. *)
     val mk_sort : context -> Sort.sort
 
-    (** Retrieve the int value. *)
-    val get_int : Expr.expr -> int
-
     (** Get a big_int from an integer numeral *)
     val get_big_int : Expr.expr -> Big_int.big_int
 
@@ -1543,9 +1540,6 @@ sig
   (** The size of a bit-vector sort. *)
   val get_size : Sort.sort -> int
 
-  (**  Retrieve the int value. *)
-  val get_int : Expr.expr -> int
-
   (** Returns a string representation of a numeral. *)
   val numeral_to_string : Expr.expr -> string
 
diff --git a/src/ast/arith_decl_plugin.cpp b/src/ast/arith_decl_plugin.cpp
index db3604a99..cdf18875c 100644
--- a/src/ast/arith_decl_plugin.cpp
+++ b/src/ast/arith_decl_plugin.cpp
@@ -21,6 +21,7 @@ Revision History:
 #include "math/polynomial/algebraic_numbers.h"
 #include "util/id_gen.h"
 #include "ast/ast_smt2_pp.h"
+#include "util/gparams.h"
 
 struct arith_decl_plugin::algebraic_numbers_wrapper {
     unsynch_mpq_manager           m_qmanager;
@@ -487,7 +488,7 @@ func_decl * arith_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters
         if (arity != 1 || domain[0] != m_int_decl || num_parameters != 1 || !parameters[0].is_int()) {
             m_manager->raise_exception("invalid divides application. Expects integer parameter and one argument of sort integer");
         }
-        return m_manager->mk_func_decl(symbol("divides"), 1, &m_int_decl, m_manager->mk_bool_sort(), 
+        return m_manager->mk_func_decl(symbol("divisible"), 1, &m_int_decl, m_manager->mk_bool_sort(), 
                                        func_decl_info(m_family_id, k, num_parameters, parameters));
     }
 
@@ -512,7 +513,7 @@ func_decl * arith_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters
         if (num_args != 1 || m_manager->get_sort(args[0]) != m_int_decl || num_parameters != 1 || !parameters[0].is_int()) {
             m_manager->raise_exception("invalid divides application. Expects integer parameter and one argument of sort integer");
         }
-        return m_manager->mk_func_decl(symbol("divides"), 1, &m_int_decl, m_manager->mk_bool_sort(), 
+        return m_manager->mk_func_decl(symbol("divisible"), 1, &m_int_decl, m_manager->mk_bool_sort(), 
                                        func_decl_info(m_family_id, k, num_parameters, parameters));
     }
     if (m_manager->int_real_coercions() && use_coercion(k)) {
@@ -549,8 +550,9 @@ void arith_decl_plugin::get_op_names(svector<builtin_name>& op_names, symbol con
     op_names.push_back(builtin_name("*",OP_MUL));
     op_names.push_back(builtin_name("/",OP_DIV));
     op_names.push_back(builtin_name("div",OP_IDIV));
-    // clashes with user-defined functions
-    // op_names.push_back(builtin_name("divides",OP_IDIVIDES));
+    if (gparams::get_value("smtlib2_compliant") == "true") {
+        op_names.push_back(builtin_name("divisible",OP_IDIVIDES));
+    }
     op_names.push_back(builtin_name("rem",OP_REM));
     op_names.push_back(builtin_name("mod",OP_MOD));
     op_names.push_back(builtin_name("to_real",OP_TO_REAL));
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_ */
diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp
index e5c0bcddb..5d4eb3fc5 100644
--- a/src/opt/opt_context.cpp
+++ b/src/opt/opt_context.cpp
@@ -351,7 +351,7 @@ namespace opt {
     void context::get_model_core(model_ref& mdl) {
         mdl = m_model;
         fix_model(mdl);
-        mdl->set_model_completion(true);
+        if (mdl) mdl->set_model_completion(true);
         TRACE("opt", tout << *mdl;);
     }
 
diff --git a/src/sat/ba_solver.cpp b/src/sat/ba_solver.cpp
index 4226b9791..de6635d09 100644
--- a/src/sat/ba_solver.cpp
+++ b/src/sat/ba_solver.cpp
@@ -1551,10 +1551,10 @@ namespace sat {
         if (k == 1 && lit == null_literal) {
             literal_vector _lits(lits);
             s().mk_clause(_lits.size(), _lits.c_ptr(), learned);
-            return 0;
+            return nullptr;
         }
         if (!learned && clausify(lit, lits.size(), lits.c_ptr(), k)) {
-            return 0;
+            return nullptr;
         }
         void * mem = m_allocator.allocate(card::get_obj_size(lits.size()));
         card* c = new (mem) card(next_id(), lit, lits, k);
@@ -1615,7 +1615,7 @@ namespace sat {
         bool units = true;
         for (wliteral wl : wlits) units &= wl.first == 1;
         if (k == 0 && lit == null_literal) {
-            return 0;
+            return nullptr;
         }
         if (units || k == 1) {
             literal_vector lits;
@@ -3405,7 +3405,7 @@ namespace sat {
             return;
         }
         for (wliteral l : p1) {
-            SASSERT(m_weights[l.second.index()] == 0);
+            SASSERT(m_weights.size() <= l.second.index() || m_weights[l.second.index()] == 0);
             m_weights.setx(l.second.index(), l.first, 0);
             mark_visited(l.second);  
         }
@@ -3837,8 +3837,8 @@ namespace sat {
         reset_active_var_set();
         m_wlits.reset();
         uint64_t sum = 0;
-        if (m_bound == 1) return 0;
-        if (m_overflow) return 0;
+        if (m_bound == 1) return nullptr;
+        if (m_overflow) return nullptr;
         
         for (bool_var v : m_active_vars) {
             int coeff = get_int_coeff(v);
@@ -3850,7 +3850,7 @@ namespace sat {
         }
 
         if (m_overflow || sum >= UINT_MAX/2) {
-            return 0;
+            return nullptr;
         }
         else {
             return add_pb_ge(null_literal, m_wlits, m_bound, true);
@@ -3905,7 +3905,7 @@ namespace sat {
             ++k;
         }
         if (k == 1) {
-            return 0;
+            return nullptr;
         }
         while (!m_wlits.empty()) {
             wliteral wl = m_wlits.back();
@@ -3928,7 +3928,7 @@ namespace sat {
                 ++num_max_level;
             }
         }
-        if (m_overflow) return 0;
+        if (m_overflow) return nullptr;
 
         if (slack >= k) {
 #if 0
@@ -3937,7 +3937,7 @@ namespace sat {
             std::cout << "not asserting\n";
             display(std::cout, m_A, true);
 #endif
-            return 0;
+            return nullptr;
         }
 
         // produce asserting cardinality constraint
diff --git a/src/util/mpz.h b/src/util/mpz.h
index 65f89f078..2df03666f 100644
--- a/src/util/mpz.h
+++ b/src/util/mpz.h
@@ -152,7 +152,7 @@ class mpz_manager {
     
     // make sure that n is a big number and has capacity equal to at least c.
     void allocate_if_needed(mpz & n, unsigned c) {
-        c = std::max(c, m_init_cell_capacity);
+        if (m_init_cell_capacity > c) c = m_init_cell_capacity;
         if (n.m_ptr == nullptr || capacity(n) < c) {
             deallocate(n);
             n.m_val             = 1;
diff --git a/src/util/union_find.h b/src/util/union_find.h
index 9dd0b6fbd..f8ae0402f 100644
--- a/src/util/union_find.h
+++ b/src/util/union_find.h
@@ -122,8 +122,10 @@ public:
         TRACE("union_find", tout << "merging " << r1 << " " << r2 << "\n";);
         if (r1 == r2)
             return;
-        if (m_size[r1] > m_size[r2])
+        if (m_size[r1] > m_size[r2]) {
             std::swap(r1, r2);
+            std::swap(v1, v2);
+        }
         m_ctx.merge_eh(r2, r1, v2, v1);
         m_find[r1] = r2;
         m_size[r2] += m_size[r1];