Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable

scripts/mk_util.py

@@ -1084,6 +1084,10 @@ class JavaDLLComponent(Component):
             mk_dir(os.path.join(dist_path, 'bin'))
             shutil.copy('%s.jar' % os.path.join(build_path, self.package_name),
                         '%s.jar' % os.path.join(dist_path, 'bin', self.package_name))
+            shutil.copy(os.path.join(build_path, 'libz3java.dll'), 
+                        os.path.join(dist_path, 'bin', 'libz3java.dll'))
+            shutil.copy(os.path.join(build_path, 'libz3java.lib'),
+                        os.path.join(dist_path, 'bin', 'libz3java.lib'))
 
 class ExampleComponent(Component):
     def __init__(self, name, path):

scripts/update_api.py

@@ -395,8 +395,7 @@ def mk_dotnet():
     dotnet.write('        public delegate void Z3_error_handler(Z3_context c, Z3_error_code e);\n\n')
     dotnet.write('        public unsafe class LIB\n')
     dotnet.write('        {\n')
-    dotnet.write('           '
+    dotnet.write('            const string Z3_DLL_NAME = \"libz3.dll\";\n'
-                 '            const string Z3_DLL_NAME = \"libz3.dll\";\n'
                  '            \n');
     dotnet.write('            [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]\n')
     dotnet.write('            public extern static void Z3_set_error_handler(Z3_context a0, Z3_error_handler a1);\n\n')
@@ -420,7 +419,8 @@ def mk_dotnet():
     dotnet.write('        }\n')
 
 
-DotnetUnwrapped = [ 'Z3_del_context' ]
+NULLWrapped = [ 'Z3_mk_context', 'Z3_mk_context_rc' ]
+Unwrapped = [ 'Z3_del_context' ]
 
 def mk_dotnet_wrappers():
     global Type2Str
@@ -469,7 +469,11 @@ def mk_dotnet_wrappers():
             dotnet.write('a%d' % i)
             i = i + 1
         dotnet.write(');\n');
-        if name not in DotnetUnwrapped:
+        if name not in Unwrapped:
+            if name in NULLWrapped:
+                dotnet.write("            if (r == IntPtr.Zero)\n")
+                dotnet.write("                throw new Z3Exception(\"Object allocation failed.\");\n")
+            else:
                 if len(params) > 0 and param_type(params[0]) == CONTEXT:
                     dotnet.write("            Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);\n")
                     dotnet.write("            if (err != Z3_error_code.Z3_OK)\n")
@@ -550,7 +554,7 @@ def mk_java():
             java_native.write('%s a%d' % (param2java(param), i))
             i = i + 1
         java_native.write(')')
-        if len(params) > 0 and param_type(params[0]) == CONTEXT:
+        if (len(params) > 0 and param_type(params[0]) == CONTEXT) or name in NULLWrapped:
             java_native.write(' throws Z3Exception')
         java_native.write('\n')
         java_native.write('  {\n')
@@ -568,6 +572,11 @@ def mk_java():
             java_native.write('a%d' % i)
             i = i + 1
         java_native.write(');\n')
+        if name not in Unwrapped:
+            if name in NULLWrapped:
+                java_native.write("      if (res == 0)\n")
+                java_native.write("          throw new Z3Exception(\"Object allocation failed.\");\n")
+            else:
                 if len(params) > 0 and param_type(params[0]) == CONTEXT:
                     java_native.write('      Z3_error_code err = Z3_error_code.fromInt(INTERNALgetErrorCode(a0));\n')
                     java_native.write('      if (err != Z3_error_code.Z3_OK)\n')

src/api/api_context.cpp

@@ -419,17 +419,21 @@ namespace api {
 extern "C" {
     
     Z3_context Z3_API Z3_mk_context(Z3_config c) {
+        Z3_TRY;
         LOG_Z3_mk_context(c);
         memory::initialize(UINT_MAX);
         Z3_context r = reinterpret_cast<Z3_context>(alloc(api::context, reinterpret_cast<context_params*>(c), false));
         RETURN_Z3(r);
+        Z3_CATCH_RETURN_NO_HANDLE(0);
     }
 
     Z3_context Z3_API Z3_mk_context_rc(Z3_config c) {
+        Z3_TRY;
         LOG_Z3_mk_context_rc(c);
         memory::initialize(UINT_MAX);
         Z3_context r = reinterpret_cast<Z3_context>(alloc(api::context, reinterpret_cast<context_params*>(c), true));
         RETURN_Z3(r);
+        Z3_CATCH_RETURN_NO_HANDLE(0);
     }
 
     void Z3_API Z3_del_context(Z3_context c) {

src/api/api_util.h

@@ -26,6 +26,7 @@ Revision History:
 #define Z3_CATCH_CORE(CODE) } catch (z3_exception & ex) { mk_c(c)->handle_exception(ex); CODE }
 #define Z3_CATCH Z3_CATCH_CORE(return;)
 #define Z3_CATCH_RETURN(VAL) Z3_CATCH_CORE(return VAL;)
+#define Z3_CATCH_RETURN_NO_HANDLE(VAL) } catch (z3_exception &) { return VAL; }
 
 #define CHECK_REF_COUNT(a) (reinterpret_cast<ast const*>(a)->get_ref_count() > 0)
 #define VALIDATE(a) SASSERT(!a || CHECK_REF_COUNT(a))

src/api/java/Context.java

@@ -3053,10 +3053,10 @@ public class Context extends IDisposable
                 // OK.
             }
             m_ctx = 0;
-        } else
+        } 
-            /* re-queue the finalizer */
+        /*
-            /* BUG: DRQ's need to be taken over too! */
+        else
-            new Context(m_ctx, m_refCount);
+            CMW: re-queue the finalizer? */
     }
 
     /**

src/ast/arith_decl_plugin.cpp

@@ -492,13 +492,6 @@ static bool is_const_op(decl_kind k) {
     
 func_decl * arith_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters, 
                                           unsigned arity, sort * const * domain, sort * range) {
-    if (range != 0) {
-        if (is_sort_of(range, m_family_id, REAL_SORT) || is_sort_of(range, m_family_id, INT_SORT))
-            m_manager->raise_exception("unneeded disambiguation");
-        else
-            m_manager->raise_exception("incorrect disambiguation");
-        return 0;
-    }
     if (k == OP_NUM)
         return mk_num_decl(num_parameters, parameters, arity);
     if (arity == 0 && !is_const_op(k)) {
@@ -516,13 +509,6 @@ func_decl * arith_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters
 
 func_decl * arith_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters, 
                                           unsigned num_args, expr * const * args, sort * range) {
-    if (range != 0) {
-        if (is_sort_of(range, m_family_id, REAL_SORT) || is_sort_of(range, m_family_id, INT_SORT))
-            m_manager->raise_exception("unneeded disambiguation");
-        else
-            m_manager->raise_exception("incorrect disambiguation");
-        return 0;
-    }
     if (k == OP_NUM)
         return mk_num_decl(num_parameters, parameters, num_args);
     if (num_args == 0 && !is_const_op(k)) {

src/ast/ast.cpp

@@ -1010,13 +1010,6 @@ func_decl * basic_decl_plugin::mk_ite_decl(sort * s) {
 
 func_decl * basic_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters,
                                           unsigned arity, sort * const * domain, sort * range) {
-    if (range != 0) {
-        if (is_sort_of(range, m_family_id, BOOL_SORT))
-            m_manager->raise_exception("unneeded disambiguation");
-        else
-            m_manager->raise_exception("incorrect disambiguation");
-        return 0;
-    }
     switch (static_cast<basic_op_kind>(k)) {
     case OP_TRUE:    return m_true_decl;
     case OP_FALSE:   return m_false_decl;
@@ -1052,13 +1045,6 @@ func_decl * basic_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters
 
 func_decl * basic_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters,
                                             unsigned num_args, expr * const * args, sort * range) {
-    if (range != 0) {
-        if (is_sort_of(range, m_family_id, BOOL_SORT))
-            m_manager->raise_exception("unneeded disambiguation");
-        else
-            m_manager->raise_exception("incorrect disambiguation");
-        return 0;
-    }
     switch (static_cast<basic_op_kind>(k)) {
     case OP_TRUE:    return m_true_decl;
     case OP_FALSE:   return m_false_decl;

src/ast/ast_smt_pp.cpp

@@ -537,7 +537,7 @@ class smt_printer {
     }
 
     void print_bound(symbol const& name) {
-        if (name.is_numerical() || '?' != name.bare_str()[0]) {
+        if (!m_is_smt2 && (name.is_numerical() || '?' != name.bare_str()[0])) {
             m_out << "?";
         }
         m_out << name;
@@ -642,9 +642,11 @@ class smt_printer {
             m_out << m_var_names[m_num_var_names - idx - 1];
         }
         else {
+            if (!m_is_smt2) {
                 m_out << "?" << idx;
             }
         }
+    }
 
     void pp_marked_expr(expr* n) {
         if (m_mark.is_marked(n)) {

src/ast/bv_decl_plugin.cpp

@@ -461,13 +461,6 @@ func_decl * bv_decl_plugin::mk_mkbv(unsigned arity, sort * const * domain) {
 
 func_decl * bv_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters,
                                          unsigned arity, sort * const * domain, sort * range) {
-    if (range != 0) {
-        if (is_sort_of(range, m_family_id, BV_SORT))
-            m_manager->raise_exception("unneeded disambiguation");
-        else
-            m_manager->raise_exception("incorrect disambiguation");
-        return 0;
-    }
     int bv_size;
     if (k == OP_INT2BV && get_int2bv_size(num_parameters, parameters, bv_size)) {
         // bv_size is filled in.
@@ -566,13 +559,6 @@ func_decl * bv_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, p
 
 func_decl * bv_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters, 
                                          unsigned num_args, expr * const * args, sort * range) {
-    if (range != 0) {
-        if (is_sort_of(range, m_family_id, BV_SORT))
-            m_manager->raise_exception("unneeded disambiguation");
-        else
-            m_manager->raise_exception("incorrect disambiguation");
-        return 0;
-    }
     int bv_size;
     if (k == OP_INT2BV && get_int2bv_size(num_parameters, parameters, bv_size)) {
         // bv_size is filled in.

src/muz_qe/dl_compiler.cpp

@@ -87,12 +87,12 @@ namespace datalog {
         acc.push_back(instruction::mk_clone(src, result));
     }
 
-    void compiler::make_union(reg_idx src, reg_idx tgt, reg_idx delta, bool widening, 
+    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(widening) {
+        if (use_widening) {
             acc.push_back(instruction::mk_widen(src, tgt, delta));
         }
         else {
@@ -129,8 +129,7 @@ namespace datalog {
         func_decl_set::iterator pend = preds.end();
         for(; pit!=pend; ++pit) {
             func_decl * pred = *pit;
-            reg_idx reg;
+            reg_idx reg = m_pred_regs.find(pred);
-            TRUSTME( m_pred_regs.find(pred, reg) );
 
             SASSERT(!regs.contains(pred));
             relation_signature sig = m_reg_signatures[reg];
@@ -576,8 +575,7 @@ namespace datalog {
             }
             SASSERT(t_cols.size()==neg_cols.size());
 
-            reg_idx neg_reg;
+            reg_idx neg_reg = m_pred_regs.find(neg_pred);
-            TRUSTME( m_pred_regs.find(neg_pred, neg_reg) );
             acc.push_back(instruction::mk_filter_by_negation(filtered_res, neg_reg, t_cols.size(),
                 t_cols.c_ptr(), neg_cols.c_ptr()));
         }
@@ -762,15 +760,13 @@ namespace datalog {
         typedef svector<tail_delta_info> tail_delta_infos;
 
         unsigned rule_len = r->get_uninterpreted_tail_size();
-        reg_idx head_reg;
+        reg_idx head_reg = m_pred_regs.find(r->get_head()->get_decl());
-        TRUSTME( m_pred_regs.find(r->get_head()->get_decl(), head_reg) );
 
         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;
+            reg_idx tail_reg = m_pred_regs.find(tail_pred);
-            TRUSTME( m_pred_regs.find(tail_pred, tail_reg) );
             tail_regs.push_back(tail_reg);
 
             if(input_deltas && !all_or_nothing_deltas()) {
@@ -858,7 +854,7 @@ namespace datalog {
         rule_dependencies deps(m_rule_set.get_dependencies());
         deps.restrict(preds);
         cycle_breaker(deps, global_deltas)();
-        TRUSTME( deps.sort_deps(ordered_preds) );
+        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
@@ -903,8 +899,7 @@ namespace datalog {
         for(; gdit!=gend; ++gdit) {
             func_decl * pred = gdit->m_key;
             reg_idx head_reg = gdit->m_value;
-            reg_idx tail_reg;
+            reg_idx tail_reg = global_tail_deltas.find(pred);
-            TRUSTME( global_tail_deltas.find(pred, tail_reg) );
             acc.push_back(instruction::mk_move(head_reg, tail_reg));
         }
         //empty local deltas
@@ -985,50 +980,11 @@ namespace datalog {
         //generate code for the initial run
         compile_preds(preds_vector, empty_func_decl_set, input_deltas, d_global_src, acc);
 
-        if(!compile_with_widening()) {
+        if (compile_with_widening()) {
-            compile_loop(preds_vector, empty_func_decl_set, d_global_tgt, d_global_src,
+            compile_loop(preds_vector, global_deltas, d_global_tgt, d_global_src, d_local, acc);
-                d_local, acc);
         }
         else {
-            //do the part where we zero the global predicates and run the loop saturation loop again
+            compile_loop(preds_vector, empty_func_decl_set, d_global_tgt, d_global_src, d_local, acc);
-            if(global_deltas.size()<head_preds.size()) {
-
-                pred2idx globals_backup;
-                get_fresh_registers(global_deltas, globals_backup); //these actually are not deltas
-
-                {
-                    //make backup copy of relations that will be widened
-                    func_decl_set::iterator it = global_deltas.begin();
-                    func_decl_set::iterator end = global_deltas.end();
-                    for(; it!=end; ++it) {
-                        reg_idx rel_idx;
-                        TRUSTME( m_pred_regs.find(*it, rel_idx) );
-                        reg_idx backup_idx;
-                        TRUSTME( globals_backup.find(*it, backup_idx) );
-
-                        make_clone(rel_idx, backup_idx, acc);
-                    }
-                }
-
-                compile_loop(preds_vector, global_deltas, d_global_tgt, d_global_src,
-                    d_local, acc);
-
-                {
-                    //restore the original values of widened relations before we rerun the loop
-                    func_decl_set::iterator it = global_deltas.begin();
-                    func_decl_set::iterator end = global_deltas.end();
-                    for(; it!=end; ++it) {
-                        reg_idx rel_idx;
-                        TRUSTME( m_pred_regs.find(*it, rel_idx) );
-                        reg_idx backup_idx;
-                        TRUSTME( globals_backup.find(*it, backup_idx) );
-
-                        acc.push_back(instruction::mk_move(backup_idx, rel_idx));
-                    }
-                }
-            }
-            compile_loop(preds_vector, global_deltas, d_global_tgt, d_global_src,
-                d_local, acc);
         }
 
 

src/muz_qe/dl_mk_array_blast.cpp

@@ -50,6 +50,94 @@ namespace datalog {
         return false;
     }
     
+    bool mk_array_blast::ackermanize(expr_ref& body, expr_ref& head) {
+        expr_ref_vector conjs(m);
+        flatten_and(body, conjs);
+        defs_t defs;
+        expr_safe_replace sub(m);
+        ptr_vector<expr> todo;
+        todo.push_back(head);
+        for (unsigned i = 0; i < conjs.size(); ++i) {
+            expr* e = conjs[i].get();
+            expr* x, *y;
+            if (m.is_eq(e, x, y) || m.is_iff(e, x, y)) {
+                if (a.is_select(y)) {
+                    std::swap(x,y);
+                }
+                if (a.is_select(x) && is_var(y)) {
+                    //
+                    // For the Ackermann reduction we would like the arrays 
+                    // to be variables, so that variables can be 
+                    // assumed to represent difference (alias) 
+                    // classes.
+                    // 
+                    if (!is_var(to_app(x)->get_arg(0))) {
+                        return false;
+                    }
+                    sub.insert(x, y);
+                    defs.insert(to_app(x), to_var(y));
+                }
+            }
+            todo.push_back(e);
+        }
+        // now check that all occurrences of select have been covered.
+        ast_mark mark;
+        while (!todo.empty()) {
+            expr* e = todo.back();
+            todo.pop_back();
+            if (mark.is_marked(e)) {
+                continue;
+            }
+            mark.mark(e, true);
+            if (is_var(e)) {
+                continue;
+            }
+            if (!is_app(e)) {
+                return false;
+            }
+            app* ap = to_app(e);
+            if (a.is_select(e) && !defs.contains(ap)) {
+                return false;
+            }
+            for (unsigned i = 0; i < ap->get_num_args(); ++i) {
+                todo.push_back(ap->get_arg(i));
+            }
+        }
+        sub(body);
+        sub(head);
+        conjs.reset();
+
+        // perform the Ackermann reduction by creating implications
+        // i1 = i2 => val1 = val2 for each equality pair:
+        // (= val1 (select a_i i1))
+        // (= val2 (select a_i i2))
+        defs_t::iterator it1 = defs.begin(), end = defs.end();
+        for (; it1 != end; ++it1) {
+            app* a1 = it1->m_key;
+            var* v1 = it1->m_value;
+            defs_t::iterator it2 = it1;
+            ++it2;
+            for (; it2 != end; ++it2) {
+                app* a2 = it2->m_key;
+                var* v2 = it2->m_value;
+                if (a1->get_arg(0) != a2->get_arg(0)) {
+                    continue;
+                }
+                expr_ref_vector eqs(m);
+                for (unsigned j = 1; j < a1->get_num_args(); ++j) {
+                    eqs.push_back(m.mk_eq(a1->get_arg(j), a2->get_arg(j)));
+                }
+                conjs.push_back(m.mk_implies(m.mk_and(eqs.size(), eqs.c_ptr()), m.mk_eq(v1, v2)));
+            }
+        }
+        if (!conjs.empty()) {
+            conjs.push_back(body);
+            body = m.mk_and(conjs.size(), conjs.c_ptr());
+        }
+        m_rewriter(body);   
+        return true;
+    }
+
     bool mk_array_blast::blast(rule& r, rule_set& rules) {
         unsigned utsz = r.get_uninterpreted_tail_size();
         unsigned tsz = r.get_tail_size();
@@ -92,10 +180,6 @@ namespace datalog {
                 new_conjs.push_back(tmp);
             }
         }
-        if (!inserted && !change) {
-            rules.add_rule(&r);
-            return false;
-        }
         
         rule_ref_vector new_rules(rm);
         expr_ref fml1(m), fml2(m), body(m), head(m);
@@ -106,11 +190,17 @@ namespace datalog {
         m_rewriter(body);
         sub(head);
         m_rewriter(head);
+        change = ackermanize(body, head) || change;
+        if (!inserted && !change) {
+            rules.add_rule(&r);
+            return false;
+        }
+
         fml2 = m.mk_implies(body, head);
         rm.mk_rule(fml2, new_rules, r.name());
         SASSERT(new_rules.size() == 1);
 
-        TRACE("dl", tout << "new body " << mk_pp(fml2, m) << "\n";);
+        TRACE("dl", new_rules[0]->display(m_ctx, tout << "new rule\n"););
         
         rules.add_rule(new_rules[0].get());
         if (m_pc) {

src/muz_qe/dl_mk_array_blast.h

@@ -39,10 +39,14 @@ namespace datalog {
         th_rewriter     m_rewriter;
         equiv_proof_converter* m_pc;
 
+        typedef obj_map<app, var*> defs_t;
+
         bool blast(rule& r, rule_set& new_rules);
 
         bool is_store_def(expr* e, expr*& x, expr*& y);
 
+        bool ackermanize(expr_ref& body, expr_ref& head);
+
     public:
         /**
            \brief Create rule transformer that extracts universal quantifiers (over recursive predicates).

src/muz_qe/fixedpoint_params.pyg

@@ -44,6 +44,7 @@ def_module_params('fixedpoint',
                           ('coalesce_rules', BOOL, False, "BMC: coalesce rules"),
                           ('use_multicore_generalizer', BOOL, False, "PDR: extract multiple cores for blocking states"),
                           ('use_inductive_generalizer', BOOL, True, "PDR: generalize lemmas using induction strengthening"),
+                          ('use_arith_inductive_generalizer', BOOL, False, "PDR: generalize lemmas using arithmetic heuristics for induction strengthening"),
                           ('cache_mode', UINT, 0, "PDR: use no (0), symbolic (1) or explicit cache (2) for model search"),
                           ('inductive_reachability_check', BOOL, False, "PDR: assume negation of the cube on the previous level when "
                                                                         "checking for reachability (not only during cube weakening)"),

src/muz_qe/pdr_context.cpp

@@ -53,6 +53,20 @@ namespace pdr {
 
     static unsigned next_level(unsigned lvl) { return is_infty_level(lvl)?lvl:(lvl+1); }
 
+    struct pp_level {
+        unsigned m_level;
+        pp_level(unsigned l): m_level(l) {}        
+    };
+
+    static std::ostream& operator<<(std::ostream& out, pp_level const& p) {
+        if (is_infty_level(p.m_level)) {
+            return out << "oo";
+        }
+        else {
+            return out << p.m_level;
+        }
+    }
+    
     // ----------------
     // pred_tansformer
 
@@ -263,7 +277,7 @@ namespace pdr {
             else if (is_invariant(tgt_level, curr, false, assumes_level)) {
                 
                 add_property(curr, assumes_level?tgt_level:infty_level);
-                TRACE("pdr", tout << "is invariant: "<< tgt_level << " " << mk_pp(curr, m) << "\n";);              
+                TRACE("pdr", tout << "is invariant: "<< pp_level(tgt_level) << " " << mk_pp(curr, m) << "\n";);              
                 src[i] = src.back();
                 src.pop_back();
                 ++m_stats.m_num_propagations;
@@ -273,14 +287,7 @@ namespace pdr {
                 ++i;
             }
         }        
-        IF_VERBOSE(2, verbose_stream() << "propagate: ";
+        IF_VERBOSE(3, verbose_stream() << "propagate: " << pp_level(src_level) << "\n";
-                   if (is_infty_level(src_level)) {
-                       verbose_stream() << "infty"; 
-                   }
-                   else {
-                       verbose_stream() << src_level;
-                   }
-                   verbose_stream() << "\n";
                    for (unsigned i = 0; i < src.size(); ++i) {
                        verbose_stream() << mk_pp(src[i].get(), m) << "\n";   
                    });
@@ -304,14 +311,14 @@ namespace pdr {
         ensure_level(lvl);        
         unsigned old_level;
         if (!m_prop2level.find(lemma, old_level) || old_level < lvl) {
-            TRACE("pdr", tout << "property1: " << lvl << " " << head()->get_name() << " " << mk_pp(lemma, m) << "\n";);
+            TRACE("pdr", tout << "property1: " << pp_level(lvl) << " " << head()->get_name() << " " << mk_pp(lemma, m) << "\n";);
             m_levels[lvl].push_back(lemma);
             m_prop2level.insert(lemma, lvl);
             m_solver.add_level_formula(lemma, lvl);
             return true;
         }
         else {
-            TRACE("pdr", tout << "old-level: " << old_level << " " << head()->get_name() << " " << mk_pp(lemma, m) << "\n";);
+            TRACE("pdr", tout << "old-level: " << pp_level(old_level) << " " << head()->get_name() << " " << mk_pp(lemma, m) << "\n";);
             return false;
         }
     }
@@ -337,7 +344,7 @@ namespace pdr {
         for (unsigned i = 0; i < lemmas.size(); ++i) {
             expr* lemma_i = lemmas[i].get();
             if (add_property1(lemma_i, lvl)) {
-                IF_VERBOSE(2, verbose_stream() << lvl << " " << mk_pp(lemma_i, m) << "\n";);
+                IF_VERBOSE(2, verbose_stream() << pp_level(lvl) << " " << mk_pp(lemma_i, m) << "\n";);
                 for (unsigned j = 0; j < m_use.size(); ++j) {
                     m_use[j]->add_child_property(*this, lemma_i, next_level(lvl));
                 }
@@ -1470,6 +1477,10 @@ namespace pdr {
         if (m_params.inductive_reachability_check()) {
             m_core_generalizers.push_back(alloc(core_induction_generalizer, *this));
         }
+        if (m_params.use_arith_inductive_generalizer()) {
+            m_core_generalizers.push_back(alloc(core_arith_inductive_generalizer, *this));
+        }
+        
     }
 
     void context::get_level_property(unsigned lvl, expr_ref_vector& res, vector<relation_info>& rs) const {
@@ -1914,7 +1925,7 @@ namespace pdr {
             model_node* child = alloc(model_node, &n, n_cube, pt, n.level()-1);
             ++m_stats.m_num_nodes;
             m_search.add_leaf(*child); 
-            IF_VERBOSE(2, verbose_stream() << "Predecessor: " << mk_pp(o_cube, m) << "\n";);
+            IF_VERBOSE(3, verbose_stream() << "Predecessor: " << mk_pp(o_cube, m) << "\n";);
             m_stats.m_max_depth = std::max(m_stats.m_max_depth, child->depth());
         }
         check_pre_closed(n);

src/muz_qe/pdr_generalizers.cpp

@@ -28,7 +28,9 @@ Revision History:
 namespace pdr {
 
 
-    //
+    // ------------------------
+    // core_bool_inductive_generalizer
+
     // main propositional induction generalizer.
     // drop literals one by one from the core and check if the core is still inductive.
     //    
@@ -97,6 +99,9 @@ namespace pdr {
         }
     }
 
+    // ------------------------
+    // core_farkas_generalizer 
+
     // 
     // for each disjunct of core:
     //     weaken predecessor.
@@ -142,6 +147,158 @@ namespace pdr {
     }
 
 
+    // -----------------------------
+    // core_arith_inductive_generalizer 
+
+    core_arith_inductive_generalizer::core_arith_inductive_generalizer(context& ctx):
+        core_generalizer(ctx), 
+        m(ctx.get_manager()),
+        a(m),
+        m_refs(m) {}
+
+    void core_arith_inductive_generalizer::operator()(model_node& n, expr_ref_vector& core, bool& uses_level) {
+        if (core.size() <= 1) {
+            return;
+        }
+        reset();
+        expr_ref e(m), t1(m), t2(m), t3(m);
+        rational r;
+        
+        TRACE("pdr", for (unsigned i = 0; i < core.size(); ++i) { tout << mk_pp(core[i].get(), m) << "\n"; });
+
+        svector<eq> eqs;
+        get_eqs(core, eqs);
+        
+        for (unsigned eq = 0; eq < eqs.size(); ++eq) {
+            rational r = eqs[eq].m_value;
+            expr* x = eqs[eq].m_term;
+            unsigned k = eqs[eq].m_i;
+            unsigned l = eqs[eq].m_j;
+
+            expr_ref_vector new_core(m);
+            for (unsigned i = 0; i < core.size(); ++i) {
+                if (i == k || k == l) {
+                    new_core.push_back(m.mk_true());
+                }
+                else {
+                    if (!substitute_alias(r, x, core[i].get(), e)) {
+                        e = core[i].get();
+                    }
+                    new_core.push_back(e);
+                }
+            }
+            if (abs(r) >= rational(2) && a.is_int(x)) {
+                new_core[k] = m.mk_eq(a.mk_mod(x, a.mk_numeral(rational(2), true)), a.mk_numeral(rational(0), true));
+                new_core[l] = a.mk_le(x, a.mk_numeral(r, true));
+            }
+
+            bool inductive = n.pt().check_inductive(n.level(), new_core, uses_level);
+
+            IF_VERBOSE(1, 
+                       verbose_stream() << (inductive?"":"non") << "inductive\n";
+                       for (unsigned j = 0; j < new_core.size(); ++j) { 
+                           verbose_stream() << mk_pp(new_core[j].get(), m) << "\n"; 
+                       });
+
+            if (inductive) {
+                core.reset();
+                core.append(new_core);
+            }
+        }
+    }    
+
+    void core_arith_inductive_generalizer::insert_bound(bool is_lower, expr* x, rational const& r, unsigned i) {
+        if (r.is_neg()) {
+            expr_ref e(m);
+            e = a.mk_uminus(x);
+            m_refs.push_back(e);
+            x = e;
+            is_lower = !is_lower;
+        }
+
+        if (is_lower) {
+            m_lb.insert(abs(r), std::make_pair(x, i));
+        }
+        else {
+            m_ub.insert(abs(r), std::make_pair(x, i));
+        }
+    }
+
+    void core_arith_inductive_generalizer::reset() {
+        m_refs.reset();
+        m_lb.reset();
+        m_ub.reset();
+    }
+
+    void core_arith_inductive_generalizer::get_eqs(expr_ref_vector const& core, svector<eq>& eqs) {
+        expr* e1, *x, *y;
+        expr_ref e(m);
+        rational r;
+
+        for (unsigned i = 0; i < core.size(); ++i) {
+            e = core[i];
+            if (m.is_not(e, e1) && a.is_le(e1, x, y) && a.is_numeral(y, r) && a.is_int(x)) {
+                // not (<= x r) <=> x >= r + 1
+                insert_bound(true, x, r + rational(1), i);
+            }
+            else if (m.is_not(e, e1) && a.is_ge(e1, x, y) && a.is_numeral(y, r) && a.is_int(x)) {
+                // not (>= x r) <=> x <= r - 1
+                insert_bound(false, x, r - rational(1), i);
+            }
+            else if (a.is_le(e, x, y) && a.is_numeral(y, r)) {
+                insert_bound(false, x, r, i);
+            }
+            else if (a.is_ge(e, x, y) && a.is_numeral(y, r)) {
+                insert_bound(true, x, r, i);
+            }
+        }
+        bounds_t::iterator it = m_lb.begin(), end = m_lb.end();
+        for (; it != end; ++it) {
+            rational r = it->m_key;
+            vector<term_loc_t> & terms1 = it->m_value;
+            vector<term_loc_t> terms2;
+            if (r >= rational(2) && m_ub.find(r, terms2)) {
+                for (unsigned i = 0; i < terms1.size(); ++i) {
+                    bool done = false;
+                    for (unsigned j = 0; !done && j < terms2.size(); ++j) {
+                        expr* t1 = terms1[i].first;
+                        expr* t2 = terms2[j].first;
+                        if (t1 == t2) {
+                            eqs.push_back(eq(t1, r, terms1[i].second, terms2[j].second));
+                            done = true;
+                        }
+                        else {
+                            e = m.mk_eq(t1, t2);
+                            th_rewriter rw(m);
+                            rw(e);
+                            if (m.is_true(e)) {
+                                eqs.push_back(eq(t1, r, terms1[i].second, terms2[j].second));
+                                done = true;                                
+                            }
+                        }
+                    }
+                }
+            }
+        }
+    }
+
+    bool core_arith_inductive_generalizer::substitute_alias(rational const& r, expr* x, expr* e, expr_ref& result) {
+        rational r2;
+        expr* y, *z, *e1;
+        if (m.is_not(e, e1) && substitute_alias(r, x, e1, result)) {
+            result = m.mk_not(result);
+            return true;
+        }
+        if (a.is_le(e, y, z) && a.is_numeral(z, r2) && r == r2) {
+            result = a.mk_le(y, x);
+            return true;
+        }
+        if (a.is_ge(e, y, z) && a.is_numeral(z, r2) && r == r2) {
+            result = a.mk_ge(y, x);
+            return true;
+        }
+        return false;
+    }
 
 
     // 

src/muz_qe/pdr_generalizers.h

@@ -33,6 +33,37 @@ namespace pdr {
         virtual void operator()(model_node& n, expr_ref_vector& core, bool& uses_level);
     };
 
+    template <typename T>
+    class r_map : public map<rational, T, rational::hash_proc, rational::eq_proc> {
+    };
+
+    class core_arith_inductive_generalizer : public core_generalizer {
+        typedef std::pair<expr*, unsigned> term_loc_t;
+        typedef r_map<vector<term_loc_t> > bounds_t;
+
+        ast_manager&    m;
+        arith_util      a;
+        expr_ref_vector m_refs;
+        bounds_t        m_lb;
+        bounds_t        m_ub;
+
+        struct eq {
+            expr*    m_term;
+            rational m_value;
+            unsigned m_i;
+            unsigned m_j;
+            eq(expr* t, rational const& r, unsigned i, unsigned j): m_term(t), m_value(r), m_i(i), m_j(j) {}
+        };
+        void reset();
+        void insert_bound(bool is_lower, expr* x, rational const& r, unsigned i);
+        void get_eqs(expr_ref_vector const& core, svector<eq>& eqs);
+        bool substitute_alias(rational const&r, expr* x, expr* e, expr_ref& result);
+    public:
+        core_arith_inductive_generalizer(context& ctx);
+        virtual ~core_arith_inductive_generalizer() {}
+        virtual void operator()(model_node& n, expr_ref_vector& core, bool& uses_level);
+    };
+
     class core_farkas_generalizer : public core_generalizer {
         farkas_learner m_farkas_learner;
     public:

src/muz_qe/pdr_smt_context_manager.cpp

@@ -88,7 +88,6 @@ namespace pdr {
                   for (unsigned i = 0; i < assumptions.size(); ++i) {
                       pp.add_assumption(assumptions[i].get());
                   }
-                  pp.display_smt2(tout, m.mk_true());
 
                   static unsigned lemma_id = 0;
                   std::ostringstream strm;
@@ -97,6 +96,7 @@ namespace pdr {
                   pp.display_smt2(out, m.mk_true());
                   out.close();
                   lemma_id++;
+                  tout << "pdr_check: " << strm.str() << "\n";
               });
         lbool result = m_context.check(assumptions.size(), assumptions.c_ptr());
         if (!m.is_true(m_pred)) {

src/muz_qe/qe_arith_plugin.cpp

@@ -524,7 +524,8 @@ namespace qe {
                 expr_ref as_bt_le_0(result, m), tmp2(m), tmp3(m), tmp4(m);
                 
                 // a*s + b*t + (a-1)(b-1) <= 0
-                mk_le(m_arith.mk_add(as_bt, slack), result1);
+                tmp2 = m_arith.mk_add(as_bt, slack);
+                mk_le(tmp2, result1);
                 
                 rational a1 = a, b1 = b;
                 if (abs_a < abs_b) {