mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-09-03 08:38:06 +00:00
Code Activity

only allow flip if it doesn't increase unsat score

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2025-01-02 08:39:43 -08:00
parent 814d7f4d0a
commit f67e1b8b8b
3 changed files with 16 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

3
src/ast/sls/sls_bv_lookahead.cpp
View file

@ -553,8 +553,11 @@ namespace sls {
continue;
if (ctx.is_true(v) == v1)
continue;
unsigned num_unsat = ctx.unsat().size();
TRACE("bv", tout << "update flip " << mk_bounded_pp(e, m) << "\n";);
ctx.flip(v);
if (num_unsat < ctx.unsat().size())
ctx.flip(v);
}
m_ev.set_bool_value(to_app(e), v1);
}