From b259f46f8502e8ee2da0fcf781d3f013f5d80b43 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 13 Jan 2022 12:34:58 -0800 Subject: [PATCH] dependencies --- scripts/mk_project.py | 2 +- src/sat/smt/q_solver.cpp | 3 ++- 2 files changed, 3 insertions(+), 2 deletions(-) diff --git a/scripts/mk_project.py b/scripts/mk_project.py index 12604d079..147e310a7 100644 --- a/scripts/mk_project.py +++ b/scripts/mk_project.py @@ -51,7 +51,7 @@ def init_project_def(): add_lib('mbp', ['model', 'simplex'], 'qe/mbp') add_lib('qe_lite', ['tactic', 'mbp'], 'qe/lite') add_lib('solver_assertions', ['pattern','smt_params','cmd_context','qe_lite'], 'solver/assertions') - add_lib('sat_smt', ['sat', 'euf', 'tactic', 'solver', 'smt_params', 'bit_blaster', 'fpa', 'mbp', 'normal_forms', 'lp', 'pattern'], 'sat/smt') + add_lib('sat_smt', ['sat', 'euf', 'tactic', 'solver', 'smt_params', 'bit_blaster', 'fpa', 'mbp', 'normal_forms', 'lp', 'pattern', 'qe_lite'], 'sat/smt') add_lib('sat_tactic', ['tactic', 'sat', 'solver', 'sat_smt'], 'sat/tactic') add_lib('nlsat_tactic', ['nlsat', 'sat_tactic', 'arith_tactics'], 'nlsat/tactic') add_lib('subpaving_tactic', ['core_tactics', 'subpaving'], 'math/subpaving/tactic') diff --git a/src/sat/smt/q_solver.cpp b/src/sat/smt/q_solver.cpp index f0a28cfd4..ed19469a7 100644 --- a/src/sat/smt/q_solver.cpp +++ b/src/sat/smt/q_solver.cpp @@ -301,7 +301,8 @@ namespace q { } return true; } - else if (updated) { + else if (m_expanded.size() == 1 && updated) { + m_expanded[0] = r; flatten(to_quantifier(r)); return true; }