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

fix return value when in external mode bool-flip

Browse source 
return null_bool_var instead of false (= 0).
This commit is contained in:
Nikolaj Bjorner 2025-01-25 22:57:58 -08:00
parent d4f2de734b
commit 7fb6497ce1
2 changed files with 4 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/ast/sls/sat_ddfw.cpp
View file

@ -161,7 +161,7 @@ namespace sat {
if (m_unsat_vars.empty())
return null_bool_var;
if (m_in_external_flip)
return false;
return null_bool_var;
return m_unsat_vars.elem_at(m_rand(m_unsat_vars.size()));
}

4
src/ast/sls/sls_arith_clausal.cpp
View file

@ -276,7 +276,9 @@ namespace sls {
for (sat::bool_var bv = 0; bv < ctx.num_bool_vars(); ++bv) {
if (a.get_ineq(bv) && a.get_ineq(bv)->is_true() != ctx.is_true(bv)) {
TRACE("arith", tout << "bv:" << bv << " " << *a.get_ineq(bv) << ctx.is_true(bv) << "\n";
tout << "bool vars: " << a.m_vars[v].m_bool_vars_of << "\n");
tout << "v" << v << " bool vars: " << a.m_vars[v].m_bool_vars_of << "\n";
tout << mk_bounded_pp(a.m_vars[v].m_expr, a.m) << "\n";
tout << mk_bounded_pp(ctx.atom(bv), a.m) << "\n");
}
VERIFY(!a.get_ineq(bv) || a.get_ineq(bv)->is_true() == ctx.is_true(bv));
});