From f0625b604acadab9d94e264a5013dc14ecb396f3 Mon Sep 17 00:00:00 2001
From: Jakob Rath <git@jakobrath.eu>
Date: Wed, 1 Feb 2023 11:12:13 +0100
Subject: [PATCH] Promote assertions to release mode

---
 src/math/polysat/solver.cpp | 6 ++----
 1 file changed, 2 insertions(+), 4 deletions(-)

diff --git a/src/math/polysat/solver.cpp b/src/math/polysat/solver.cpp
index 774f15793..91e7d7edb 100644
--- a/src/math/polysat/solver.cpp
+++ b/src/math/polysat/solver.cpp
@@ -723,9 +723,7 @@ namespace polysat {
     /// Verify the value we're trying to assign against the univariate solver
     void solver::assign_verify(pvar v, rational val, justification j) {
         SASSERT(j.is_decision() || j.is_propagation());
-#ifndef NDEBUG
         unsigned const old_size = m_search.size();
-#endif
         signed_constraint c;
         clause_ref lemma;
         {
@@ -746,8 +744,8 @@ namespace polysat {
                 LOG("Produced lemma: " << show_deref(lemma));
             }
         }
-        SASSERT(m_search.size() == old_size);
-        SASSERT(!m_search.get_assignment().contains(v));
+        VERIFY_EQ(m_search.size(), old_size);
+        VERIFY(!m_search.get_assignment().contains(v));
         if (lemma) {
             add_clause(*lemma);
             if (is_conflict()) {