From 920f494a0cb8f801a01ff176648076bf2b26893b Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 9 Dec 2023 16:20:35 -0800 Subject: [PATCH] fixed fixme Signed-off-by: Nikolaj Bjorner --- src/sat/smt/polysat/polysat_viable.cpp | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/src/sat/smt/polysat/polysat_viable.cpp b/src/sat/smt/polysat/polysat_viable.cpp index 8d9009af0..9af70d716 100644 --- a/src/sat/smt/polysat/polysat_viable.cpp +++ b/src/sat/smt/polysat/polysat_viable.cpp @@ -637,8 +637,9 @@ namespace polysat { if (c.is_assigned(v)) return; auto [sc, d, value] = c.m_constraint_index[idx]; - // fixme: constraint must be assigned a value l_true or l_false at this point. - // adjust sc to the truth value of the constraint when passed to forbidden intervals. + SASSERT(value != l_undef); + if (value == l_false) + sc = ~sc; entry* ne = alloc_entry(v, idx); if (!m_forbidden_intervals.get_interval(sc, v, *ne)) {