From 9038dfd30de27770672d790f58bea7f64c97667b Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 16 Jun 2021 23:27:26 -0500 Subject: [PATCH] #5336 --- src/sat/smt/q_solver.cpp | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/src/sat/smt/q_solver.cpp b/src/sat/smt/q_solver.cpp index 2caf0eb75..eebb4a721 100644 --- a/src/sat/smt/q_solver.cpp +++ b/src/sat/smt/q_solver.cpp @@ -61,8 +61,11 @@ namespace q { return; } - if (l.sign() == is_forall(e)) - add_clause(~l, skolemize(q)); + if (l.sign() == is_forall(e)) { + sat::literal lit = skolemize(q); + add_clause(~l, lit); + ctx.add_root(~l, lit); + } else { ctx.push_vec(m_universal, l); if (ctx.get_config().m_ematching)