flush gmc for sat-preprocessor model bug #4532

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
Z3Prover · Jul 26, 2020 · ac39ddb · ac39ddb
1 parent e8ef9a8
commit ac39ddb
Show file tree

Hide file tree

Showing 3 changed files with 12 additions and 8 deletions.
diff --git a/src/sat/sat_model_converter.h b/src/sat/sat_model_converter.h
@@ -81,7 +81,7 @@ namespace sat {
     private:
         vector<entry>          m_entries;           // entries accumulated during SAT search
         unsigned               m_exposed_lim;       // last entry that was exposed to model converter.
-        bool_vector          m_mark;              // literals that are used in asserted clauses.
+        bool_vector            m_mark;              // literals that are used in asserted clauses.
         solver const*          m_solver;
         elim_stackv            m_elim_stack;
 

diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp
@@ -91,9 +91,9 @@ namespace sat {
     solver::~solver() {
         m_ext = nullptr;
         SASSERT(m_config.m_num_threads > 1 || check_invariant());
-        TRACE("sat", tout << "Delete clauses\n";);
+        CTRACE("sat", !m_clauses.empty(), tout << "Delete clauses\n";);
         del_clauses(m_clauses);
-        TRACE("sat", tout << "Delete learned\n";);
+        CTRACE("sat", !m_learned.empty(), tout << "Delete learned\n";);
         del_clauses(m_learned);
         dealloc(m_cuber);
         m_cuber = nullptr;
@@ -1207,6 +1207,7 @@ namespace sat {
             propagate(false);
             if (check_inconsistent()) return l_false;
             if (m_config.m_force_cleanup) do_cleanup(true);
+            TRACE("sat", display(tout););
 
             if (m_config.m_gc_burst) {
                 // force gc
@@ -1221,6 +1222,7 @@ namespace sat {
 
             if (m_config.m_max_conflicts == 0) {
                 IF_VERBOSE(SAT_VB_LVL, verbose_stream() << "(sat \"abort: max-conflicts = 0\")\n";);
+                TRACE("sat", display(tout); m_mc.display(tout););
                 return l_undef;
             }
 

diff --git a/src/sat/tactic/goal2sat.cpp b/src/sat/tactic/goal2sat.cpp
@@ -965,8 +965,10 @@ void sat2goal::mc::flush_smc(sat::solver_core& s, atom2bool_var const& map) {
     s.flush(m_smc);
     m_var2expr.resize(s.num_vars());
     map.mk_var_inv(m_var2expr);
+    flush_gmc();
 }
 
+
 void sat2goal::mc::flush_gmc() {
     sat::literal_vector updates;
     m_smc.expand(updates);    
@@ -1072,14 +1074,15 @@ void sat2goal::mc::insert(sat::bool_var v, app * atom, bool aux) {
 }
 
 expr_ref sat2goal::mc::lit2expr(sat::literal l) {
-    if (!m_var2expr.get(l.var())) {
+    sat::bool_var v = l.var();
+    if (!m_var2expr.get(v)) {
         app* aux = m.mk_fresh_const(nullptr, m.mk_bool_sort());
-        m_var2expr.set(l.var(), aux);
+        m_var2expr.set(v, aux);
         if (!m_gmc) m_gmc = alloc(generic_model_converter, m, "sat2goal");
         m_gmc->hide(aux->get_decl());
     }
-    VERIFY(m_var2expr.get(l.var()));
-    expr_ref result(m_var2expr.get(l.var()), m);
+    VERIFY(m_var2expr.get(v));
+    expr_ref result(m_var2expr.get(v), m);
     if (l.sign()) {
         result = m.mk_not(result);
     }
@@ -1210,7 +1213,6 @@ struct sat2goal::imp {
             checkpoint();            
             r.assert_expr(lit2expr(mc, s.trail_literal(i)));
         }
-
         // collect binary clauses
         svector<sat::solver::bin_clause> bin_clauses;
         s.collect_bin_clauses(bin_clauses, m_learned, false);