diff --git a/src/sat/smt/polysat/viable.cpp b/src/sat/smt/polysat/viable.cpp
index b21a203a2..cd309fa8f 100644
--- a/src/sat/smt/polysat/viable.cpp
+++ b/src/sat/smt/polysat/viable.cpp
@@ -174,7 +174,8 @@ namespace polysat {
                 if (!e)
                     continue;
                 last = e;
-                update_value_to_high(val, e);
+                if (e->interval.is_proper())
+                   update_value_to_high(val, e);
                 m_explain.push_back({ e, val });
                 if (is_conflict()) {
                     m_explain_kind = explain_t::conflict;