diff --git a/examples/dotnet/Program.cs b/examples/dotnet/Program.cs
index 76624fa1c..3d2910c8f 100644
--- a/examples/dotnet/Program.cs
+++ b/examples/dotnet/Program.cs
@@ -474,7 +474,7 @@ namespace test_mapi
                 cells_c[i] = new BoolExpr[9];
                 for (uint j = 0; j < 9; j++)
                     cells_c[i][j] = ctx.MkAnd(ctx.MkLe(ctx.MkInt(1), X[i][j]),
-                                                ctx.MkLe(X[i][j], ctx.MkInt(9)));
+                                              ctx.MkLe(X[i][j], ctx.MkInt(9)));
             }
 
             // each row contains a digit at most once
@@ -485,7 +485,13 @@ namespace test_mapi
             // each column contains a digit at most once
             BoolExpr[] cols_c = new BoolExpr[9];
             for (uint j = 0; j < 9; j++)
-                cols_c[j] = ctx.MkDistinct(X[j]);
+            {
+                IntExpr[] column = new IntExpr[9];
+                for (uint i = 0; i < 9; i++)
+                    column[i] = X[i][j];
+
+                cols_c[j] = ctx.MkDistinct(column);
+            }
 
             // each 3x3 square contains a digit at most once
             BoolExpr[][] sq_c = new BoolExpr[3][];
diff --git a/scripts/mk_util.py b/scripts/mk_util.py
index 38213a88b..59122af32 100644
--- a/scripts/mk_util.py
+++ b/scripts/mk_util.py
@@ -1089,20 +1089,19 @@ class DotNetDLLComponent(Component):
                     cs_fp_files.append(os.path.join(self.to_src_dir, self.assembly_info_dir, cs_file))
                     cs_files.append(os.path.join(self.assembly_info_dir, cs_file))
             dllfile = '%s.dll' % self.dll_name
-            out.write('%s:' % dllfile)
+            out.write('%s: %s$(SO_EXT)' % (dllfile, get_component(Z3_DLL_COMPONENT).dll_name))
             for cs_file in cs_fp_files:
                 out.write(' ')
                 out.write(cs_file)
             out.write('\n')
-            out.write('  cd %s && csc /noconfig /unsafe+ /nowarn:1701,1702 /nostdlib+ /errorreport:prompt /warn:4 /define:DEBUG;TRACE /reference:mscorlib.dll /reference:System.Core.dll /reference:System.dll /reference:System.Numerics.dll /debug+ /debug:full /filealign:512 /optimize- /out:%s.dll /target:library' % (self.to_src_dir, self.dll_name))
+            out.write('  csc /noconfig /unsafe+ /nowarn:1701,1702 /nostdlib+ /errorreport:prompt /warn:4 /define:DEBUG;TRACE /reference:mscorlib.dll /reference:System.Core.dll /reference:System.dll /reference:System.Numerics.dll /debug+ /debug:full /filealign:512 /optimize- /linkresource:%s.dll /out:%s.dll /target:library' % (get_component(Z3_DLL_COMPONENT).dll_name, self.dll_name))
+            if VS_X64:
+                out.write(' /platform:x64')
+            else:
+                out.write(' /platform:x86')
             for cs_file in cs_files:
-                out.write(' ')
-                out.write(cs_file)
+                out.write(' %s' % os.path.join(self.to_src_dir, cs_file))
             out.write('\n')
-            # HACK
-            win_to_src_dir = self.to_src_dir.replace('/', '\\')
-            out.write('  move %s\n' % os.path.join(win_to_src_dir, dllfile))
-            out.write('  move %s.pdb\n' % os.path.join(win_to_src_dir, self.dll_name))
             out.write('%s: %s\n\n' % (self.name, dllfile))
             return
     
