From 6c9cf6182ceb265fef751316d68e19ecac705e89 Mon Sep 17 00:00:00 2001 From: Jakob Rath Date: Thu, 16 Mar 2023 16:55:40 +0100 Subject: [PATCH] update comment --- src/math/polysat/solver.cpp | 10 ++++------ 1 file changed, 4 insertions(+), 6 deletions(-) diff --git a/src/math/polysat/solver.cpp b/src/math/polysat/solver.cpp index dfae863ff..a15d2ef1e 100644 --- a/src/math/polysat/solver.cpp +++ b/src/math/polysat/solver.cpp @@ -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;