From f90db2ba1c813de705ddfba8b269c231c5752bb1 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 23 Aug 2019 21:35:45 +0300 Subject: [PATCH] add back compression to ensure local functions are inlined #2517 Signed-off-by: Nikolaj Bjorner --- src/parsers/smt2/smt2parser.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/parsers/smt2/smt2parser.cpp b/src/parsers/smt2/smt2parser.cpp index 99312c912..ae2a1fff6 100644 --- a/src/parsers/smt2/smt2parser.cpp +++ b/src/parsers/smt2/smt2parser.cpp @@ -2650,7 +2650,7 @@ namespace smt2 { m_ctx.regular_stream() << "("; expr ** expr_it = expr_stack().c_ptr() + spos; expr ** expr_end = expr_it + m_cached_strings.size(); - // md->compress(); + md->compress(); for (unsigned i = 0; expr_it < expr_end; expr_it++, i++) { model::scoped_model_completion _scm(md, true); expr_ref v = (*md)(*expr_it);