From 18a76ab82c29a2777674499c3efdf0e71f477fa5 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 11 Jul 2021 06:42:27 +0200 Subject: [PATCH] #5336 Signed-off-by: Nikolaj Bjorner --- src/sat/smt/euf_internalize.cpp | 4 ++-- src/sat/smt/q_solver.cpp | 2 +- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/src/sat/smt/euf_internalize.cpp b/src/sat/smt/euf_internalize.cpp index caf12235c..a7476bc5d 100644 --- a/src/sat/smt/euf_internalize.cpp +++ b/src/sat/smt/euf_internalize.cpp @@ -140,8 +140,8 @@ namespace euf { s().mk_clause(~lit, lit2, sat::status::th(m_is_redundant, m.get_basic_family_id())); s().mk_clause(lit, ~lit2, sat::status::th(m_is_redundant, m.get_basic_family_id())); if (relevancy_enabled()) { - add_root(~lit, lit2); - add_root(lit, ~lit2); + add_aux(~lit, lit2); + add_aux(lit, ~lit2); } lit = lit2; } diff --git a/src/sat/smt/q_solver.cpp b/src/sat/smt/q_solver.cpp index b114e844f..af670297c 100644 --- a/src/sat/smt/q_solver.cpp +++ b/src/sat/smt/q_solver.cpp @@ -50,7 +50,7 @@ namespace q { } return; } - if (exp.size() > 1 && is_exists(q) /* && l.sign() */) { + if (exp.size() > 1 && is_exists(q) && l.sign()) { sat::literal_vector lits; lits.push_back(~l); for (expr* e : exp)