From 181995a4fbd6de4b2e03328e977cfc05b6d21df0 Mon Sep 17 00:00:00 2001
From: Jakob Rath <git@jakobrath.eu>
Date: Mon, 9 Jan 2023 17:16:47 +0100
Subject: [PATCH] extend invariant check

---
 src/math/polysat/solver.cpp | 13 +++++++++----
 src/math/polysat/solver.h   |  2 +-
 2 files changed, 10 insertions(+), 5 deletions(-)

diff --git a/src/math/polysat/solver.cpp b/src/math/polysat/solver.cpp
index 7ee877bea..3328a89b2 100644
--- a/src/math/polysat/solver.cpp
+++ b/src/math/polysat/solver.cpp
@@ -210,7 +210,7 @@ namespace polysat {
             linear_propagate();
         SASSERT(wlist_invariant());
         SASSERT(bool_watch_invariant());
-        SASSERT(assignment_invariant());
+        SASSERT(eval_invariant());
     }
 
     /**
@@ -1486,7 +1486,7 @@ namespace polysat {
     }
 
     /** Check that boolean assignment and constraint evaluation are consistent */
-    bool solver::assignment_invariant() const {
+    bool solver::eval_invariant() const {
         if (is_conflict())
             return true;
         bool ok = true;
@@ -1510,11 +1510,16 @@ namespace polysat {
         if (is_conflict())
             return true;
         uint_set active;
+        bool ok = true;
         for (pvar v : m_free_pvars)
             active.insert(v);
-        for (auto const& [v, val] : assignment())
+        for (auto const& [v, val] : get_assignment()) {
+            if (active.contains(v)) {
+                ok = false;
+                LOG("Variable v" << v << " is in free var queue despite already assigned " << assignment_pp(*this, v, val));
+            }
             active.insert(v);
-        bool ok = true;
+        }
         for (pvar v = 0; v < num_vars(); ++v) {
             if (!active.contains(v)) {
                 ok = false;
diff --git a/src/math/polysat/solver.h b/src/math/polysat/solver.h
index 4eee7d120..59e3bd11a 100644
--- a/src/math/polysat/solver.h
+++ b/src/math/polysat/solver.h
@@ -314,7 +314,7 @@ namespace polysat {
         static bool invariant(signed_constraints const& cs);
         bool wlist_invariant() const;
         bool bool_watch_invariant() const;
-        bool assignment_invariant() const;
+        bool eval_invariant() const;
         bool var_queue_invariant() const;
         bool verify_sat();