mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-10 19:27:06 +00:00
Code Activity

smc

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2022-09-25 18:03:16 -07:00
parent 3dfff3d7a1
commit d7b9cc70d0
1 changed files with 4 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
src/sat/smt/q_mbi.cpp
View file

@ -355,8 +355,10 @@ namespace q {
return expr_ref(m);
}
else if (!(*p)(*m_model, vars, fmls))
else if (!(*p)(*m_model, vars, fmls)) {
TRACE("q", tout << "theory projection failed\n");
return expr_ref(m);
}
}
for (app* v : vars) {
expr_ref term(m);
@ -581,6 +583,7 @@ namespace q {
binding.reset();
auto const& nodes = ctx.get_egraph().nodes();
m_model->reset_eval_cache();
model::scoped_model_completion _sc(*m_model, true);
for (unsigned j = 0; j < offsets.size(); ++j) {
unsigned offset = offsets[j];
binding.push_back(nodes[offset]->get_expr());