mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-24 17:45:32 +00:00
Code Activity

UNREACHABLE was actually reachable

Browse source
This commit is contained in:
Jakob Rath 2023-03-09 13:35:07 +01:00
parent 60a405d134
commit 686f1c6aaf
1 changed files with 10 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -787,11 +787,18 @@ namespace polysat {
justification j;
switch (m_viable.find_viable(v, val)) {
case find_t::empty:
UNREACHABLE(); // should have been discovered earlier in viable::intersect
// NOTE: this case can happen if find_viable calls the fallback solver,
// because the fallback solver has access to all univariate constraints
// even if they are not used for intervals (e.g., op_constraints)
VERIFY(is_conflict());
return;
case find_t::singleton:
UNREACHABLE(); // should have been discovered earlier in viable::intersect
return;
// NOTE: see comment on find_t::empty.
// We treat this case the same as decisions, because
// - it is very rare (not yet observed once as far as I can tell, but it should be possible),
// - if we set it as propagation we would need to handle justifications differently since they must
// contain at least one constraint that's not handled by intervals.
Z3_fallthrough;
case find_t::multiple:
j = justification::decision(m_level + 1);
break;