From 75c6d7b5a8f2570c197cd1f350f0eb1729171ce8 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 9 Aug 2023 16:31:44 -0700 Subject: [PATCH] add comments Signed-off-by: Nikolaj Bjorner --- src/sat/smt/synth_solver.cpp | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/src/sat/smt/synth_solver.cpp b/src/sat/smt/synth_solver.cpp index 6c839af4f..0292c3d46 100644 --- a/src/sat/smt/synth_solver.cpp +++ b/src/sat/smt/synth_solver.cpp @@ -156,11 +156,15 @@ namespace synth { } } + if (m_blockers.size() > m_blockers_qhead) + return; + for (app* e : m_synth) { + // TODO: actually wait to call compute_solution until unit propagation! euf::enode* n = expr2enode(e->get_arg(0)); if (is_computable(n)) { expr_ref sol = compute_solution(e); - verbose_stream() << "solution " << sol << "\n"; + IF_VERBOSE(0, verbose_stream() << "solution " << sol << "\n"); ctx.push_vec(m_blockers, ~eq_internalize(sol, n->get_expr())); } }