#6758

check-assumptions with compound formulas create fresh proxy variables both during compilation to internal format and for the assumptions. These fresh variables may occur in lemmas that are created during search. The lemmas are garbage for future check-sats, but the solver needs to be allowed to invoke GC. Adding a GC call before a check-sat with assumptions allows removing some lemmas every time a new assumptions are used. Eager GC when using assumptions is used elsewhere, for example in cube&conquer scenarios where lemmas learned from one set of assumptions are less likely to be useful for other assumptions.

With the GC invocation memory grows at a lesser pace. However, it is not entirely free of memory increases. To avoid memory bloat, have the solver pre-compile the assumptions by defining them as propositional variables, add assertions that the propositional variables are equivalent to the compound formulas and use the propositional variables as assumptions. The same propositional variables come with no extra overhead when invoking check-assumptions. The lemmas are then over the same fixed vocabulary. It is generally a good idea to recycle useful lemmas during the enumeration pass.

src/smt/smt_context.cpp

@@ -3337,6 +3337,7 @@ namespace smt {
         reset_assumptions();
         m_literal2assumption.reset();
         m_unsat_core.reset();
+
         if (!asms.empty()) {
             // We must give a chance to the theories to propagate before we create a new scope...
             propagate();
@@ -3346,6 +3347,7 @@ namespace smt {
                 return;
             if (get_cancel_flag())
                 return;
+            del_inactive_lemmas();
             push_scope();
             vector<std::pair<expr*,expr_ref>> asm2proxy;
             internalize_proxies(asms, asm2proxy);