diff --git a/src/muz_qe/dl_compiler.cpp b/src/muz_qe/dl_compiler.cpp
index e4528426a..57d9880c0 100644
--- a/src/muz_qe/dl_compiler.cpp
+++ b/src/muz_qe/dl_compiler.cpp
@@ -832,19 +832,19 @@ namespace datalog {
         typedef rule_dependencies::item_set item_set; //set of T
 
         rule_dependencies & m_deps;
-        rule_set const& m_rules;
-        context& m_context;
         item_set & m_removed;
         svector<T> m_stack;
+        ast_mark m_stack_content;
         ast_mark m_visited;
 
         void traverse(T v) {
-            SASSERT(!m_visited.is_marked(v));
-            if (m_removed.contains(v)) {
+            SASSERT(!m_stack_content.is_marked(v)); 
+            if(m_visited.is_marked(v) || m_removed.contains(v)) { 
                 return;
             }
 
             m_stack.push_back(v);
+            m_stack_content.mark(v, true); 
             m_visited.mark(v, true);
 
             const item_set & deps = m_deps.get_deps(v);
@@ -852,49 +852,22 @@ namespace datalog {
             item_set::iterator end = deps.end();
             for(; it!=end; ++it) {
                 T d = *it;
-                if (m_visited.is_marked(d)) {
+                if(m_stack_content.is_marked(d)) { 
                     //TODO: find the best vertex to remove in the cycle
-                    remove_from_stack();
-                    continue;
+                    m_removed.insert(v);
+                    break;
                 }
                 traverse(d);
             }
             SASSERT(m_stack.back()==v);
 
             m_stack.pop_back();
-            m_visited.mark(v, false);
-        }
-
-        void remove_from_stack() {
-            for (unsigned i = 0; i < m_stack.size(); ++i) {
-                func_decl* p = m_stack[i];
-                if (m_context.has_facts(p)) {
-                    m_removed.insert(p);
-                    return;
-                }
-
-                rule_vector const& rules = m_rules.get_predicate_rules(p);
-                unsigned stratum = m_rules.get_predicate_strat(p);
-                for (unsigned j = 0; j < rules.size(); ++j) {
-                    rule const& r = *rules[j];
-                    bool ok = true;
-                    for (unsigned k = 0; ok && k < r.get_uninterpreted_tail_size(); ++k) {
-                        ok = m_rules.get_predicate_strat(r.get_decl(k)) < stratum;
-                    }
-                    if (ok) {
-                        m_removed.insert(p);
-                        return;
-                    }
-                }
-            }
-
-            // nothing was found.
-            m_removed.insert(m_stack.back());
+            m_stack_content.mark(v, false); 
         }
 
     public:
-        cycle_breaker(rule_dependencies & deps, rule_set const& rules, context& ctx, item_set & removed) 
-            : m_deps(deps), m_rules(rules), m_context(ctx), m_removed(removed) { SASSERT(removed.empty()); }
+        cycle_breaker(rule_dependencies & deps, item_set & removed) 
+            : m_deps(deps), m_removed(removed) { SASSERT(removed.empty()); }
 
         void operator()() {
             rule_dependencies::iterator it = m_deps.begin();
@@ -916,7 +889,7 @@ namespace datalog {
 
         rule_dependencies deps(m_rule_set.get_dependencies());
         deps.restrict(preds);
-        cycle_breaker(deps, m_rule_set, m_context, global_deltas)();
+        cycle_breaker(deps, global_deltas)();
         VERIFY( deps.sort_deps(ordered_preds) );
 
         //the predicates that were removed to get acyclic induced subgraph are put last
@@ -1052,12 +1025,17 @@ namespace datalog {
         }
 
         func_decl_vector preds_vector;
-        func_decl_set global_deltas;
+        func_decl_set global_deltas_dummy;
 
-        detect_chains(head_preds, preds_vector, global_deltas);
+        detect_chains(head_preds, preds_vector, global_deltas_dummy);
 
+        /*
+          FIXME: right now we use all preds as global deltas for correctness purposes
         func_decl_set local_deltas(head_preds);
         set_difference(local_deltas, global_deltas);
+        */
+        func_decl_set local_deltas;
+        func_decl_set global_deltas(head_preds);
 
         pred2idx d_global_src;  //these deltas serve as sources of tuples for rule evaluation inside the loop
         get_fresh_registers(global_deltas, d_global_src);
diff --git a/src/muz_qe/dl_compiler.cpp.orig b/src/muz_qe/dl_compiler.cpp.orig
new file mode 100644
index 000000000..e4528426a
--- /dev/null
+++ b/src/muz_qe/dl_compiler.cpp.orig
@@ -0,0 +1,1245 @@
+/*++
+Copyright (c) 2006 Microsoft Corporation
+
+Module Name:
+
+    dl_compiler.cpp
+
+Abstract:
+
+    <abstract>
+
+Author:
+
+    Krystof Hoder (t-khoder) 2010-09-14.
+
+Revision History:
+
+--*/
+
+
+#include <sstream>
+#include"ref_vector.h"
+#include"dl_context.h"
+#include"dl_rule.h"
+#include"dl_util.h"
+#include"dl_compiler.h"
+#include"ast_pp.h"
+#include"ast_smt2_pp.h"
+
+
+namespace datalog {
+
+    void compiler::reset() {
+        m_pred_regs.reset();
+        m_new_reg = 0;
+    }
+
+    void compiler::ensure_predicate_loaded(func_decl * pred, instruction_block & acc) {
+        pred2idx::obj_map_entry * e = m_pred_regs.insert_if_not_there2(pred, UINT_MAX);
+        if(e->get_data().m_value!=UINT_MAX) {
+            //predicate is already loaded
+            return;
+        }
+        relation_signature sig;
+        m_context.get_rel_context().get_rmanager().from_predicate(pred, sig);
+        reg_idx reg = get_fresh_register(sig);
+        e->get_data().m_value=reg;
+
+        acc.push_back(instruction::mk_load(m_context.get_manager(), pred, reg));
+    }
+
+    void compiler::make_join(reg_idx t1, reg_idx t2, const variable_intersection & vars, reg_idx & result, 
+            instruction_block & acc) {
+        relation_signature res_sig;
+        relation_signature::from_join(m_reg_signatures[t1], m_reg_signatures[t2], vars.size(), 
+            vars.get_cols1(), vars.get_cols2(), res_sig);
+        result = get_fresh_register(res_sig);
+        acc.push_back(instruction::mk_join(t1, t2, vars.size(), vars.get_cols1(), vars.get_cols2(), result));
+    }
+
+    void compiler::make_join_project(reg_idx t1, reg_idx t2, const variable_intersection & vars, 
+            const unsigned_vector & removed_cols, reg_idx & result, instruction_block & acc) {
+        relation_signature aux_sig;
+        relation_signature sig1 = m_reg_signatures[t1];
+        relation_signature sig2 = m_reg_signatures[t2];
+        relation_signature::from_join(sig1, sig2, vars.size(), vars.get_cols1(), vars.get_cols2(), aux_sig);
+        relation_signature res_sig;
+        relation_signature::from_project(aux_sig, removed_cols.size(), removed_cols.c_ptr(), 
+            res_sig);
+        result = get_fresh_register(res_sig);
+
+        acc.push_back(instruction::mk_join_project(t1, t2, vars.size(), vars.get_cols1(), 
+            vars.get_cols2(), removed_cols.size(), removed_cols.c_ptr(), result));
+    }
+
+    void compiler::make_select_equal_and_project(reg_idx src, const relation_element & val, unsigned col,
+            reg_idx & result, instruction_block & acc) {
+        relation_signature res_sig;
+        relation_signature::from_project(m_reg_signatures[src], 1, &col, res_sig);
+        result = get_fresh_register(res_sig);
+        acc.push_back(instruction::mk_select_equal_and_project(m_context.get_manager(),
+            src, val, col, result));
+    }
+
+    void compiler::make_clone(reg_idx src, reg_idx & result, instruction_block & acc) {
+        relation_signature sig = m_reg_signatures[src];
+        result = get_fresh_register(sig);
+        acc.push_back(instruction::mk_clone(src, result));
+    }
+
+    void compiler::make_union(reg_idx src, reg_idx tgt, reg_idx delta, bool use_widening, 
+            instruction_block & acc) {
+        SASSERT(m_reg_signatures[src]==m_reg_signatures[tgt]);
+        SASSERT(delta==execution_context::void_register || m_reg_signatures[src]==m_reg_signatures[delta]);
+
+        if (use_widening) {
+            acc.push_back(instruction::mk_widen(src, tgt, delta));
+        }
+        else {
+            acc.push_back(instruction::mk_union(src, tgt, delta));
+        }
+    }
+
+    void compiler::make_projection(reg_idx src, unsigned col_cnt, const unsigned * removed_cols, 
+            reg_idx & result, instruction_block & acc) {
+        SASSERT(col_cnt>0);
+
+        relation_signature res_sig;
+        relation_signature::from_project(m_reg_signatures[src], col_cnt, removed_cols, res_sig);
+        result = get_fresh_register(res_sig);
+        acc.push_back(instruction::mk_projection(src, col_cnt, removed_cols, result));
+    }
+
+    compiler::reg_idx compiler::get_fresh_register(const relation_signature & sig) {
+        //since we might be resizing the m_reg_signatures vector, the argument must not point inside it
+        SASSERT((&sig>=m_reg_signatures.end()) || (&sig<m_reg_signatures.begin()));
+        reg_idx result = m_reg_signatures.size();
+        m_reg_signatures.push_back(sig);
+        return result;
+    }
+
+    compiler::reg_idx compiler::get_single_column_register(const relation_sort & s) {
+        relation_signature singl_sig;
+        singl_sig.push_back(s);
+        return get_fresh_register(singl_sig);
+    }
+
+    void compiler::get_fresh_registers(const func_decl_set & preds,  pred2idx & regs) {
+        func_decl_set::iterator pit = preds.begin();
+        func_decl_set::iterator pend = preds.end();
+        for(; pit!=pend; ++pit) {
+            func_decl * pred = *pit;
+            reg_idx reg = m_pred_regs.find(pred);
+
+            SASSERT(!regs.contains(pred));
+            relation_signature sig = m_reg_signatures[reg];
+            reg_idx delta_reg = get_fresh_register(sig);
+            regs.insert(pred, delta_reg);
+        }
+    }
+
+    void compiler::make_dealloc_non_void(reg_idx r, instruction_block & acc) {
+        if(r!=execution_context::void_register) {
+            acc.push_back(instruction::mk_dealloc(r));
+        }
+    }
+
+    void compiler::make_add_constant_column(func_decl* head_pred, reg_idx src, const relation_sort & s, const relation_element & val,
+            reg_idx & result, bool & dealloc, instruction_block & acc) {
+        reg_idx singleton_table;
+        if(!m_constant_registers.find(s, val, singleton_table)) {
+            singleton_table = get_single_column_register(s);
+            m_top_level_code.push_back(
+                instruction::mk_unary_singleton(m_context.get_manager(), head_pred, s, val, singleton_table));
+            m_constant_registers.insert(s, val, singleton_table);
+        }
+        if(src==execution_context::void_register) {
+            result = singleton_table;
+            dealloc = false;
+        }
+        else {
+            variable_intersection empty_vars(m_context.get_manager());
+            make_join(src, singleton_table, empty_vars, result, acc);
+            dealloc = true;
+        }
+    }
+
+    void compiler::make_add_unbound_column(rule* compiled_rule, unsigned col_idx, func_decl* pred, reg_idx src, const relation_sort & s, reg_idx & result, 
+            bool & dealloc, instruction_block & acc) {
+        
+        TRACE("dl", tout << "Adding unbound column " << mk_pp(pred, m_context.get_manager()) << "\n";);
+            IF_VERBOSE(3, { 
+                    expr_ref e(m_context.get_manager()); 
+                    compiled_rule->to_formula(e); 
+                    verbose_stream() << "Compiling unsafe rule column " << col_idx << "\n" 
+                                     << mk_ismt2_pp(e, m_context.get_manager()) << "\n"; 
+                });
+        reg_idx total_table;
+        if (!m_total_registers.find(s, pred, total_table)) {
+            total_table = get_single_column_register(s);
+            relation_signature sig;
+            sig.push_back(s);
+            m_top_level_code.push_back(instruction::mk_total(sig, pred, total_table));
+            m_total_registers.insert(s, pred, total_table);
+        }       
+        if(src == execution_context::void_register) {
+            result = total_table;
+            dealloc = false;
+        }
+        else {
+            variable_intersection empty_vars(m_context.get_manager());
+            make_join(src, total_table, empty_vars, result, acc);
+            dealloc = true;
+        }
+    }
+
+    void compiler::make_full_relation(func_decl* pred, const relation_signature & sig, reg_idx & result, 
+            instruction_block & acc) {
+        SASSERT(sig.empty());
+        TRACE("dl", tout << "Adding unbound column " << mk_pp(pred, m_context.get_manager()) << "\n";);
+        if (m_empty_tables_registers.find(pred, result))
+            return;
+
+        result = get_fresh_register(sig);
+        m_top_level_code.push_back(instruction::mk_total(sig, pred, result));
+        m_empty_tables_registers.insert(pred, result);
+    }
+
+
+    void compiler::make_duplicate_column(reg_idx src, unsigned col, reg_idx & result, 
+            instruction_block & acc) {
+
+        relation_signature & src_sig = m_reg_signatures[src];
+        reg_idx single_col_reg;
+        unsigned src_col_cnt = src_sig.size();
+        if(src_col_cnt==1) {
+            single_col_reg = src;
+        }
+        else {
+            unsigned_vector removed_cols;
+            for(unsigned i=0; i<src_col_cnt; i++) {
+                if(i!=col) {
+                    removed_cols.push_back(i);
+                }
+            }
+            make_projection(src, removed_cols.size(), removed_cols.c_ptr(), single_col_reg, acc);
+        }
+        variable_intersection vi(m_context.get_manager());
+        vi.add_pair(col, 0);
+        make_join(src, single_col_reg, vi, result, acc);
+        make_dealloc_non_void(single_col_reg, acc);
+    }
+
+    void compiler::make_rename(reg_idx src, unsigned cycle_len, const unsigned * permutation_cycle, 
+            reg_idx & result, instruction_block & acc) {
+        relation_signature res_sig;
+        relation_signature::from_rename(m_reg_signatures[src], cycle_len, permutation_cycle, res_sig);
+        result = get_fresh_register(res_sig);
+        acc.push_back(instruction::mk_rename(src, cycle_len, permutation_cycle, result));
+    }
+
+    void compiler::make_assembling_code(
+        rule* compiled_rule, 
+        func_decl* head_pred, 
+        reg_idx    src, 
+        const svector<assembling_column_info> & acis0,
+        reg_idx &           result, 
+        bool & dealloc,
+        instruction_block & acc) {
+
+        TRACE("dl", tout << mk_pp(head_pred, m_context.get_manager()) << "\n";);
+
+        unsigned col_cnt = acis0.size();
+        reg_idx curr = src;
+
+        relation_signature empty_signature;
+
+        relation_signature * curr_sig;
+        if(curr!=execution_context::void_register) {
+            curr_sig = & m_reg_signatures[curr];
+        }
+        else {
+            curr_sig = & empty_signature;
+        }
+        unsigned src_col_cnt=curr_sig->size();
+
+        svector<assembling_column_info> acis(acis0);
+        int2int handled_unbound;
+
+        //first remove unused source columns
+        int_set referenced_src_cols;
+        for(unsigned i=0; i<col_cnt; i++) {
+            if(acis[i].kind==ACK_BOUND_VAR) {
+                SASSERT(acis[i].source_column<src_col_cnt); //we refer only to existing columns
+                referenced_src_cols.insert(acis[i].source_column);
+            }
+        }
+
+        //if an ACK_BOUND_VAR pointed to column i, after projection it will point to
+        //i-new_src_col_offset[i] due to removal of some of earlier columns
+        unsigned_vector new_src_col_offset;
+
+        unsigned_vector src_cols_to_remove;
+        for(unsigned i=0; i<src_col_cnt; i++) {
+            if(!referenced_src_cols.contains(i)) {
+                src_cols_to_remove.push_back(i);
+            }
+            new_src_col_offset.push_back(src_cols_to_remove.size());
+        }
+        if(!src_cols_to_remove.empty()) {
+            reg_idx new_curr;
+            make_projection(curr, src_cols_to_remove.size(), src_cols_to_remove.c_ptr(), new_curr, acc);
+            if (dealloc)
+                make_dealloc_non_void(curr, acc);
+            dealloc = true;
+            curr=new_curr;
+            curr_sig = & m_reg_signatures[curr];
+
+            //update ACK_BOUND_VAR references
+            for(unsigned i=0; i<col_cnt; i++) {
+                if(acis[i].kind==ACK_BOUND_VAR) {
+                    unsigned col = acis[i].source_column;
+                    acis[i].source_column = col-new_src_col_offset[col];
+                }
+            }
+        }
+
+        //convert all result columns into bound variables by extending the source table
+        for(unsigned i=0; i<col_cnt; i++) {
+            if(acis[i].kind==ACK_BOUND_VAR) {
+                continue;
+            }
+            unsigned bound_column_index;
+            if(acis[i].kind!=ACK_UNBOUND_VAR || !handled_unbound.find(acis[i].var_index,bound_column_index)) {
+                reg_idx new_curr;
+                bool new_dealloc;
+                bound_column_index=curr_sig->size();
+                if(acis[i].kind==ACK_CONSTANT) {
+                    make_add_constant_column(head_pred, curr, acis[i].domain, acis[i].constant, new_curr, new_dealloc, acc);
+                }
+                else {
+                    SASSERT(acis[i].kind==ACK_UNBOUND_VAR);
+                    make_add_unbound_column(compiled_rule, i, head_pred, curr, acis[i].domain, new_curr, new_dealloc, acc);
+                    handled_unbound.insert(acis[i].var_index,bound_column_index);
+                }
+                if (dealloc)
+                    make_dealloc_non_void(curr, acc);
+                dealloc = new_dealloc;
+                curr=new_curr;
+                curr_sig = & m_reg_signatures[curr];
+                SASSERT(bound_column_index==curr_sig->size()-1);
+            }
+            SASSERT((*curr_sig)[bound_column_index]==acis[i].domain);
+            acis[i].kind=ACK_BOUND_VAR;
+            acis[i].source_column=bound_column_index;
+        }
+
+        //duplicate needed source columns
+        int_set used_cols;
+        for(unsigned i=0; i<col_cnt; i++) {
+            SASSERT(acis[i].kind==ACK_BOUND_VAR);
+            unsigned col=acis[i].source_column;
+            if(!used_cols.contains(col)) {
+                used_cols.insert(col);
+                continue;
+            }
+            reg_idx new_curr;
+            make_duplicate_column(curr, col, new_curr, acc);
+            if (dealloc)
+                make_dealloc_non_void(curr, acc);
+            dealloc = true;
+            curr=new_curr;
+            curr_sig = & m_reg_signatures[curr];
+            unsigned bound_column_index=curr_sig->size()-1;
+            SASSERT((*curr_sig)[bound_column_index]==acis[i].domain);
+            acis[i].source_column=bound_column_index;
+        }
+
+        //reorder source columns to match target
+        SASSERT(curr_sig->size()==col_cnt); //now the intermediate table is a permutation
+        for(unsigned i=0; i<col_cnt; i++) {
+            if(acis[i].source_column==i) {
+                continue;
+            }
+            unsigned_vector permutation;
+            unsigned next=i;
+            do {
+                permutation.push_back(next);
+                unsigned prev=next;
+                next=acis[prev].source_column;
+                SASSERT(next>=i); //columns below i are already reordered
+                SASSERT(next<col_cnt);
+                acis[prev].source_column=prev;
+                SASSERT(permutation.size()<=col_cnt); //this should not be an infinite loop
+            } while(next!=i);
+
+            reg_idx new_curr;
+            make_rename(curr, permutation.size(), permutation.c_ptr(), new_curr, acc);
+            if (dealloc)
+                make_dealloc_non_void(curr, acc);
+            dealloc = true;
+            curr=new_curr;
+            curr_sig = & m_reg_signatures[curr];
+        }
+
+        if(curr==execution_context::void_register) {
+            SASSERT(src==execution_context::void_register);
+            SASSERT(acis0.size()==0);
+            make_full_relation(head_pred, empty_signature, curr, acc);
+            dealloc = false;
+        }
+
+        result=curr;
+    }
+
+    void compiler::get_local_indexes_for_projection(app * t, var_counter & globals, unsigned ofs, 
+            unsigned_vector & res) {
+        unsigned n = t->get_num_args();
+        for(unsigned i = 0; i<n; i++) {
+            expr * e = t->get_arg(i);
+            if(!is_var(e) || globals.get(to_var(e)->get_idx())!=0) {
+                continue;
+            }
+            res.push_back(i+ofs);
+        }
+    }
+
+    void compiler::get_local_indexes_for_projection(rule * r, unsigned_vector & res) {
+        SASSERT(r->get_positive_tail_size()==2);
+        ast_manager & m = m_context.get_manager();
+        rule_counter counter;
+        counter.count_rule_vars(m, r);
+        app * t1 = r->get_tail(0);
+        app * t2 = r->get_tail(1);
+        counter.count_vars(m, t1, -1);
+        counter.count_vars(m, t2, -1);
+        get_local_indexes_for_projection(t1, counter, 0, res);
+        get_local_indexes_for_projection(t2, counter, t1->get_num_args(), res);
+    }
+
+    void compiler::compile_rule_evaluation_run(rule * r, reg_idx head_reg, const reg_idx * tail_regs, 
+            reg_idx delta_reg, bool use_widening, instruction_block & acc) {
+        
+        ast_manager & m = m_context.get_manager();
+        m_instruction_observer.start_rule(r);
+
+        const app * h = r->get_head();
+        unsigned head_len = h->get_num_args();
+        func_decl * head_pred = h->get_decl();
+
+        TRACE("dl", r->display(m_context, tout); );
+
+        unsigned pt_len = r->get_positive_tail_size();
+        SASSERT(pt_len<=2); //we require rules to be processed by the mk_simple_joins rule transformer plugin
+
+        reg_idx single_res;
+        expr_ref_vector single_res_expr(m);
+
+        //used to save on filter_identical instructions where the check is already done 
+        //by the join operation
+        unsigned second_tail_arg_ofs;
+
+        // whether to dealloc the previous result
+        bool dealloc = true;
+
+        if(pt_len == 2) {
+            reg_idx t1_reg=tail_regs[0];
+            reg_idx t2_reg=tail_regs[1];
+            app * a1 = r->get_tail(0);
+            app * a2 = r->get_tail(1);
+            SASSERT(m_reg_signatures[t1_reg].size()==a1->get_num_args());
+            SASSERT(m_reg_signatures[t2_reg].size()==a2->get_num_args());
+
+            variable_intersection a1a2(m_context.get_manager());
+            a1a2.populate(a1,a2);
+
+            unsigned_vector removed_cols;
+            get_local_indexes_for_projection(r, removed_cols);
+
+            if(removed_cols.empty()) {
+                make_join(t1_reg, t2_reg, a1a2, single_res, acc);
+            }
+            else {
+                make_join_project(t1_reg, t2_reg, a1a2, removed_cols, single_res, acc);
+            }
+
+            unsigned rem_index = 0;
+            unsigned rem_sz = removed_cols.size();
+            unsigned a1len=a1->get_num_args();
+            for(unsigned i=0; i<a1len; i++) {
+                SASSERT(rem_index==rem_sz || removed_cols[rem_index]>=i);
+                if(rem_index<rem_sz && removed_cols[rem_index]==i) {
+                    rem_index++;
+                    continue;
+                }
+                single_res_expr.push_back(a1->get_arg(i));
+            }
+            second_tail_arg_ofs = single_res_expr.size();
+            unsigned a2len=a2->get_num_args();
+            for(unsigned i=0; i<a2len; i++) {
+                SASSERT(rem_index==rem_sz || removed_cols[rem_index]>=i+a1len);
+                if(rem_index<rem_sz && removed_cols[rem_index]==i+a1len) {
+                    rem_index++;
+                    continue;
+                }
+                single_res_expr.push_back(a2->get_arg(i));
+            }
+            SASSERT(rem_index==rem_sz);
+        }
+        else if(pt_len==1) {
+            reg_idx t_reg=tail_regs[0];
+            app * a = r->get_tail(0);
+            SASSERT(m_reg_signatures[t_reg].size()==a->get_num_args());
+
+            single_res = t_reg;
+
+            unsigned n=a->get_num_args();
+            for(unsigned i=0; i<n; i++) {
+                expr * arg = a->get_arg(i);
+                if(is_app(arg)) {
+                    app * c = to_app(arg); //argument is a constant
+                    SASSERT(c->get_num_args()==0);
+                    SASSERT(m_context.get_decl_util().is_numeral_ext(arg));
+                    reg_idx new_reg;
+                    make_select_equal_and_project(single_res, c, single_res_expr.size(), new_reg, acc);
+                    if(single_res!=t_reg) {
+                        //since single_res is a local register, we deallocate it
+                        make_dealloc_non_void(single_res, acc);
+                    }
+                    single_res = new_reg;
+                }
+                else {
+                    SASSERT(is_var(arg));
+                    single_res_expr.push_back(arg);
+                }
+            }
+            if(single_res==t_reg) {
+                dealloc = false;
+            }
+
+        }
+        else {
+            SASSERT(pt_len==0);
+
+            //single_res register should never be used in this case
+            single_res=execution_context::void_register;
+        }
+
+        add_unbound_columns_for_negation(r, head_pred, single_res, single_res_expr, dealloc, acc);
+
+        int2ints var_indexes;
+
+        reg_idx filtered_res = single_res;
+
+        {
+            //enforce equality to constants
+            unsigned srlen=single_res_expr.size();
+            SASSERT((single_res==execution_context::void_register) ? (srlen==0) : (srlen==m_reg_signatures[single_res].size()));
+            for(unsigned i=0; i<srlen; i++) {
+                expr * exp = single_res_expr[i].get();
+                if(is_app(exp)) {
+                    SASSERT(m_context.get_decl_util().is_numeral_ext(exp));
+                    relation_element value = to_app(exp);
+                    if (!dealloc)
+                        make_clone(filtered_res, filtered_res, acc);
+                    acc.push_back(instruction::mk_filter_equal(m_context.get_manager(), filtered_res, value, i));
+                    dealloc = true;
+                }
+                else {
+                    SASSERT(is_var(exp));
+                    unsigned var_num=to_var(exp)->get_idx();
+                    int2ints::entry * e = var_indexes.insert_if_not_there2(var_num, unsigned_vector());
+                    e->get_data().m_value.push_back(i);
+                }
+            }
+        }
+
+        //enforce equality of columns
+        int2ints::iterator vit=var_indexes.begin();
+        int2ints::iterator vend=var_indexes.end();
+        for(; vit!=vend; ++vit) {
+            int2ints::key_data & k = *vit;
+            unsigned_vector & indexes = k.m_value;
+            if(indexes.size()==1) {
+                continue;
+            }
+            SASSERT(indexes.size()>1);
+            if(pt_len==2 && indexes[0]<second_tail_arg_ofs && indexes.back()>=second_tail_arg_ofs) {
+                //If variable appears in multiple tails, the identicity will already be enforced by join.
+                //(If behavior the join changes so that it is not enforced anymore, remove this
+                //condition!)
+                continue;
+            }
+            if (!dealloc)
+                make_clone(filtered_res, filtered_res, acc);
+            acc.push_back(instruction::mk_filter_identical(filtered_res, indexes.size(), indexes.c_ptr()));
+            dealloc = true;
+        }
+
+        //enforce negative predicates
+        unsigned ut_len=r->get_uninterpreted_tail_size();
+        for(unsigned i=pt_len; i<ut_len; i++) {
+            app * neg_tail = r->get_tail(i);
+            func_decl * neg_pred = neg_tail->get_decl();
+            variable_intersection neg_intersection(m_context.get_manager());
+            neg_intersection.populate(single_res_expr, neg_tail);
+            unsigned_vector t_cols(neg_intersection.size(), neg_intersection.get_cols1());
+            unsigned_vector neg_cols(neg_intersection.size(), neg_intersection.get_cols2());
+
+            unsigned neg_len = neg_tail->get_num_args();
+            for(unsigned i=0; i<neg_len; i++) {
+                expr * e = neg_tail->get_arg(i);
+                if(is_var(e)) {
+                    continue;
+                }
+                SASSERT(is_app(e));
+                relation_sort arg_sort;
+                m_context.get_rel_context().get_rmanager().from_predicate(neg_pred, i, arg_sort);
+                reg_idx new_reg;
+                bool new_dealloc;
+                make_add_constant_column(head_pred, filtered_res, arg_sort, to_app(e), new_reg, new_dealloc, acc);
+
+                if (dealloc)
+                    make_dealloc_non_void(filtered_res, acc);
+                dealloc = new_dealloc;
+                filtered_res = new_reg;                // here filtered_res value gets changed !!
+
+                t_cols.push_back(single_res_expr.size());
+                neg_cols.push_back(i);
+                single_res_expr.push_back(e);
+            }
+            SASSERT(t_cols.size()==neg_cols.size());
+
+            reg_idx neg_reg = m_pred_regs.find(neg_pred);
+            if (!dealloc)
+                make_clone(filtered_res, filtered_res, acc);
+            acc.push_back(instruction::mk_filter_by_negation(filtered_res, neg_reg, t_cols.size(),
+                t_cols.c_ptr(), neg_cols.c_ptr()));
+            dealloc = true;
+        }
+
+        // enforce interpreted tail predicates
+        unsigned ft_len=r->get_tail_size(); //full tail
+        for(unsigned tail_index=ut_len; tail_index<ft_len; tail_index++) {
+            app * t = r->get_tail(tail_index);
+            ptr_vector<sort> t_vars;
+            ::get_free_vars(t, t_vars);
+            
+            if(t_vars.empty()) {
+                expr_ref simplified(m);
+                m_context.get_rewriter()(t, simplified);
+                if(m.is_true(simplified)) {
+                    //this tail element is always true
+                    continue;
+                }
+                //the tail of this rule is never satisfied
+                SASSERT(m.is_false(simplified));
+                goto finish;
+            }
+
+            //determine binding size
+            while (!t_vars.back()) {
+                t_vars.pop_back();
+            }
+            unsigned max_var = t_vars.size();
+
+            //create binding
+            expr_ref_vector binding(m);
+            binding.resize(max_var+1);
+            
+            for(unsigned v = 0; v < t_vars.size(); ++v) {
+                if (!t_vars[v]) {
+                    continue;
+                }
+                int2ints::entry * e = var_indexes.find_core(v);
+                if(!e) {
+                    //we have an unbound variable, so we add an unbound column for it
+                    relation_sort unbound_sort = t_vars[v];
+
+                    reg_idx new_reg;
+                    TRACE("dl", tout << mk_pp(head_pred, m_context.get_manager()) << "\n";);
+                    bool new_dealloc;
+                    make_add_unbound_column(r, 0, head_pred, filtered_res, unbound_sort, new_reg, new_dealloc, acc);
+
+                    if (dealloc)
+                        make_dealloc_non_void(filtered_res, acc);
+                    dealloc = new_dealloc;
+                    filtered_res = new_reg;                // here filtered_res value gets changed !!
+
+                    unsigned unbound_column_index = single_res_expr.size();
+                    single_res_expr.push_back(m.mk_var(v, unbound_sort));
+
+                    e = var_indexes.insert_if_not_there2(v, unsigned_vector());
+                    e->get_data().m_value.push_back(unbound_column_index);
+                }
+                unsigned src_col=e->get_data().m_value.back();
+                relation_sort var_sort = m_reg_signatures[filtered_res][src_col];
+                binding[max_var-v]=m.mk_var(src_col, var_sort);
+            }
+
+
+            expr_ref renamed(m);
+            m_context.get_var_subst()(t, binding.size(), binding.c_ptr(), renamed);
+            app_ref app_renamed(to_app(renamed), m);
+            if (!dealloc)
+                make_clone(filtered_res, filtered_res, acc);
+            acc.push_back(instruction::mk_filter_interpreted(filtered_res, app_renamed));
+            dealloc = true;
+        }
+
+        {
+            //put together the columns of head relation
+            relation_signature & head_sig = m_reg_signatures[head_reg];
+            svector<assembling_column_info> head_acis;
+            unsigned_vector head_src_cols;
+            for(unsigned i=0; i<head_len; i++) {
+                assembling_column_info aci;
+                aci.domain=head_sig[i];
+
+                expr * exp = h->get_arg(i);
+                if(is_var(exp)) {
+                    unsigned var_num=to_var(exp)->get_idx();
+                    int2ints::entry * e = var_indexes.find_core(var_num);
+                    if(e) {
+                        unsigned_vector & binding_indexes = e->get_data().m_value;
+                        aci.kind=ACK_BOUND_VAR;
+                        aci.source_column=binding_indexes.back();
+                        SASSERT(aci.source_column<single_res_expr.size()); //we bind only to existing columns
+                        if(binding_indexes.size()>1) {
+                            //if possible, we do not want multiple head columns
+                            //point to a single column in the intermediate table,
+                            //since then we would have to duplicate the column
+                            //(and remove columns we did not point to at all)
+                            binding_indexes.pop_back();
+                        }
+                    }
+                    else {
+                        aci.kind=ACK_UNBOUND_VAR;
+                        aci.var_index=var_num;
+                    }
+                }
+                else {
+                    SASSERT(is_app(exp));
+                    SASSERT(m_context.get_decl_util().is_numeral_ext(exp));
+                    aci.kind=ACK_CONSTANT;
+                    aci.constant=to_app(exp);
+                }
+                head_acis.push_back(aci);
+            }
+            SASSERT(head_acis.size()==head_len);
+
+            reg_idx new_head_reg;
+            make_assembling_code(r, head_pred, filtered_res, head_acis, new_head_reg, dealloc, acc);
+
+            //update the head relation
+            make_union(new_head_reg, head_reg, delta_reg, use_widening, acc);
+            if (dealloc)
+                make_dealloc_non_void(new_head_reg, acc);
+        }
+
+    finish:
+        m_instruction_observer.finish_rule();
+    }
+
+    void compiler::add_unbound_columns_for_negation(rule* r, func_decl* pred, reg_idx& single_res, expr_ref_vector& single_res_expr, 
+                                                    bool & dealloc, instruction_block & acc) {
+        uint_set pos_vars;
+        u_map<expr*> neg_vars;
+        ast_manager& m = m_context.get_manager();
+        unsigned pt_len = r->get_positive_tail_size();
+        unsigned ut_len = r->get_uninterpreted_tail_size();
+        if (pt_len == ut_len || pt_len == 0) {
+            return;
+        }
+        // populate negative variables:
+        for (unsigned i = pt_len; i < ut_len; ++i) {
+            app * neg_tail = r->get_tail(i);
+            unsigned neg_len = neg_tail->get_num_args();
+            for (unsigned j = 0; j < neg_len; ++j) {
+                expr * e = neg_tail->get_arg(j);
+                if (is_var(e)) {
+                    neg_vars.insert(to_var(e)->get_idx(), e);
+                }
+            }
+        }
+        // populate positive variables:
+        for (unsigned i = 0; i < single_res_expr.size(); ++i) {
+            expr* e = single_res_expr[i].get();
+            if (is_var(e)) {
+                pos_vars.insert(to_var(e)->get_idx());
+            }
+        }
+        // add negative variables that are not in positive:
+        u_map<expr*>::iterator it = neg_vars.begin(), end = neg_vars.end();
+        for (; it != end; ++it) {
+            unsigned v = it->m_key;
+            expr* e = it->m_value;
+            if (!pos_vars.contains(v)) {
+                single_res_expr.push_back(e);
+                reg_idx new_single_res;
+                bool new_dealloc;
+                make_add_unbound_column(r, v, pred, single_res, m.get_sort(e), new_single_res, new_dealloc, acc);
+                if (dealloc)
+                    make_dealloc_non_void(single_res, acc);
+                dealloc = new_dealloc;
+                single_res = new_single_res;
+                TRACE("dl", tout << "Adding unbound column: " << mk_pp(e, m) << "\n";);
+            }
+        }
+    }
+
+    void compiler::compile_rule_evaluation(rule * r, const pred2idx * input_deltas,
+            reg_idx output_delta, bool use_widening, instruction_block & acc) {
+        typedef std::pair<reg_idx, unsigned> tail_delta_info; //(delta register, tail index)
+        typedef svector<tail_delta_info> tail_delta_infos;
+
+        unsigned rule_len = r->get_uninterpreted_tail_size();
+        reg_idx head_reg = m_pred_regs.find(r->get_decl());
+
+        svector<reg_idx> tail_regs;
+        tail_delta_infos tail_deltas;
+        for(unsigned j=0;j<rule_len;j++) {
+            func_decl * tail_pred = r->get_tail(j)->get_decl();
+            reg_idx tail_reg = m_pred_regs.find(tail_pred);
+            tail_regs.push_back(tail_reg);
+
+            if(input_deltas && !all_or_nothing_deltas()) {
+                reg_idx tail_delta_idx;
+                if(input_deltas->find(tail_pred, tail_delta_idx)) {
+                    tail_deltas.push_back(tail_delta_info(tail_delta_idx, j));
+                }
+            }
+        }
+
+        if(!input_deltas || all_or_nothing_deltas()) {
+            compile_rule_evaluation_run(r, head_reg, tail_regs.c_ptr(), output_delta, use_widening, acc);
+        }
+        else {
+            tail_delta_infos::iterator tdit = tail_deltas.begin();
+            tail_delta_infos::iterator tdend = tail_deltas.end();
+            for(; tdit!=tdend; ++tdit) {
+                tail_delta_info tdinfo = *tdit;
+                flet<reg_idx> flet_tail_reg(tail_regs[tdinfo.second], tdinfo.first);
+                compile_rule_evaluation_run(r, head_reg, tail_regs.c_ptr(), output_delta, use_widening, acc);
+            }
+        }
+    }
+
+    class cycle_breaker
+    {
+        typedef func_decl * T;
+        typedef rule_dependencies::item_set item_set; //set of T
+
+        rule_dependencies & m_deps;
+        rule_set const& m_rules;
+        context& m_context;
+        item_set & m_removed;
+        svector<T> m_stack;
+        ast_mark m_visited;
+
+        void traverse(T v) {
+            SASSERT(!m_visited.is_marked(v));
+            if (m_removed.contains(v)) {
+                return;
+            }
+
+            m_stack.push_back(v);
+            m_visited.mark(v, true);
+
+            const item_set & deps = m_deps.get_deps(v);
+            item_set::iterator it = deps.begin();
+            item_set::iterator end = deps.end();
+            for(; it!=end; ++it) {
+                T d = *it;
+                if (m_visited.is_marked(d)) {
+                    //TODO: find the best vertex to remove in the cycle
+                    remove_from_stack();
+                    continue;
+                }
+                traverse(d);
+            }
+            SASSERT(m_stack.back()==v);
+
+            m_stack.pop_back();
+            m_visited.mark(v, false);
+        }
+
+        void remove_from_stack() {
+            for (unsigned i = 0; i < m_stack.size(); ++i) {
+                func_decl* p = m_stack[i];
+                if (m_context.has_facts(p)) {
+                    m_removed.insert(p);
+                    return;
+                }
+
+                rule_vector const& rules = m_rules.get_predicate_rules(p);
+                unsigned stratum = m_rules.get_predicate_strat(p);
+                for (unsigned j = 0; j < rules.size(); ++j) {
+                    rule const& r = *rules[j];
+                    bool ok = true;
+                    for (unsigned k = 0; ok && k < r.get_uninterpreted_tail_size(); ++k) {
+                        ok = m_rules.get_predicate_strat(r.get_decl(k)) < stratum;
+                    }
+                    if (ok) {
+                        m_removed.insert(p);
+                        return;
+                    }
+                }
+            }
+
+            // nothing was found.
+            m_removed.insert(m_stack.back());
+        }
+
+    public:
+        cycle_breaker(rule_dependencies & deps, rule_set const& rules, context& ctx, item_set & removed) 
+            : m_deps(deps), m_rules(rules), m_context(ctx), m_removed(removed) { SASSERT(removed.empty()); }
+
+        void operator()() {
+            rule_dependencies::iterator it = m_deps.begin();
+            rule_dependencies::iterator end = m_deps.end();
+            for(; it!=end; ++it) {
+                T v = it->m_key;
+                traverse(v);
+            }
+            m_deps.remove(m_removed);
+        }
+    };
+
+    void compiler::detect_chains(const func_decl_set & preds, func_decl_vector & ordered_preds, 
+            func_decl_set & global_deltas) {
+        typedef obj_map<func_decl, func_decl *> pred2pred;
+
+        SASSERT(ordered_preds.empty());
+        SASSERT(global_deltas.empty());
+
+        rule_dependencies deps(m_rule_set.get_dependencies());
+        deps.restrict(preds);
+        cycle_breaker(deps, m_rule_set, m_context, global_deltas)();
+        VERIFY( deps.sort_deps(ordered_preds) );
+
+        //the predicates that were removed to get acyclic induced subgraph are put last
+        //so that all their local input deltas are already populated
+        func_decl_set::iterator gdit = global_deltas.begin();
+        func_decl_set::iterator gend = global_deltas.end();
+        for(; gdit!=gend; ++gdit) {
+            ordered_preds.push_back(*gdit);
+        }
+    }
+
+    void compiler::compile_preds(const func_decl_vector & head_preds, const func_decl_set & widened_preds,
+            const pred2idx * input_deltas, const pred2idx & output_deltas, instruction_block & acc) {
+        func_decl_vector::const_iterator hpit = head_preds.begin();
+        func_decl_vector::const_iterator hpend = head_preds.end();
+        for(; hpit!=hpend; ++hpit) {
+            func_decl * head_pred = *hpit;
+
+            bool widen_predicate_in_loop = widened_preds.contains(head_pred);
+
+            reg_idx d_head_reg; //output delta for the initial rule execution
+            if(!output_deltas.find(head_pred, d_head_reg)) {
+                d_head_reg = execution_context::void_register;
+            }
+
+            const rule_vector & pred_rules = m_rule_set.get_predicate_rules(head_pred);
+            rule_vector::const_iterator rit = pred_rules.begin();
+            rule_vector::const_iterator rend = pred_rules.end();
+            for(; rit!=rend; ++rit) {
+                rule * r = *rit;
+                SASSERT(head_pred==r->get_decl());
+
+                compile_rule_evaluation(r, input_deltas, d_head_reg, widen_predicate_in_loop, acc);
+            }
+        }
+    }
+
+    void compiler::compile_preds_init(const func_decl_vector & head_preds, const func_decl_set & widened_preds,
+            const pred2idx * input_deltas, const pred2idx & output_deltas, instruction_block & acc) {
+        func_decl_vector::const_iterator hpit = head_preds.begin();
+        func_decl_vector::const_iterator hpend = head_preds.end();
+        reg_idx void_reg = execution_context::void_register;
+        for(; hpit!=hpend; ++hpit) {
+            func_decl * head_pred = *hpit;
+            const rule_vector & pred_rules = m_rule_set.get_predicate_rules(head_pred);
+            rule_vector::const_iterator rit = pred_rules.begin();
+            rule_vector::const_iterator rend = pred_rules.end();
+            unsigned stratum = m_rule_set.get_predicate_strat(head_pred);
+
+            for(; rit != rend; ++rit) {
+                rule * r = *rit;
+                SASSERT(head_pred==r->get_decl());
+
+                for (unsigned i = 0; i < r->get_uninterpreted_tail_size(); ++i) {
+                    unsigned stratum1 = m_rule_set.get_predicate_strat(r->get_decl(i));
+                    if (stratum1 >= stratum) {
+                        goto next_loop;
+                    }
+                }
+                compile_rule_evaluation(r, input_deltas, void_reg, false, acc);
+            next_loop:
+                ;
+            }
+
+            reg_idx d_head_reg;
+            if (output_deltas.find(head_pred, d_head_reg)) {
+                acc.push_back(instruction::mk_clone(m_pred_regs.find(head_pred), d_head_reg));
+            }
+        }
+    }
+
+    void compiler::make_inloop_delta_transition(const pred2idx & global_head_deltas, 
+            const pred2idx & global_tail_deltas, const pred2idx & local_deltas, instruction_block & acc) {
+        //move global head deltas into tail ones
+        pred2idx::iterator gdit = global_head_deltas.begin();
+        pred2idx::iterator gend = global_head_deltas.end();
+        for(; gdit!=gend; ++gdit) {
+            func_decl * pred = gdit->m_key;
+            reg_idx head_reg = gdit->m_value;
+            reg_idx tail_reg = global_tail_deltas.find(pred);
+            acc.push_back(instruction::mk_move(head_reg, tail_reg));
+        }
+        //empty local deltas
+        pred2idx::iterator lit = local_deltas.begin();
+        pred2idx::iterator lend = local_deltas.end();
+        for(; lit!=lend; ++lit) {
+            acc.push_back(instruction::mk_dealloc(lit->m_value));
+        }
+    }
+
+    void compiler::compile_loop(const func_decl_vector & head_preds, const func_decl_set & widened_preds,
+            const pred2idx & global_head_deltas, const pred2idx & global_tail_deltas, 
+            const pred2idx & local_deltas, instruction_block & acc) {
+        instruction_block * loop_body = alloc(instruction_block);
+        loop_body->set_observer(&m_instruction_observer);
+
+        pred2idx all_head_deltas(global_head_deltas);
+        unite_disjoint_maps(all_head_deltas, local_deltas);
+        pred2idx all_tail_deltas(global_tail_deltas);
+        unite_disjoint_maps(all_tail_deltas, local_deltas);
+
+        //generate code for the iterative fixpoint search
+        //The order in which we iterate the preds_vector matters, since rules can depend on
+        //deltas generated earlier in the same iteration.
+        compile_preds(head_preds, widened_preds, &all_tail_deltas, all_head_deltas, *loop_body);
+
+        svector<reg_idx> loop_control_regs; //loop is controlled by global src regs
+        collect_map_range(loop_control_regs, global_tail_deltas);
+        //move target deltas into source deltas at the end of the loop
+        //and clear local deltas
+        make_inloop_delta_transition(global_head_deltas, global_tail_deltas, local_deltas, *loop_body);
+
+        loop_body->set_observer(0);
+        acc.push_back(instruction::mk_while_loop(loop_control_regs.size(),
+            loop_control_regs.c_ptr(), loop_body));
+    }
+
+    void compiler::compile_dependent_rules(const func_decl_set & head_preds,
+            const pred2idx * input_deltas, const pred2idx & output_deltas, 
+            bool add_saturation_marks, instruction_block & acc) {
+        
+        if (!output_deltas.empty()) {
+            func_decl_set::iterator hpit = head_preds.begin();
+            func_decl_set::iterator hpend = head_preds.end();
+            for(; hpit!=hpend; ++hpit) {
+                if(output_deltas.contains(*hpit)) {
+                    //we do not support retrieving deltas for rules that are inside a recursive 
+                    //stratum, since we would have to maintain this 'global' delta through the loop
+                    //iterations
+                    NOT_IMPLEMENTED_YET();
+                }
+            }
+        }
+
+        func_decl_vector preds_vector;
+        func_decl_set global_deltas;
+
+        detect_chains(head_preds, preds_vector, global_deltas);
+
+        func_decl_set local_deltas(head_preds);
+        set_difference(local_deltas, global_deltas);
+
+        pred2idx d_global_src;  //these deltas serve as sources of tuples for rule evaluation inside the loop
+        get_fresh_registers(global_deltas, d_global_src);
+        pred2idx d_global_tgt;  //these deltas are targets for new tuples in rule evaluation inside the loop
+        get_fresh_registers(global_deltas, d_global_tgt);
+        pred2idx d_local;
+        get_fresh_registers(local_deltas, d_local);
+
+        pred2idx d_all_src(d_global_src); //src together with local deltas
+        unite_disjoint_maps(d_all_src, d_local);
+        pred2idx d_all_tgt(d_global_tgt); //tgt together with local deltas
+        unite_disjoint_maps(d_all_tgt, d_local);
+
+
+        func_decl_set empty_func_decl_set;
+
+        //generate code for the initial run
+        // compile_preds(preds_vector, empty_func_decl_set, input_deltas, d_global_src, acc);
+        compile_preds_init(preds_vector, empty_func_decl_set, input_deltas, d_global_src, acc);
+
+        if (compile_with_widening()) {
+            compile_loop(preds_vector, global_deltas, d_global_tgt, d_global_src, d_local, acc);
+        }
+        else {
+            compile_loop(preds_vector, empty_func_decl_set, d_global_tgt, d_global_src, d_local, acc);
+        }
+
+
+        if(add_saturation_marks) {
+            //after the loop finishes, all predicates in the group are saturated, 
+            //so we may mark them as such
+            func_decl_set::iterator fdit = head_preds.begin();
+            func_decl_set::iterator fdend = head_preds.end();
+            for(; fdit!=fdend; ++fdit) {
+                acc.push_back(instruction::mk_mark_saturated(m_context.get_manager(), *fdit));
+            }
+        }
+    }
+
+    bool compiler::is_nonrecursive_stratum(const func_decl_set & preds) const {
+        SASSERT(preds.size()>0);
+        if(preds.size()>1) {
+            return false;
+        }
+        func_decl * head_pred = *preds.begin();
+        const rule_vector & rules = m_rule_set.get_predicate_rules(head_pred);
+        rule_vector::const_iterator it = rules.begin();
+        rule_vector::const_iterator end = rules.end();
+        for(; it!=end; ++it) {
+            //it is sufficient to check just for presence of the first head predicate,
+            //since if the rules are recursive and their heads are strongly connected by dependence,
+            //this predicate must appear in some tail
+            if((*it)->is_in_tail(head_pred)) {
+                return false;
+            }
+        }
+        return true;
+    }
+
+    void compiler::compile_nonrecursive_stratum(const func_decl_set & preds, 
+            const pred2idx * input_deltas, const pred2idx & output_deltas, 
+            bool add_saturation_marks, instruction_block & acc) {
+        //non-recursive stratum always has just one head predicate
+        SASSERT(preds.size()==1);
+        SASSERT(is_nonrecursive_stratum(preds));
+        func_decl * head_pred = *preds.begin();
+        const rule_vector & rules = m_rule_set.get_predicate_rules(head_pred);
+
+
+
+        reg_idx output_delta;
+        if (!output_deltas.find(head_pred, output_delta)) {
+            output_delta = execution_context::void_register;
+        }
+
+        rule_vector::const_iterator it = rules.begin();
+        rule_vector::const_iterator end = rules.end();
+        for (; it != end; ++it) {
+            rule * r = *it;
+            SASSERT(r->get_decl()==head_pred);
+
+            compile_rule_evaluation(r, input_deltas, output_delta, false, acc);
+        }
+
+        if (add_saturation_marks) {
+            //now the predicate is saturated, so we may mark it as such
+            acc.push_back(instruction::mk_mark_saturated(m_context.get_manager(), head_pred));
+        }
+    }
+
+    bool compiler::all_saturated(const func_decl_set & preds) const {
+        func_decl_set::iterator fdit = preds.begin();
+        func_decl_set::iterator fdend = preds.end();
+        for(; fdit!=fdend; ++fdit) {
+            if(!m_context.get_rel_context().get_rmanager().is_saturated(*fdit)) {
+                return false;
+            }
+        }
+        return true;
+    }
+
+    void compiler::compile_strats(const rule_stratifier & stratifier, 
+            const pred2idx * input_deltas, const pred2idx & output_deltas, 
+            bool add_saturation_marks, instruction_block & acc) {
+        rule_set::pred_set_vector strats = stratifier.get_strats();
+        rule_set::pred_set_vector::const_iterator sit = strats.begin();
+        rule_set::pred_set_vector::const_iterator send = strats.end();
+        for(; sit!=send; ++sit) {
+            func_decl_set & strat_preds = **sit;
+
+            if (all_saturated(strat_preds)) {
+                //all predicates in stratum are saturated, so no need to compile rules for them
+                continue;
+            }
+
+            TRACE("dl",
+                tout << "Stratum: ";
+                func_decl_set::iterator pit = strat_preds.begin();
+                func_decl_set::iterator pend = strat_preds.end();
+                for(; pit!=pend; ++pit) {
+                    func_decl * pred = *pit;
+                    tout << pred->get_name() << " ";
+                }
+                tout << "\n";
+                );
+
+            if (is_nonrecursive_stratum(strat_preds)) {
+                //this stratum contains just a single non-recursive rule
+                compile_nonrecursive_stratum(strat_preds, input_deltas, output_deltas, add_saturation_marks, acc);
+            }
+            else {
+                compile_dependent_rules(strat_preds, input_deltas, output_deltas, 
+                    add_saturation_marks, acc);
+            }
+        }
+    }
+
+    void compiler::do_compilation(instruction_block & execution_code, 
+            instruction_block & termination_code) {
+
+        unsigned rule_cnt=m_rule_set.get_num_rules();
+        if(rule_cnt==0) {
+            return;
+        }
+
+        instruction_block & acc = execution_code;
+        acc.set_observer(&m_instruction_observer);
+
+
+        //load predicate data
+        for(unsigned i=0;i<rule_cnt;i++) {
+            const rule * r = m_rule_set.get_rule(i);
+            ensure_predicate_loaded(r->get_decl(), acc);
+
+            unsigned rule_len = r->get_uninterpreted_tail_size();
+            for(unsigned j=0;j<rule_len;j++) {
+                ensure_predicate_loaded(r->get_tail(j)->get_decl(), acc);
+            }
+        }
+        
+        pred2idx empty_pred2idx_map;
+
+        compile_strats(m_rule_set.get_stratifier(), static_cast<pred2idx *>(0), 
+            empty_pred2idx_map, true, execution_code);
+
+
+
+        //store predicate data
+        pred2idx::iterator pit = m_pred_regs.begin();
+        pred2idx::iterator pend = m_pred_regs.end();
+        for(; pit!=pend; ++pit) {
+            pred2idx::key_data & e = *pit;
+            func_decl * pred = e.m_key;
+            reg_idx reg = e.m_value;
+            termination_code.push_back(instruction::mk_store(m_context.get_manager(), pred, reg));
+        }
+
+        acc.set_observer(0);
+
+        TRACE("dl", execution_code.display(m_context.get_rel_context(), tout););
+    }
+
+
+}
+