mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-06-19 15:16:29 +00:00
Code Activity

remove atom

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2026-06-12 10:58:11 -07:00
parent 7f1e74c0da
commit 81af0cc230
1 changed files with 8 additions and 8 deletions
Download patch file Download diff file Expand all files Collapse all files

16
src/smt/smt_solver.cpp
View file

@ -88,13 +88,13 @@ namespace {
updt_params(p);
}
solver * translate(ast_manager & m, params_ref const & p) override {
ast_translation translator(get_manager(), m);
solver * translate(ast_manager & target, params_ref const & p) override {
ast_translation translator(get_manager(), target);
params_ref init;
init.copy(get_params());
init.copy(p);
smt_solver* result = alloc(smt_solver, m, init, m_logic);
smt_solver* result = alloc(smt_solver, target, init, m_logic);
smt::kernel::copy(m_context, result->m_context, true);
if (mc0())
@ -481,12 +481,12 @@ namespace {
}
vars.reset();
for (auto const& c : candidates)
vars.push_back(c.e);
expr_ref_vector lits(m);
if (!candidates.empty())
lits.push_back(candidates[0].e);
for (auto const &c : candidates) {
vars.push_back(c.e);
lits.push_back(c.e);
}
return lits;
}