diff --git a/src/api/api_ast.cpp b/src/api/api_ast.cpp
index ccc2cbf88..0ad056204 100644
--- a/src/api/api_ast.cpp
+++ b/src/api/api_ast.cpp
@@ -1079,6 +1079,12 @@ extern "C" {
             case OP_BSMUL_NO_OVFL: 
             case OP_BUMUL_NO_OVFL:
             case OP_BSMUL_NO_UDFL:
+            case OP_BSDIV_I:
+            case OP_BUDIV_I:
+            case OP_BSREM_I:
+            case OP_BUREM_I:
+            case OP_BSMOD_I:
+
                 return Z3_OP_UNINTERPRETED;
             default:
                 UNREACHABLE();
diff --git a/src/api/api_datalog.cpp b/src/api/api_datalog.cpp
index bf4752645..64b8b064e 100644
--- a/src/api/api_datalog.cpp
+++ b/src/api/api_datalog.cpp
@@ -29,107 +29,123 @@ Revision History:
 #include"dl_cmds.h"
 #include"cmd_context.h"
 #include"smt2parser.h"
+#include"dl_context.h"
+#include"dl_external_relation.h"
+#include"dl_decl_plugin.h"
 
 namespace api {
-    
-    fixedpoint_context::fixedpoint_context(ast_manager& m, smt_params& p) : 
-        m_state(0), 
-        m_reduce_app(0), 
-        m_reduce_assign(0), 
-        m_context(m, p),
-        m_trail(m) {}
-    
-    
-    void fixedpoint_context::set_state(void* state) {
-        SASSERT(!m_state);
-        m_state = state;
-        symbol name("datalog_relation");
-        ast_manager& m = m_context.get_manager();
-        if (!m.has_plugin(name)) {
-            m.register_plugin(name, alloc(datalog::dl_decl_plugin));
-        }        
-        datalog::rel_context* rel = m_context.get_rel_context();
-        if (rel) {
-            datalog::relation_manager& r = rel->get_rmanager();
-            r.register_plugin(alloc(datalog::external_relation_plugin, *this, r));
-        }
-    }        
-    
-    void fixedpoint_context::reduce(func_decl* f, unsigned num_args, expr * const* args, expr_ref& result) {
-        expr* r = 0;
-        if (m_reduce_app) {
-            m_reduce_app(m_state, f, num_args, args, &r);
-            result = r;
-            m_trail.push_back(f);
-            for (unsigned i = 0; i < num_args; ++i) {
-                m_trail.push_back(args[i]);
-            }
-            m_trail.push_back(r);
-        }
-        // allow fallthrough.
-        if (r == 0) {
+
+    class fixedpoint_context : public datalog::external_relation_context {
+        void *                       m_state;
+        reduce_app_callback_fptr     m_reduce_app;
+        reduce_assign_callback_fptr  m_reduce_assign;
+        datalog::context             m_context;    
+        ast_ref_vector               m_trail;        
+    public:
+        fixedpoint_context(ast_manager& m, smt_params& p): 
+            m_state(0), 
+            m_reduce_app(0), 
+            m_reduce_assign(0), 
+            m_context(m, p),
+            m_trail(m) {}
+
+        virtual ~fixedpoint_context() {}
+        family_id get_family_id() const { return const_cast<datalog::context&>(m_context).get_decl_util().get_family_id(); }
+        void set_state(void* state) {
+            SASSERT(!m_state);
+            m_state = state;
+            symbol name("datalog_relation");
             ast_manager& m = m_context.get_manager();
-            result = m.mk_app(f, num_args, args);
-        }
-    }
-    
-    // overwrite terms passed in outs vector with values computed by function.
-    void fixedpoint_context::reduce_assign(func_decl* f, unsigned num_args, expr * const* args, unsigned num_out, expr* const* outs) {
-        if (m_reduce_assign) {
-            m_trail.push_back(f);
-            for (unsigned i = 0; i < num_args; ++i) {
-                m_trail.push_back(args[i]);
+            if (!m.has_plugin(name)) {
+                m.register_plugin(name, alloc(datalog::dl_decl_plugin));
+            }        
+            datalog::rel_context* rel = m_context.get_rel_context();
+            if (rel) {
+                datalog::relation_manager& r = rel->get_rmanager();
+                r.register_plugin(alloc(datalog::external_relation_plugin, *this, r));
             }
-            m_reduce_assign(m_state, f, num_args, args, num_out, outs);
         }
-    }
-
-
-    void fixedpoint_context::add_rule(expr* rule, symbol const& name) {
-        m_context.add_rule(rule, name);
-    }   
-
-    void fixedpoint_context::update_rule(expr* rule, symbol const& name) {
-        m_context.update_rule(rule, name);
-    }   
-
-    void fixedpoint_context::add_table_fact(func_decl* r, unsigned num_args, unsigned args[]) {
-        m_context.add_table_fact(r, num_args, args);
-    }   
-
-    unsigned fixedpoint_context::get_num_levels(func_decl* pred) {
-        return m_context.get_num_levels(pred);
-    }
-
-    expr_ref fixedpoint_context::get_cover_delta(int level, func_decl* pred) {
-        return m_context.get_cover_delta(level, pred);
-    }
-
-    void fixedpoint_context::add_cover(int level, func_decl* pred, expr* predicate) {
-        m_context.add_cover(level, pred, predicate);
-    }
-
-    std::string fixedpoint_context::get_last_status() {
-        datalog::execution_result status = m_context.get_status();
-        switch(status) {
-        case datalog::INPUT_ERROR:
-            return "input error";        
-        case datalog::OK:
-            return "ok";
-        case datalog::TIMEOUT:            
-            return "timeout";
-        default:
-            UNREACHABLE();
-            return "unknown";
+        void set_reduce_app(reduce_app_callback_fptr f) { 
+            m_reduce_app = f; 
         }
-    } 
-
-    std::string fixedpoint_context::to_string(unsigned num_queries, expr*const* queries) {
-        std::stringstream str;
-        m_context.display_smt2(num_queries, queries, str);
-        return str.str();
-    } 
-
+        void set_reduce_assign(reduce_assign_callback_fptr f) { 
+            m_reduce_assign = f; 
+        }
+        virtual void reduce(func_decl* f, unsigned num_args, expr * const* args, expr_ref& result) {
+            expr* r = 0;
+            if (m_reduce_app) {
+                m_reduce_app(m_state, f, num_args, args, &r);
+                result = r;
+                m_trail.push_back(f);
+                for (unsigned i = 0; i < num_args; ++i) {
+                    m_trail.push_back(args[i]);
+                }
+                m_trail.push_back(r);
+            }
+            // allow fallthrough.
+            if (r == 0) {
+                ast_manager& m = m_context.get_manager();
+                result = m.mk_app(f, num_args, args);
+            }
+        }
+        virtual void reduce_assign(func_decl* f, unsigned num_args, expr * const* args, unsigned num_out, expr* const* outs) {
+            if (m_reduce_assign) {
+                m_trail.push_back(f);
+                for (unsigned i = 0; i < num_args; ++i) {
+                    m_trail.push_back(args[i]);
+                }
+                m_reduce_assign(m_state, f, num_args, args, num_out, outs);
+            }
+        }
+        datalog::context& ctx() { return m_context; }
+        void add_rule(expr* rule, symbol const& name) {
+            m_context.add_rule(rule, name);
+        }
+        void update_rule(expr* rule, symbol const& name) {
+            m_context.update_rule(rule, name);
+        }
+        void add_table_fact(func_decl* r, unsigned num_args, unsigned args[]) {
+            m_context.add_table_fact(r, num_args, args);
+        }
+        std::string get_last_status() {
+            datalog::execution_result status = m_context.get_status();
+            switch(status) {
+            case datalog::INPUT_ERROR:
+                return "input error";        
+            case datalog::OK:
+                return "ok";
+            case datalog::TIMEOUT:            
+                return "timeout";
+            case datalog::APPROX:
+                return "approximated";
+            default:
+                UNREACHABLE();
+                return "unknown";
+            }
+        }
+        std::string to_string(unsigned num_queries, expr*const* queries) {
+            std::stringstream str;
+            m_context.display_smt2(num_queries, queries, str);
+            return str.str();
+        }
+        void cancel() { 
+            m_context.cancel(); 
+        }
+        void reset_cancel() { 
+            m_context.reset_cancel(); 
+        }
+        unsigned get_num_levels(func_decl* pred) {
+            return m_context.get_num_levels(pred);
+        }
+        expr_ref get_cover_delta(int level, func_decl* pred) {
+            return m_context.get_cover_delta(level, pred);
+        }
+        void add_cover(int level, func_decl* pred, expr* predicate) {
+            m_context.add_cover(level, pred, predicate);
+        }
+        void collect_param_descrs(param_descrs & p) { m_context.collect_params(p); }
+        void updt_params(params_ref const& p) { m_context.updt_params(p); }
+    };         
 };
 
 extern "C" {
diff --git a/src/api/api_datalog.h b/src/api/api_datalog.h
index 51dbb72ec..f5bfada33 100644
--- a/src/api/api_datalog.h
+++ b/src/api/api_datalog.h
@@ -22,48 +22,14 @@ Revision History:
 #include"z3.h"
 #include"ast.h"
 #include"smt_params.h"
-#include"dl_external_relation.h"
-#include"dl_decl_plugin.h"
 #include"smt_kernel.h"
 #include"api_util.h"
-#include"dl_context.h"
 
 typedef void (*reduce_app_callback_fptr)(void*, func_decl*, unsigned, expr*const*, expr**);
 typedef void (*reduce_assign_callback_fptr)(void*, func_decl*, unsigned, expr*const*, unsigned, expr*const*);
 
 namespace api {
-    
-    class fixedpoint_context : public datalog::external_relation_context {
-        void *                       m_state;
-        reduce_app_callback_fptr     m_reduce_app;
-        reduce_assign_callback_fptr  m_reduce_assign;
-        datalog::context             m_context;    
-        ast_ref_vector               m_trail;        
-    public:
-        fixedpoint_context(ast_manager& m, smt_params& p);
-        virtual ~fixedpoint_context() {}
-        family_id get_family_id() const { return const_cast<datalog::context&>(m_context).get_decl_util().get_family_id(); }
-        void set_state(void* state);
-        void set_reduce_app(reduce_app_callback_fptr f) { m_reduce_app = f; }
-        void set_reduce_assign(reduce_assign_callback_fptr f) { m_reduce_assign = f; }
-        virtual void reduce(func_decl* f, unsigned num_args, expr * const* args, expr_ref& result);
-        virtual void reduce_assign(func_decl* f, unsigned num_args, expr * const* args, unsigned num_out, expr* const* outs);
-        datalog::context& ctx() { return m_context; }
-        void add_rule(expr* rule, symbol const& name);
-        void update_rule(expr* rule, symbol const& name);
-        void add_table_fact(func_decl* r, unsigned num_args, unsigned args[]);
-        std::string get_last_status();
-        std::string to_string(unsigned num_queries, expr*const* queries);
-        void cancel() { m_context.cancel(); }
-        void reset_cancel() { m_context.reset_cancel(); }
-
-        unsigned get_num_levels(func_decl* pred);
-        expr_ref get_cover_delta(int level, func_decl* pred);
-        void add_cover(int level, func_decl* pred, expr* predicate);
-        void collect_param_descrs(param_descrs & p) { m_context.collect_params(p); }
-        void updt_params(params_ref const& p) { m_context.updt_params(p); }
-
-    };
+    class fixedpoint_context;
 };
 
 
diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h
index a255c2d97..6f745d620 100644
--- a/src/api/c++/z3++.h
+++ b/src/api/c++/z3++.h
@@ -1305,7 +1305,7 @@ namespace z3 {
         expr as_expr() const {
             unsigned n = size();
             if (n == 0) 
-                return ctx().bool_val(false);
+                return ctx().bool_val(true);
             else if (n == 1)
                 return operator[](0);
             else {
diff --git a/src/ast/bv_decl_plugin.cpp b/src/ast/bv_decl_plugin.cpp
index 8b77244f9..f1c61619a 100644
--- a/src/ast/bv_decl_plugin.cpp
+++ b/src/ast/bv_decl_plugin.cpp
@@ -210,6 +210,10 @@ func_decl * bv_decl_plugin::mk_unary(ptr_vector<func_decl> & decls, decl_kind k,
 
 func_decl * bv_decl_plugin::mk_int2bv(unsigned bv_size, unsigned num_parameters, parameter const * parameters,
                                     unsigned arity, sort * const * domain) {
+    if (bv_size == 0) {
+        m_manager->raise_exception("bit-vector size must be greater than zero");
+    }
+
     force_ptr_array_size(m_int2bv, bv_size + 1);
 
     if (arity != 1) {
@@ -415,6 +419,9 @@ func_decl * bv_decl_plugin::mk_num_decl(unsigned num_parameters, parameter const
         return 0;
     }
     unsigned bv_size = parameters[1].get_int();
+    if (bv_size == 0) {
+        m_manager->raise_exception("bit-vector size must be greater than zero");
+    }
     // TODO: sign an error if the parameters[0] is out of range, that is, it is a value not in [0, 2^{bv_size})
     // This cannot be enforced now, since some Z3 modules try to generate these invalid numerals.
     // After SMT-COMP, I should find all offending modules.
diff --git a/src/muz_qe/dl_base.h b/src/muz_qe/dl_base.h
index 200ce2d83..f9078c2f2 100644
--- a/src/muz_qe/dl_base.h
+++ b/src/muz_qe/dl_base.h
@@ -776,7 +776,7 @@ namespace datalog {
         bool is_finite_product_relation() const { return m_special_type==ST_FINITE_PRODUCT_RELATION; }
         bool is_product_relation() const { return m_special_type==ST_PRODUCT_RELATION; }
         bool is_sieve_relation() const { return m_special_type==ST_SIEVE_RELATION; }
-       
+
         /**
            \brief If true, the relation can contain only one or zero elements.
 
@@ -805,6 +805,7 @@ namespace datalog {
         virtual void to_formula(expr_ref& fml) const = 0;
 
         bool from_table() const { return get_plugin().from_table(); }
+        virtual bool is_precise() const { return true; }
     };
 
     typedef ptr_vector<relation_base> relation_vector;
diff --git a/src/muz_qe/dl_bound_relation.cpp b/src/muz_qe/dl_bound_relation.cpp
index 0c76e8e1e..182046c1e 100644
--- a/src/muz_qe/dl_bound_relation.cpp
+++ b/src/muz_qe/dl_bound_relation.cpp
@@ -677,7 +677,7 @@ namespace datalog {
 
     void bound_relation::display_index(unsigned i, uint_set2 const& src, std::ostream & out) const {
         uint_set::iterator it = src.lt.begin(), end = src.lt.end();
-        out << i;
+        out << "#" << i;
         if (!src.lt.empty()) {
             out << " < ";
             for(; it != end; ++it) {
@@ -691,6 +691,9 @@ namespace datalog {
                 out << *it << " ";
             }
         }
+        if (src.lt.empty() && src.le.empty()) {
+            out << " < oo";
+        }
         out << "\n";
     }
 
diff --git a/src/muz_qe/dl_bound_relation.h b/src/muz_qe/dl_bound_relation.h
index 603717bd8..04479b3b6 100644
--- a/src/muz_qe/dl_bound_relation.h
+++ b/src/muz_qe/dl_bound_relation.h
@@ -69,6 +69,7 @@ namespace datalog {
                     unsigned joined_col_cnt, const unsigned * cols1, const unsigned * cols2, 
                     unsigned removed_col_cnt, const unsigned * removed_cols) { return 0; }
 
+
 #if 0
         virtual intersection_filter_fn * mk_filter_by_intersection_fn(
             const relation_base & t, 
@@ -138,6 +139,7 @@ namespace datalog {
 
         bool is_lt(unsigned i, unsigned j) const;
 
+        virtual bool is_precise() const { return false; }
 
     private:
         typedef uint_set2 T;
diff --git a/src/muz_qe/dl_cmds.cpp b/src/muz_qe/dl_cmds.cpp
index 693105e6e..dcdf3ebb4 100644
--- a/src/muz_qe/dl_cmds.cpp
+++ b/src/muz_qe/dl_cmds.cpp
@@ -260,7 +260,11 @@ public:
             case datalog::TIMEOUT:
                 ctx.regular_stream() << "timeout\n";
                 break;
-                
+               
+            case datalog::APPROX:
+                ctx.regular_stream() << "approximated relations\n";
+                break;
+
             case datalog::OK: 
                 UNREACHABLE();
                 break;
diff --git a/src/muz_qe/dl_context.cpp b/src/muz_qe/dl_context.cpp
index 2627cbbec..34513cc76 100644
--- a/src/muz_qe/dl_context.cpp
+++ b/src/muz_qe/dl_context.cpp
@@ -434,7 +434,10 @@ namespace datalog {
 
     void context::set_predicate_representation(func_decl * pred, unsigned relation_name_cnt, 
             symbol const * relation_names) {
-        if (m_rel && relation_name_cnt > 0) {
+        if (relation_name_cnt > 0) {
+            ensure_engine();
+        }
+        if (relation_name_cnt > 0 && m_rel) {
             m_rel->set_predicate_representation(pred, relation_name_cnt, relation_names);
         }
     }
diff --git a/src/muz_qe/dl_context.h b/src/muz_qe/dl_context.h
index c54f7d591..a3c7e583c 100644
--- a/src/muz_qe/dl_context.h
+++ b/src/muz_qe/dl_context.h
@@ -56,6 +56,7 @@ namespace datalog {
         TIMEOUT,
         MEMOUT,
         INPUT_ERROR,
+        APPROX,
         CANCELED
     };
 
diff --git a/src/muz_qe/dl_instruction.cpp b/src/muz_qe/dl_instruction.cpp
index df4736b8e..55327f55b 100644
--- a/src/muz_qe/dl_instruction.cpp
+++ b/src/muz_qe/dl_instruction.cpp
@@ -494,6 +494,7 @@ namespace datalog {
 
             relation_mutator_fn * fn;
             relation_base & r = *ctx.reg(m_reg);
+            TRACE("dl_verbose", r.display(tout <<"pre-filter-interpreted:\n"););
             if (!find_fn(r, fn)) {
                 fn = r.get_manager().mk_filter_interpreted_fn(r, m_cond);
                 if (!fn) {
@@ -507,7 +508,9 @@ namespace datalog {
 
             if (ctx.eager_emptiness_checking() && r.empty()) {
                 ctx.make_empty(m_reg);
-            }
+            }            
+            TRACE("dl_verbose", r.display(tout <<"post-filter-interpreted:\n"););
+
             return true;
         }
         virtual void display_head_impl(rel_context const& ctx, std::ostream & out) const {
@@ -545,6 +548,7 @@ namespace datalog {
 
             relation_transformer_fn * fn;
             relation_base & reg = *ctx.reg(m_src);
+            TRACE("dl_verbose", reg.display(tout <<"pre-filter-interpreted-and-project:\n"););
             if (!find_fn(reg, fn)) {
                 fn = reg.get_manager().mk_filter_interpreted_and_project_fn(reg, m_cond, m_cols.size(), m_cols.c_ptr());
                 if (!fn) {
@@ -560,6 +564,7 @@ namespace datalog {
             if (ctx.eager_emptiness_checking() && ctx.reg(m_res)->empty()) {
                 ctx.make_empty(m_res);
             }
+            TRACE("dl_verbose", reg.display(tout << "post-filter-interpreted-and-project:\n"););
             return true;
         }
 
diff --git a/src/muz_qe/dl_interval_relation.cpp b/src/muz_qe/dl_interval_relation.cpp
index 4c8171bc7..adc8cb760 100644
--- a/src/muz_qe/dl_interval_relation.cpp
+++ b/src/muz_qe/dl_interval_relation.cpp
@@ -48,7 +48,7 @@ namespace datalog {
         return alloc(interval_relation, *this, s, true);
     }
 
-    relation_base * interval_relation_plugin::mk_full(func_decl* p, const relation_signature & s) {
+    relation_base * interval_relation_plugin::mk_full(func_decl* p, const relation_signature & s) {        
         return alloc(interval_relation, *this, s, false);
     }
 
@@ -317,6 +317,7 @@ namespace datalog {
     interval_relation::interval_relation(interval_relation_plugin& p, relation_signature const& s, bool is_empty):
         vector_relation<interval>(p, s, is_empty, interval(p.dep())) 
     {
+        TRACE("interval_relation", tout << s.size() << "\n";);
     }    
 
     void interval_relation::add_fact(const relation_fact & f) {
diff --git a/src/muz_qe/dl_interval_relation.h b/src/muz_qe/dl_interval_relation.h
index 1a25f430f..685ef5c86 100644
--- a/src/muz_qe/dl_interval_relation.h
+++ b/src/muz_qe/dl_interval_relation.h
@@ -104,6 +104,7 @@ namespace datalog {
         interval_relation_plugin& get_plugin() const; 
 
         void filter_interpreted(app* cond);
+        virtual bool is_precise() const { return false; }
 
     private:
 
diff --git a/src/muz_qe/dl_mk_karr_invariants.cpp b/src/muz_qe/dl_mk_karr_invariants.cpp
index 4987a7e3d..e4e5a1ff8 100644
--- a/src/muz_qe/dl_mk_karr_invariants.cpp
+++ b/src/muz_qe/dl_mk_karr_invariants.cpp
@@ -355,6 +355,8 @@ namespace datalog {
             return m_empty;
         }
 
+        virtual bool is_precise() const { return false; }
+
         virtual void add_fact(const relation_fact & f) {
             SASSERT(m_empty);
             SASSERT(!m_basis_valid);
diff --git a/src/muz_qe/dl_mk_karr_invariants.h b/src/muz_qe/dl_mk_karr_invariants.h
index 3d993e60a..a86f726ef 100644
--- a/src/muz_qe/dl_mk_karr_invariants.h
+++ b/src/muz_qe/dl_mk_karr_invariants.h
@@ -123,6 +123,7 @@ namespace datalog {
         virtual relation_mutator_fn * mk_filter_equal_fn(const relation_base & t, const relation_element & value, 
             unsigned col);
         virtual relation_mutator_fn * mk_filter_interpreted_fn(const relation_base & t, app * condition);
+
     private:
         bool dualizeI(matrix& dst, matrix const& src);
         void dualizeH(matrix& dst, matrix const& src);
diff --git a/src/muz_qe/dl_mk_magic_symbolic.cpp b/src/muz_qe/dl_mk_magic_symbolic.cpp
index 2820ecaef..a06a573ad 100644
--- a/src/muz_qe/dl_mk_magic_symbolic.cpp
+++ b/src/muz_qe/dl_mk_magic_symbolic.cpp
@@ -95,11 +95,13 @@ namespace datalog {
                 neg.push_back(false);
             }
             new_rule = rm.mk(mk_ans(r.get_head()), tail.size(), tail.c_ptr(), neg.c_ptr(), r.name(), true);
+            result->add_rule(new_rule);                
             if (source.is_output_predicate(r.get_decl())) {
                 result->set_output_predicate(new_rule->get_decl());
+                new_rule = rm.mk(mk_query(r.get_head()), 0, 0, 0, r.name(), true);
+                result->add_rule(new_rule);
             }
 
-            result->add_rule(new_rule);                
             for (unsigned j = 0; j < utsz; ++j) {
                 new_rule = rm.mk(mk_query(r.get_tail(j)), tail.size()-utsz+j, tail.c_ptr(), neg.c_ptr(), r.name(), true);
                 result->add_rule(new_rule);
diff --git a/src/muz_qe/dl_product_relation.cpp b/src/muz_qe/dl_product_relation.cpp
index c10b5799a..48cd666e6 100644
--- a/src/muz_qe/dl_product_relation.cpp
+++ b/src/muz_qe/dl_product_relation.cpp
@@ -174,8 +174,7 @@ namespace datalog {
 
     relation_base * product_relation_plugin::mk_empty(const relation_signature & s, family_id kind) {
         rel_spec spec;
-        relation_signature sig_empty;
-        m_spec_store.get_relation_spec(sig_empty, kind, spec);
+        m_spec_store.get_relation_spec(s, kind, spec);
         relation_vector inner_rels;
         unsigned rel_cnt = spec.size();
         for(unsigned i=0; i<rel_cnt; i++) {
@@ -189,8 +188,7 @@ namespace datalog {
             return alloc(product_relation, *this, s);
         }
         rel_spec spec;
-        relation_signature sig_empty;
-        m_spec_store.get_relation_spec(sig_empty, kind, spec);
+        m_spec_store.get_relation_spec(s, kind, spec);
         relation_vector inner_rels;
         unsigned rel_cnt = spec.size();
         for(unsigned i=0; i<rel_cnt; i++) {
diff --git a/src/muz_qe/dl_product_relation.h b/src/muz_qe/dl_product_relation.h
index 91c2286a7..bf37a59d0 100644
--- a/src/muz_qe/dl_product_relation.h
+++ b/src/muz_qe/dl_product_relation.h
@@ -118,6 +118,7 @@ namespace datalog {
         friend class product_relation_plugin::filter_interpreted_fn;
 
 
+
         typedef product_relation_plugin::rel_spec rel_spec;
 
         /**
@@ -172,6 +173,15 @@ namespace datalog {
            false.
         */
         bool try_get_single_non_transparent(unsigned & idx) const;
+
+        virtual bool is_precise() const { 
+            for (unsigned i = 0; i < m_relations.size(); ++i) {
+                if (!m_relations[i]->is_precise()) {
+                    return false;
+                }
+            }
+            return true;
+        }
     };
         
 };
diff --git a/src/muz_qe/dl_relation_manager.cpp b/src/muz_qe/dl_relation_manager.cpp
index 812531e67..457ef28c0 100644
--- a/src/muz_qe/dl_relation_manager.cpp
+++ b/src/muz_qe/dl_relation_manager.cpp
@@ -80,12 +80,6 @@ namespace datalog {
         if(m_pred_kinds.find(pred, res)) {
             return res;
         }
-            //This is commented out as the favourite relation might not be suitable for all
-            //signatures. In the cases where it is suitable, it will be used anyway if we 
-            //now return null_family_id.
-        //else if (m_favourite_relation_plugin) {
-        //    return m_favourite_relation_plugin->get_kind();
-        //}
         else {
             return null_family_id;
         }
@@ -115,7 +109,7 @@ namespace datalog {
     void relation_manager::store_relation(func_decl * pred, relation_base * rel) {
         SASSERT(rel);
         relation_map::entry * e = m_relations.insert_if_not_there2(pred, 0);
-        if(e->get_data().m_value) {
+        if (e->get_data().m_value) {
             e->get_data().m_value->deallocate();
         }
         else {
@@ -142,7 +136,7 @@ namespace datalog {
         relation_map::iterator rend = m_relations.end();
         for(; rit!=rend; ++rit) {
             func_decl * pred = rit->m_key;
-            if(!preds.contains(pred)) {
+            if (!preds.contains(pred)) {
                 to_remove.insert(pred);
             }
         }
@@ -152,7 +146,7 @@ namespace datalog {
         for(; pit!=pend; ++pit) {
             func_decl * pred = *pit;
             relation_base * rel;
-            TRUSTME( m_relations.find(pred, rel) );
+            VERIFY( m_relations.find(pred, rel) );
             rel->deallocate();
             m_relations.remove(pred);
             get_context().get_manager().dec_ref(pred);
@@ -278,7 +272,7 @@ namespace datalog {
         SASSERT(kind>=0);
         SASSERT(kind<m_next_relation_fid);
         relation_plugin * res;
-        TRUSTME(m_kind2plugin.find(kind, res));
+        VERIFY(m_kind2plugin.find(kind, res));
         return *res;
     }
 
@@ -295,7 +289,7 @@ namespace datalog {
 
     table_relation_plugin & relation_manager::get_table_relation_plugin(table_plugin & tp) {
         table_relation_plugin * res;
-        TRUSTME( m_table_relation_plugins.find(&tp, res) );
+        VERIFY( m_table_relation_plugins.find(&tp, res) );
         return *res;
     }
 
@@ -388,7 +382,7 @@ namespace datalog {
     void relation_manager::relation_to_table(const relation_sort & sort, const relation_element & from, 
             table_element & to) {
         SASSERT(from->get_num_args()==0);
-        TRUSTME(get_context().get_decl_util().is_numeral_ext(from, to));
+        VERIFY(get_context().get_decl_util().is_numeral_ext(from, to));
     }
 
     void relation_manager::table_to_relation(const relation_sort & sort, const table_element & from, 
diff --git a/src/muz_qe/pdr_context.cpp b/src/muz_qe/pdr_context.cpp
index 6f81d93d8..034bb236a 100644
--- a/src/muz_qe/pdr_context.cpp
+++ b/src/muz_qe/pdr_context.cpp
@@ -1556,22 +1556,23 @@ namespace pdr {
         if (use_mc) {
             m_core_generalizers.push_back(alloc(core_multi_generalizer, *this, 0));
         }
-        if (m_params.use_farkas() && !classify.is_bool()) {
+        if (!classify.is_bool()) {
             m.toggle_proof_mode(PGM_FINE);
             m_fparams.m_arith_bound_prop = BP_NONE;
             m_fparams.m_arith_auto_config_simplex = true;
             m_fparams.m_arith_propagate_eqs = false;
             m_fparams.m_arith_eager_eq_axioms = false;
-            if (classify.is_dl()) {
-                m_fparams.m_arith_mode = AS_DIFF_LOGIC;
-                m_fparams.m_arith_expand_eqs = true;
+            if (m_params.use_utvpi() && !m_params.use_convex_hull_generalizer()) {
+                if (classify.is_dl()) {
+                    m_fparams.m_arith_mode = AS_DIFF_LOGIC;
+                    m_fparams.m_arith_expand_eqs = true;
+                }
+                else if (classify.is_utvpi()) {
+                    IF_VERBOSE(1, verbose_stream() << "UTVPI\n";);
+                    m_fparams.m_arith_mode = AS_UTVPI;
+                    m_fparams.m_arith_expand_eqs = true;                
+                }
             }
-            else if (classify.is_utvpi() && m_params.use_utvpi()) {
-                IF_VERBOSE(1, verbose_stream() << "UTVPI\n";);
-                m_fparams.m_arith_mode = AS_UTVPI;
-                m_fparams.m_arith_expand_eqs = true;                
-            }
-
         }
         if (m_params.use_convex_hull_generalizer()) {
             m_core_generalizers.push_back(alloc(core_convex_hull_generalizer, *this));
@@ -1800,6 +1801,7 @@ namespace pdr {
             m_expanded_lvl = n.level();
         }
 
+        n.pt().set_use_farkas(m_params.use_farkas());
         if (n.pt().is_reachable(n.state())) {
             TRACE("pdr", tout << "reachable\n";);
             close_node(n);
diff --git a/src/muz_qe/pdr_context.h b/src/muz_qe/pdr_context.h
index 1785991c6..4c26fc1ac 100644
--- a/src/muz_qe/pdr_context.h
+++ b/src/muz_qe/pdr_context.h
@@ -166,6 +166,8 @@ namespace pdr {
 
         prop_solver& get_solver() { return m_solver; }
 
+        void set_use_farkas(bool f) { get_solver().set_use_farkas(f); }
+
     };
 
 
diff --git a/src/muz_qe/pdr_generalizers.cpp b/src/muz_qe/pdr_generalizers.cpp
index 5e777bf7e..5e928ff45 100644
--- a/src/muz_qe/pdr_generalizers.cpp
+++ b/src/muz_qe/pdr_generalizers.cpp
@@ -158,7 +158,7 @@ namespace pdr {
     }
 
     void core_convex_hull_generalizer::operator()(model_node& n, expr_ref_vector& core, bool& uses_level) {
-        method2(n, core, uses_level);
+        method1(n, core, uses_level);
     }
 
     // use the entire region as starting point for generalization.
@@ -196,6 +196,7 @@ namespace pdr {
 
                   );
             model_node nd(0, state, n.pt(), n.level());
+            n.pt().set_use_farkas(true);
             if (l_false == n.pt().is_reachable(nd, &conv2, uses_level)) {
                 TRACE("pdr", 
                       tout << mk_pp(state, m) << "\n";
@@ -260,6 +261,7 @@ namespace pdr {
             expr_ref state = pm.mk_and(conv1);
             TRACE("pdr", tout << "Try:\n" << mk_pp(state, m) << "\n";);
             model_node nd(0, state, n.pt(), n.level());
+            n.pt().set_use_farkas(true);
             if (l_false == n.pt().is_reachable(nd, &conv2, uses_level)) {
                 IF_VERBOSE(0,
                            verbose_stream() << mk_pp(state, m) << "\n";
diff --git a/src/muz_qe/pdr_prop_solver.cpp b/src/muz_qe/pdr_prop_solver.cpp
index e3cd0d9c5..c7f0bfbc3 100644
--- a/src/muz_qe/pdr_prop_solver.cpp
+++ b/src/muz_qe/pdr_prop_solver.cpp
@@ -237,6 +237,7 @@ namespace pdr {
         m_proxies(m),
         m_core(0),
         m_subset_based_core(false),
+        m_use_farkas(false),
         m_in_level(false)
     {
         m_ctx->assert_expr(m_pm.get_background());
@@ -328,7 +329,11 @@ namespace pdr {
             }
         }
 
-        if (result == l_false && m_core && m.proofs_enabled() && !m_subset_based_core) {
+        if (result == l_false  && 
+            m_core && 
+            m.proofs_enabled() && 
+            m_use_farkas    && 
+            !m_subset_based_core) {
             extract_theory_core(safe);
         }
         else if (result == l_false && m_core) {
diff --git a/src/muz_qe/pdr_prop_solver.h b/src/muz_qe/pdr_prop_solver.h
index 165a37845..7712573ee 100644
--- a/src/muz_qe/pdr_prop_solver.h
+++ b/src/muz_qe/pdr_prop_solver.h
@@ -50,6 +50,7 @@ namespace pdr {
         model_ref*          m_model;
         bool                m_subset_based_core;
         bool                m_assumes_level;
+        bool                m_use_farkas;
         func_decl_set       m_aux_symbols;      
         bool                m_in_level;         
         unsigned            m_current_level;    // set when m_in_level
@@ -97,6 +98,8 @@ namespace pdr {
             ~scoped_level() { m_lev = false; }
         };
         
+        void set_use_farkas(bool f) { m_use_farkas = f; }
+        
         void add_formula(expr * form);
         void add_level_formula(expr * form, unsigned level);
                 
diff --git a/src/muz_qe/rel_context.cpp b/src/muz_qe/rel_context.cpp
index 4ebcbf2fd..ce1b30b88 100644
--- a/src/muz_qe/rel_context.cpp
+++ b/src/muz_qe/rel_context.cpp
@@ -213,17 +213,25 @@ namespace datalog {
             expr_ref_vector ans(m);
             expr_ref e(m);
             bool some_non_empty = num_rels == 0;
+            bool is_approx = false;
             for (unsigned i = 0; i < num_rels; ++i) {
                 relation_base& rel = get_relation(rels[i]);
                 if (!rel.empty()) {
                     some_non_empty = true;
                 }
+                if (!rel.is_precise()) {
+                    is_approx = true;
+                }
                 rel.to_formula(e);
                 ans.push_back(e);
             }
             SASSERT(!m_last_result_relation);
             if (some_non_empty) {
                 m_answer = m.mk_and(ans.size(), ans.c_ptr());
+                if (is_approx) {
+                    res = l_undef;
+                    m_context.set_status(APPROX);
+                }
             }
             else {
                 m_answer = m.mk_false();
@@ -278,6 +286,10 @@ namespace datalog {
             }
             else {
                 m_last_result_relation->to_formula(m_answer);
+                if (!m_last_result_relation->is_precise()) {
+                    m_context.set_status(APPROX);
+                    res = l_undef;
+                }
             }
         }
         
@@ -365,8 +377,15 @@ namespace datalog {
     void rel_context::set_predicate_representation(func_decl * pred, unsigned relation_name_cnt, 
                                                    symbol const * relation_names) {
 
-        relation_manager & rmgr = get_rmanager();
+        TRACE("dl", 
+              tout << pred->get_name() << ": ";
+              for (unsigned i = 0; i < relation_name_cnt; ++i) {
+                  tout << relation_names[i] << " ";
+              }
+              tout << "\n";
+              );
 
+        relation_manager & rmgr = get_rmanager();
         family_id target_kind = null_family_id;
         switch (relation_name_cnt) {
         case 0: 
@@ -386,7 +405,7 @@ namespace datalog {
             }
             else {
                 relation_signature rel_sig;
-                //rmgr.from_predicate(pred, rel_sig);
+                rmgr.from_predicate(pred, rel_sig);
                 product_relation_plugin & prod_plugin = product_relation_plugin::get_plugin(rmgr);
                 rel_kind = prod_plugin.get_relation_kind(rel_sig, rel_kinds);
             }