dbg build

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
Z3Prover · Aug 28, 2020 · 739b537 · 739b537
1 parent 93ee2a6
commit 739b537
Showing 1 changed file with 5 additions and 6 deletions.
diff --git a/src/sat/sat_solver/inc_sat_solver.cpp b/src/sat/sat_solver/inc_sat_solver.cpp
@@ -836,7 +836,6 @@ class inc_sat_solver : public solver {
         if (m_fmls_head == m_fmls.size()) {
             return l_true;
         }
-        dep2asm_t dep2asm;
         goal_ref g = alloc(goal, m, true, false); // models, maybe cores are enabled
         for (unsigned i = m_fmls_head ; i < m_fmls.size(); ++i) {
             expr* fml = m_fmls.get(i);
@@ -877,13 +876,13 @@ class inc_sat_solver : public solver {
                 }
             }
         }
-        CTRACE("sat", dep2asm.size() != m_asms.size(), 
-               tout << dep2asm.size() << " vs " << m_asms.size() << "\n";
+        CTRACE("sat", m_dep2asm.size() != m_asms.size(), 
+               tout << m_dep2asm.size() << " vs " << m_asms.size() << "\n";
                tout << m_asms << "\n";
-               for (auto const& kv : dep2asm) {
+               for (auto const& kv : m_dep2asm) {
                    tout << mk_pp(kv.m_key, m) << " " << kv.m_value << "\n";
                });
-        SASSERT(dep2asm.size() == m_asms.size());
+        SASSERT(m_dep2asm.size() == m_asms.size());
     }
 
     void extract_asm2dep(u_map<expr*>& asm2dep) {
@@ -897,7 +896,7 @@ class inc_sat_solver : public solver {
         extract_asm2dep(asm2dep);
         sat::literal_vector const& core = m_solver.get_core();
         TRACE("sat",
-              for (auto kv : dep2asm) {
+              for (auto kv : m_dep2asm) {
                   tout << mk_pp(kv.m_key, m) << " |-> " << sat::literal(kv.m_value) << "\n";
               }
               tout << "asm2fml: ";