mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-31 03:32:28 +00:00
Code Activity

fix missing handling of axiom

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2024-01-12 18:15:26 -08:00
parent aefbfc6ca4
commit 211aff4cba
1 changed files with 12 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

14
src/sat/smt/polysat_solver.cpp
View file

@ -286,10 +286,19 @@ namespace polysat {
++m_stats.m_num_propagations;
TRACE("bv", tout << "propagate " << d << " " << sign << "\n");
auto [core, eqs] = explain_deps(deps);
SASSERT(d.is_bool_var() || d.is_eq());
SASSERT(d.is_bool_var() || d.is_eq() || d.is_axiom());
proof_hint* hint = nullptr;
if (d.is_bool_var()) {
if (d.is_axiom()) {
if (sign) {
if (ctx.use_drat() && hint_info)
hint = mk_proof_hint(hint_info, core, eqs);
auto ex = euf::th_explain::conflict(*this, core, eqs, hint);
validate_conflict(core, eqs);
ctx.set_conflict(ex);
}
}
else if (d.is_bool_var()) {
auto bv = d.bool_var();
auto lit = sat::literal(bv, sign);
if (s().value(lit) == l_true)
@ -304,6 +313,7 @@ namespace polysat {
ctx.propagate(lit, ex);
}
else if (sign) {
SASSERT(d.is_eq());
auto const [v1, v2] = d.eq();
// equalities are always asserted so a negative propagation is a conflict.
auto n1 = var2enode(v1);