na

Signed-off-by: Nikolaj Bjorner <[email protected]>
Z3Prover · Aug 26, 2020 · 1a36d44 · 1a36d44
1 parent c21a2fc
commit 1a36d44
Showing 1 changed file with 6 additions and 3 deletions.
diff --git a/src/sat/tactic/goal2sat.cpp b/src/sat/tactic/goal2sat.cpp
@@ -173,7 +173,7 @@ struct goal2sat::imp : public sat::sat_internalizer {
                 TRACE("sat", tout << "new_var: " << v << ": " << mk_bounded_pp(t, m, 2) << " " << is_uninterp_const(t) << "\n";);
                 if (!is_uninterp_const(t)) {
                     if (m_euf) {
-                        convert_euf(t, root, sign);
+                        convert_euf(t, root, sign);                        
                         return;
                     }
                     else
@@ -186,6 +186,8 @@ struct goal2sat::imp : public sat::sat_internalizer {
             l = sat::literal(v, sign);
             m_solver.set_eliminated(v, false);
         }
+        if (root)
+            m_result_stack.reset();
         SASSERT(l != sat::null_literal);
         if (root)
             mk_clause(l);
@@ -331,7 +333,6 @@ struct goal2sat::imp : public sat::sat_internalizer {
             m_cache.insert(t, l);
             sat::literal * lits = m_result_stack.end() - num;
 
-
             // l => /\ lits
             for (unsigned i = 0; i < num; i++) {
                 mk_clause(~l, lits[i]);
@@ -481,6 +482,8 @@ struct goal2sat::imp : public sat::sat_internalizer {
         sat::literal lit = internalize.internalize(*this, t, sign, root);
         if (root)
             m_result_stack.reset();
+        else 
+            m_result_stack.shrink(m_result_stack.size() - t->get_num_args());
         if (lit == sat::null_literal)
             return;
         if (root) 
@@ -507,6 +510,7 @@ struct goal2sat::imp : public sat::sat_internalizer {
             default:
                 UNREACHABLE();
             }
+            SASSERT(!root || m_result_stack.empty());
         }
         else if (pb.is_pb(t)) {
             convert_ba(t, root, sign);
@@ -781,7 +785,6 @@ void sat2goal::mc::flush_smc(sat::solver_core& s, atom2bool_var const& map) {
     flush_gmc();
 }
 
-
 void sat2goal::mc::flush_gmc() {
     sat::literal_vector updates;
     m_smc.expand(updates);