From 4d31ff7a38ecbb7d56afec76f70f3e5d7333d8a1 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 21 Jul 2023 08:35:09 -0700 Subject: [PATCH] remove unused variable Signed-off-by: Nikolaj Bjorner --- src/sat/smt/euf_solver.cpp | 9 ++++----- 1 file changed, 4 insertions(+), 5 deletions(-) diff --git a/src/sat/smt/euf_solver.cpp b/src/sat/smt/euf_solver.cpp index 471ebac66..89a8433e1 100644 --- a/src/sat/smt/euf_solver.cpp +++ b/src/sat/smt/euf_solver.cpp @@ -240,9 +240,9 @@ namespace euf { if (ext == this) get_antecedents(l, constraint::from_idx(idx), r, probing); - else { + else ext->get_antecedents(l, idx, r, probing); - } + if (create_hint && ext != this) ext->get_antecedents(l, idx, m_hint_lits, probing); @@ -254,7 +254,6 @@ namespace euf { size_t idx = get_justification(e); auto* ext = sat::constraint_base::to_extension(idx); SASSERT(ext != this); - auto& jst = th_explain::from_index(idx); sat::literal lit = sat::null_literal; ext->get_antecedents(lit, idx, r, probing); } @@ -278,12 +277,12 @@ namespace euf { } hint = mk_hint(m_euf, l); } - + + CTRACE("euf", probing, tout << "explain " << l << " <- " << r << "\n"); unsigned j = 0; for (sat::literal lit : r) if (s().lvl(lit) > 0) r[j++] = lit; r.shrink(j); - CTRACE("euf", probing, tout << "explain " << l << " <- " << r << "\n"); CTRACE("euf", create_hint, tout << "explain " << l << " <- " << m_hint_lits << "\n"); DEBUG_CODE(for (auto lit : r) SASSERT(s().value(lit) == l_true););