mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-06 06:03:23 +00:00
Code Activity

remove code that causes infinite loop. Stackoverflow question from Dominik Wojtaszek

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2017-03-17 10:52:16 -07:00
parent d754aa2dc4
commit d58018841e
1 changed files with 0 additions and 8 deletions
Download patch file Download diff file Expand all files Collapse all files

8
src/ast/ast_smt2_pp.cpp
View file

@ -1002,14 +1002,6 @@ class smt2_printer {
reset_stacks(); reset_stacks();
SASSERT(&(r.get_manager()) == &(fm())); SASSERT(&(r.get_manager()) == &(fm()));
m_soccs(n); m_soccs(n);
TRACE("smt2_pp_shared",
tout << "shared terms for:\n" << mk_pp(n, m()) << "\n";
tout << "------>\n";
shared_occs::iterator it = m_soccs.begin_shared();
shared_occs::iterator end = m_soccs.end_shared();
for (; it != end; ++it) {
tout << mk_pp(*it, m()) << "\n";
});
m_root = n; m_root = n;
push_frame(n, true); push_frame(n, true);
while (!m_frame_stack.empty()) { while (!m_frame_stack.empty()) {