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

update comment

Browse source
This commit is contained in:
Jakob Rath 2023-03-16 16:55:40 +01:00
parent 8493ebbaba
commit 6c9cf6182c
1 changed files with 4 additions and 6 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -867,12 +867,10 @@ namespace polysat {
m_free_pvars.unassign_var_eh(v);
return;
case find_t::singleton:
// 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;
// Any propagations should have been discovered by viable::intersect.
// The fallback solver currently does not detect propagations, because we would need to handle justifications differently.
UNREACHABLE();
Z3_fallthrough; // we could still treat it as decision
case find_t::multiple:
j = justification::decision(m_level + 1);
break;