From 262acc0556d0890c06dc2828c1fe62838ac3cd4f Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 17 Jun 2019 10:28:35 -0700 Subject: [PATCH] guard insertion into enode vector @Nils-Becker, produces overflow during heavy quantifier instantiation Signed-off-by: Nikolaj Bjorner --- src/smt/mam.cpp | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/src/smt/mam.cpp b/src/smt/mam.cpp index 445f49244..022ea52f3 100644 --- a/src/smt/mam.cpp +++ b/src/smt/mam.cpp @@ -2395,7 +2395,9 @@ namespace smt { goto backtrack; // we used the equality m_n1 = m_n2 for the match and need to make sure it ends up in the log - m_used_enodes.push_back(std::make_tuple(m_n1, m_n2)); + if (m_ast_manager.has_trace_stream()) { + m_used_enodes.push_back(std::make_tuple(m_n1, m_n2)); + } m_pc = m_pc->m_next; goto main_loop;