From 0eb0306ae2421a06d152720d8a724a843722efdf Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 27 Jan 2022 17:47:27 -0800 Subject: [PATCH] update comment Signed-off-by: Nikolaj Bjorner --- src/math/polysat/conflict.cpp | 6 ++---- 1 file changed, 2 insertions(+), 4 deletions(-) diff --git a/src/math/polysat/conflict.cpp b/src/math/polysat/conflict.cpp index bfcb5a125..2bd561dad 100644 --- a/src/math/polysat/conflict.cpp +++ b/src/math/polysat/conflict.cpp @@ -331,13 +331,11 @@ namespace polysat { m_vars.remove(v); - // TODO: side-conditions depend on variable assignments - // we need to track these when the side conditions are used - // or we need to propagate the side-conditions if they are not set. - // if (j.is_propagation()) { for (auto const& c : s.m_viable.get_constraints(v)) { if (!c->has_bvar()) { + // it is a side-condition that was not propagated already. + // it is true in the current variable assignment. cm().ensure_bvar(c.get()); s.assign_eval(c.blit()); }