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

src/sat/sat_clause.cpp

@@ -174,7 +174,7 @@ namespace sat {
     }
 
     void clause_allocator::del_clause(clause * cls) {
-        TRACE("sat", tout << "delete: " << cls->id() << " " << cls << "\n";);
+        TRACE("sat", tout << "delete: " << cls->id() << " " << cls << " " << *cls << "\n";);
         m_id_gen.recycle(cls->id());
         size_t size = clause::get_obj_size(cls->m_capacity);
 #ifdef _AMD64_

src/sat/sat_elim_eqs.cpp

@@ -128,6 +128,11 @@ namespace sat {
             if (j == 0) {
                 // empty clause
                 m_solver.set_conflict(justification());
+                for (; it != end; ++it) {
+                    *it2 = *it;
+                    it2++;
+                }
+                cs.set_end(it2);
                 return;
             }
             TRACE("elim_eqs", tout << "after removing duplicates: " << c << " j: " << j << "\n";);

src/sat/sat_integrity_checker.cpp

@@ -207,6 +207,24 @@ namespace sat {
         }
         return true;
     }
+
+    bool integrity_checker::check_disjoint_clauses() const {
+        uint_set ids;
+        clause_vector::const_iterator it  = s.m_clauses.begin();
+        clause_vector::const_iterator end = s.m_clauses.end();
+        for (; it != end; ++it) {
+            ids.insert((*it)->id());
+        }
+        it = s.m_learned.begin();
+        end = s.m_learned.end();
+        for (; it != end; ++it) {
+            if (ids.contains((*it)->id())) {
+                TRACE("sat", tout << "Repeated clause: " << (*it)->id() << "\n";);
+                return false;
+            }
+        }
+        return true;
+    }
     
     bool integrity_checker::operator()() const {
         if (s.inconsistent())
@@ -216,6 +234,7 @@ namespace sat {
         SASSERT(check_watches());
         SASSERT(check_bool_vars());
         SASSERT(check_reinit_stack());
+        SASSERT(check_disjoint_clauses());
         return true;
     }
 };

src/sat/sat_integrity_checker.h

@@ -36,6 +36,7 @@ namespace sat {
         bool check_bool_vars() const;
         bool check_watches() const;
         bool check_reinit_stack() const;
+        bool check_disjoint_clauses() const;
         bool operator()() const;
     };
 };

src/sat/sat_simplifier.cpp

@@ -227,6 +227,7 @@ namespace sat {
     }
 
     void simplifier::cleanup_clauses(clause_vector & cs, bool learned, bool vars_eliminated, bool in_use_lists) {
+        TRACE("sat", tout << "cleanup_clauses\n";);
         clause_vector::iterator it  = cs.begin();
         clause_vector::iterator it2 = it;
         clause_vector::iterator end = cs.end();

src/sat/sat_solver.cpp

@@ -50,7 +50,10 @@ namespace sat {
     }
 
     solver::~solver() {
+        SASSERT(check_invariant());
+        TRACE("sat", tout << "Delete clauses\n";);
         del_clauses(m_clauses.begin(), m_clauses.end());
+        TRACE("sat", tout << "Delete learned\n";);
         del_clauses(m_learned.begin(), m_learned.end());
     }
 
@@ -1121,6 +1124,7 @@ namespace sat {
        \brief GC (the second) half of the clauses in the database.
     */
     void solver::gc_half(char const * st_name) {
+        TRACE("sat", tout << "gc\n";);
         unsigned sz     = m_learned.size();
         unsigned new_sz = sz/2;
         unsigned j      = new_sz;
@@ -1145,6 +1149,7 @@ namespace sat {
        \brief Use gc based on dynamic psm. Clauses are initially frozen.
     */
     void solver::gc_dyn_psm() {
+        TRACE("sat", tout << "gc\n";);
         // To do gc at scope_lvl() > 0, I will need to use the reinitialization stack, or live with the fact
         // that I may miss some propagations for reactivated clauses.
         SASSERT(scope_lvl() == 0);

src/smt/asserted_formulas.cpp

@@ -603,7 +603,7 @@ void asserted_formulas::propagate_values() {
     proof_ref_vector new_prs1(m_manager);
     expr_ref_vector  new_exprs2(m_manager);
     proof_ref_vector new_prs2(m_manager);
-    unsigned i  = m_asserted_qhead;
+    unsigned i  = 0;
     unsigned sz = m_asserted_formulas.size();
     for (; i < sz; i++) {
         expr * n    = m_asserted_formulas.get(i);