Merge branch 'unstable' of https://github.com/Z3Prover/z3 into unstable

src/ast/rewriter/bv_rewriter.h

@@ -168,6 +168,8 @@ public:
     }
 
     br_status mk_eq_core(expr * lhs, expr * rhs, expr_ref & result);
+
+    bool hi_div0() const { return m_hi_div0; }
 };
 
 #endif

src/opt/maxres.cpp

@@ -228,7 +228,6 @@ public:
             switch (is_sat) {
             case l_true: 
                 get_current_correction_set(cs);
-                IF_VERBOSE(2, display_vec(verbose_stream() << "correction set: ", cs););
                 if (cs.empty()) {
                     m_found_feasible_optimum = m_model.get() != 0;
                     m_lower = m_upper;
@@ -350,9 +349,11 @@ public:
             is_sat = minimize_core(core);
             ++m_stats.m_num_cores;
             if (is_sat != l_true) {
+                IF_VERBOSE(100, verbose_stream() << "(opt.maxres minimization failed)\n";);
                 break;
             }
             if (core.empty()) {
+                IF_VERBOSE(100, verbose_stream() << "(opt.maxres core is empty)\n";);
                 cores.reset();
                 m_lower = m_upper;
                 return l_true;
@@ -470,6 +471,7 @@ public:
         SASSERT(!core.empty());
         rational w = split_core(core);
         TRACE("opt", display_vec(tout << "minimized core: ", core););
+        IF_VERBOSE(10, display_vec(verbose_stream() << "core: ", core););
         max_resolve(core, w);
         fml = mk_not(m, mk_and(m, m_B.size(), m_B.c_ptr()));
         s().assert_expr(fml);

src/sat/sat_solver.cpp

@@ -964,6 +964,7 @@ namespace sat {
                 set_conflict(justification(), ~lit);
                 flet<bool> _min1(m_config.m_minimize_core, false);
                 flet<bool> _min2(m_config.m_minimize_core_partial, false);
+                m_conflict_lvl = 1;
                 resolve_conflict_for_unsat_core();
                 m_assumptions.pop_back();
                 weight += weights[i];
@@ -2630,7 +2631,7 @@ namespace sat {
         out << "p wcnf " << num_vars() << " " << num_clauses() + sz << " " << max_weight << "\n";
 
         for (unsigned i = 0; i < m_trail.size(); i++) {
-            out << dimacs_lit(m_trail[i]) << " 0\n";
+            out << max_weight << " " << dimacs_lit(m_trail[i]) << " 0\n";
         }
         vector<watch_list>::const_iterator it  = m_watches.begin();
         vector<watch_list>::const_iterator end = m_watches.end();

src/smt/theory_dl.cpp

@@ -235,13 +235,14 @@ namespace smt {
         }
 
         app* mk_bv_constant(uint64 val, sort* s) {
-            return b().mk_numeral(rational(val,rational::ui64()),64);
+            return b().mk_numeral(rational(val, rational::ui64()), 64);
         }
 
         app* max_value(sort* s) {
             uint64 sz;
             VERIFY(u().try_get_size(s, sz));
-            return mk_bv_constant(sz, s);
+            SASSERT(sz > 0);
+            return mk_bv_constant(sz-1, s);
         }
 
         void mk_lt(app* x, app* y) {

src/tactic/bv/bv1_blaster_tactic.cpp

@@ -28,6 +28,7 @@ Notes:
 #include"rewriter_def.h"
 #include"for_each_expr.h"
 #include"cooperate.h"
+#include"bv_rewriter.h"
 
 class bv1_blaster_tactic : public tactic {
 
@@ -491,6 +492,8 @@ tactic * mk_bv1_blaster_tactic(ast_manager & m, params_ref const & p) {
 class is_qfbv_eq_probe : public probe {
 public:
     virtual result operator()(goal const & g) {
+        bv_rewriter rw(g.m());
+        if (!rw.hi_div0()) return false;
         bv1_blaster_tactic t(g.m());
         return t.is_target(g);
 

src/tactic/probe.cpp

@@ -23,6 +23,7 @@ Revision History:
 #include"arith_decl_plugin.h"
 #include"bv_decl_plugin.h"
 #include"goal_util.h"
+#include"bv_rewriter.h"
 
 class memory_probe : public probe {
 public:
@@ -303,6 +304,8 @@ public:
 class is_qfbv_probe : public probe {
 public:
     virtual result operator()(goal const & g) {
+        bv_rewriter rw(g.m());
+        if (!rw.hi_div0()) return false;
         return !test<is_non_qfbv_predicate>(g);
     }
 };