From 93415740b6d6cb22561366c2e4a9a315de6d0585 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 7 Sep 2021 07:00:41 +0200 Subject: [PATCH] left over bugs #5532 disabling complete const rewriting (temporarily) as it can loop --- src/ast/rewriter/rewriter_def.h | 4 ++++ src/sat/smt/euf_solver.cpp | 3 ++- 2 files changed, 6 insertions(+), 1 deletion(-) diff --git a/src/ast/rewriter/rewriter_def.h b/src/ast/rewriter/rewriter_def.h index f8e20b2bf67..2707c229f31 100644 --- a/src/ast/rewriter/rewriter_def.h +++ b/src/ast/rewriter/rewriter_def.h @@ -195,10 +195,14 @@ bool rewriter_tpl::visit(expr * t, unsigned max_depth) { if (process_const(to_app(t))) return true; TRACE("rewriter_const", tout << "process const: " << mk_bounded_pp(t, m()) << " -> " << mk_bounded_pp(m_r, m()) << "\n";); +#if 1 +#else + // disabled pending fix for loop/stack overflow in case of recursive expansion (possible) rewriter_tpl rw(m(), false, m_cfg); expr_ref result(m()); rw(m_r, result, m_pr); m_r = result; +#endif set_new_child_flag(t, m_r); result_stack().push_back(m_r); return true; diff --git a/src/sat/smt/euf_solver.cpp b/src/sat/smt/euf_solver.cpp index fe91914a7ee..68b70cb5e5a 100644 --- a/src/sat/smt/euf_solver.cpp +++ b/src/sat/smt/euf_solver.cpp @@ -599,7 +599,8 @@ namespace euf { if (is_app(e)) for (expr* arg : *to_app(e)) args.push_back(e_internalize(arg)); - mk_enode(e, args.size(), args.data()); + if (!m_egraph.find(e)) + mk_enode(e, args.size(), args.data()); } attach_lit(lit, e); }