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

bugfixes

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2024-01-01 19:43:38 -08:00
parent 7fd1c171ce
commit f70f1bb85c
1 changed files with 7 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

9
src/sat/smt/polysat/core.cpp
View file

@ -306,11 +306,11 @@ namespace polysat {
sc = ~sc; sc = ~sc;
TRACE("bv", tout << "propagate " << sc << " using " << dep << " := " << value << "\n"); TRACE("bv", tout << "propagate " << sc << " using " << dep << " := " << value << "\n");
if (sc.is_always_false()) { if (sc.is_always_false()) {
s.set_conflict({dep}, "infeasible assignment"); s.set_conflict({dep}, "infeasible constraint");
return; return;
} }
rational var_value; rational var_value;
if (sc.is_eq(m_var, var_value)) if (sc.is_eq(m_var, var_value) && !is_assigned(m_var))
propagate_assignment(m_var, var_value, dep); propagate_assignment(m_var, var_value, dep);
else else
propagate_activation(idx, sc, dep); propagate_activation(idx, sc, dep);
@ -332,6 +332,11 @@ namespace polysat {
} }
if (v != null_var && !m_viable.add_unitary(v, idx)) if (v != null_var && !m_viable.add_unitary(v, idx))
viable_conflict(v); viable_conflict(v);
else if (v == null_var && sc.is_currently_false(*this)) {
auto ex = explain_eval(sc);
ex.push_back(dep);
s.set_conflict(ex, "infeasible propagation");
}
} }
void core::propagate_assignment(pvar v, rational const& value, dependency dep) { void core::propagate_assignment(pvar v, rational const& value, dependency dep) {