mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 10:25:18 +00:00
guard insertion into enode vector @Nils-Becker, produces overflow during heavy quantifier instantiation
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
f3b79087ee
commit
262acc0556
|
@ -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;
|
||||
|
|
Loading…
Reference in a new issue