From 543ad2f20577643ca534d964021edf1fbbad6b3a Mon Sep 17 00:00:00 2001
From: Jakob Rath <git@jakobrath.eu>
Date: Thu, 20 Jan 2022 17:46:23 +0100
Subject: [PATCH] skip unassigned variables when computing level

---
 src/math/polysat/solver.cpp | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/src/math/polysat/solver.cpp b/src/math/polysat/solver.cpp
index bd374bf36..7e93f7138 100644
--- a/src/math/polysat/solver.cpp
+++ b/src/math/polysat/solver.cpp
@@ -750,8 +750,10 @@ namespace polysat {
 
     void solver::assign_eval(sat::literal lit) {
         unsigned level = 0;
+        // NOTE: constraint may be evaluated even if some variables are still unassigned (e.g., 0*x doesn't depend on x).
         for (auto v : lit2cnstr(lit)->vars())
-            level = std::max(get_level(v), level);
+            if (is_assigned(v))
+                level = std::max(get_level(v), level);
         m_bvars.eval(lit, level);
         m_trail.push_back(trail_instr_t::assign_bool_i);
         m_search.push_boolean(lit);