mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-02 19:08:47 +00:00
Code Activity

bugfix: don't intersect forbidden intervals if variable is already assigned

Browse source
This commit is contained in:
Jakob Rath 2023-01-09 17:10:18 +01:00
parent aafd9039db
commit 3f5e6a4bfa
2 changed files with 7 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

1
src/math/polysat/solver.cpp
View file

@ -783,6 +783,7 @@ namespace polysat {
} }
void solver::assign_core(pvar v, rational const& val, justification const& j) { void solver::assign_core(pvar v, rational const& val, justification const& j) {
VERIFY(!is_assigned(v));
if (j.is_decision()) if (j.is_decision())
++m_stats.m_num_decisions; ++m_stats.m_num_decisions;
else else

6
src/math/polysat/viable.cpp
View file

@ -195,6 +195,12 @@ namespace polysat {
} }
bool viable::intersect(pvar v, signed_constraint const& c) { bool viable::intersect(pvar v, signed_constraint const& c) {
LOG("intersect v" << v << " in " << lit_pp(s, c));
if (s.is_assigned(v)) {
// this can happen e.g. for c = ovfl*(v2,v3); where intersect(pdd,pdd,signed_constraint) will try both variables.
LOG("abort intersect because v" << v << " is already assigned");
return false;
}
entry* ne = alloc_entry(); entry* ne = alloc_entry();
if (!m_forbidden_intervals.get_interval(c, v, *ne)) { if (!m_forbidden_intervals.get_interval(c, v, *ne)) {
m_alloc.push_back(ne); m_alloc.push_back(ne);