From 0e20198473c6701e24886eef606144a0917b6694 Mon Sep 17 00:00:00 2001 From: Jakob Rath Date: Fri, 17 Mar 2023 23:58:47 +0100 Subject: [PATCH] should eval new constraints --- src/math/polysat/conflict.cpp | 10 ++++++++-- 1 file changed, 8 insertions(+), 2 deletions(-) diff --git a/src/math/polysat/conflict.cpp b/src/math/polysat/conflict.cpp index 293423d68..ea178be38 100644 --- a/src/math/polysat/conflict.cpp +++ b/src/math/polysat/conflict.cpp @@ -415,8 +415,14 @@ namespace polysat { for (signed_constraint const c : s.m_viable.get_constraints(v)) insert(c); for (auto const& i : s.m_viable.units(v)) { - insert(s.eq(i.lo(), i.lo_val())); - insert(s.eq(i.hi(), i.hi_val())); + signed_constraint eq1 = s.eq(i.lo(), i.lo_val()); + signed_constraint eq2 = s.eq(i.hi(), i.hi_val()); + if (eq1.bvalue(s) == l_undef) + s.assign_eval(eq1.blit()); + if (eq2.bvalue(s) == l_undef) + s.assign_eval(eq2.blit()); + insert(eq1); + insert(eq2); } logger().log(inf_resolve_value(s, v));