Merge branch 'master' of https://github.com/z3prover/z3

src/ast/datatype_decl_plugin.cpp

@@ -857,9 +857,9 @@ func_decl * datatype_util::get_non_rec_constructor_core(sort * ty, ptr_vector<so
     ptr_vector<func_decl> const * constructors = get_datatype_constructors(ty);
     // step 1)
     unsigned sz = constructors->size();
-    ++m_start;
+    unsigned start = ++m_start;
     for (unsigned j = 0; j < sz; ++j) {        
-        func_decl * c = (*constructors)[(j + m_start) % sz];
+        func_decl * c = (*constructors)[(j + start) % sz];
         unsigned num_args = c->get_arity();
         unsigned i = 0;
         for (; i < num_args; i++) {
@@ -872,7 +872,7 @@ func_decl * datatype_util::get_non_rec_constructor_core(sort * ty, ptr_vector<so
     }
     // step 2)
     for (unsigned j = 0; j < sz; ++j) {        
-        func_decl * c = (*constructors)[(j + m_start) % sz];
+        func_decl * c = (*constructors)[(j + start) % sz];
         TRACE("datatype_util_bug", tout << "non_rec_constructor c: " << c->get_name() << "\n";);
         unsigned num_args = c->get_arity();
         unsigned i = 0;

src/ast/rewriter/seq_rewriter.cpp

@@ -1946,7 +1946,7 @@ bool seq_rewriter::solve_itos(unsigned szl, expr* const* ls, unsigned szr, expr*
         }
     }
 
-    if (szr == 1 && m_util.str.is_itos(rs[0], r) && !m_util.str.is_itos(ls[0])) {
+    if (szr == 1 && szl >= 1 && m_util.str.is_itos(rs[0], r) && !m_util.str.is_itos(ls[0])) {
         return solve_itos(szr, rs, szl, ls, rhs, lhs, is_sat);
     }
 

src/sat/tactic/goal2sat.cpp

@@ -248,6 +248,7 @@ struct goal2sat::imp {
                 for (unsigned i = 0; i < num; ++i) {
                     m_result_stack[i].neg();
                 }                
+                mk_clause(m_result_stack.size(), m_result_stack.c_ptr());
             }
             else {
                 for (unsigned i = 0; i < num; ++i) {
@@ -278,6 +279,7 @@ struct goal2sat::imp {
             if (sign)
                 l.neg();
             m_result_stack.push_back(l);
+            TRACE("goal2sat", tout << m_result_stack << "\n";);
         }
     }
 

src/smt/asserted_formulas.h

@@ -96,6 +96,8 @@ class asserted_formulas {
     void max_bv_sharing();
     bool canceled() { return m.canceled(); }
 
+    void init(unsigned num_formulas, expr * const * formulas, proof * const * prs);
+
 public:
     asserted_formulas(ast_manager & m, smt_params & p);
     ~asserted_formulas();
@@ -118,7 +120,6 @@ public:
     proof * get_formula_proof(unsigned idx) const { return m.proofs_enabled() ? m_asserted_formula_prs.get(idx) : 0; }
     expr * const * get_formulas() const { return m_asserted_formulas.c_ptr(); }
     proof * const * get_formula_proofs() const { return m_asserted_formula_prs.c_ptr(); }
-    void init(unsigned num_formulas, expr * const * formulas, proof * const * prs);
     void register_simplifier_plugin(simplifier_plugin * p) { m_simplifier.register_plugin(p); }
     simplifier & get_simplifier() { return m_simplifier; }
     void get_assertions(ptr_vector<expr> & result);

src/smt/smt_conflict_resolution.cpp

@@ -348,10 +348,8 @@ namespace smt {
         literal_vector & antecedents = m_tmp_literal_vector;
         antecedents.reset();
         justification2literals_core(js, antecedents);
-        literal_vector::iterator it  = antecedents.begin();
+        for (literal l : antecedents)
-        literal_vector::iterator end = antecedents.end();
+            process_antecedent(l, num_marks);
-        for(; it != end; ++it)
-            process_antecedent(*it, num_marks);
     }
 
     /**
@@ -517,11 +515,13 @@ namespace smt {
             }
 
             TRACE("conflict", tout << "processing consequent: "; m_ctx.display_literal_verbose(tout, consequent); tout << "\n";
-                  tout << "num_marks: " << num_marks << ", js kind: " << js.get_kind() << "\n";);
+                  tout << "num_marks: " << num_marks << ", js kind: " << js.get_kind() << " level: " << m_ctx.get_assign_level(consequent) << "\n";
+                  );
             SASSERT(js != null_b_justification);
             switch (js.get_kind()) {
             case b_justification::CLAUSE: {
                 clause * cls = js.get_clause();
+                TRACE("conflict", m_ctx.display_clause_detail(tout, cls););
                 if (cls->is_lemma())
                     cls->inc_clause_activity();
                 unsigned num_lits = cls->get_num_literals();
@@ -566,7 +566,7 @@ namespace smt {
                 if (m_ctx.is_marked(l.var()))
                     break;
                 CTRACE("conflict", m_ctx.get_assign_level(l) != m_conflict_lvl && m_ctx.get_assign_level(l) != m_ctx.get_base_level(),
-                       tout << "assign_level(l): " << m_ctx.get_assign_level(l) << ", conflict_lvl: " << m_conflict_lvl << ", l: "; m_ctx.display_literal(tout, l);
+                       tout << "assign_level(l): " << m_ctx.get_assign_level(l) << ", conflict_lvl: " << m_conflict_lvl << ", l: "; m_ctx.display_literal_verbose(tout, l);
                        tout << "\n";);
                 SASSERT(m_ctx.get_assign_level(l) == m_conflict_lvl ||
                         // it may also be an (out-of-order) asserted literal