From c1d58088bed8467c08f55c3284cf4573e77a4ad5 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Wed, 10 Nov 2021 01:42:04 -0800
Subject: [PATCH] na

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/math/polysat/conflict.cpp |  2 +-
 src/test/polysat.cpp          | 11 ++++++++---
 src/util/uint_set.h           |  2 +-
 3 files changed, 10 insertions(+), 5 deletions(-)

diff --git a/src/math/polysat/conflict.cpp b/src/math/polysat/conflict.cpp
index 785d2bebb..822d7dcc4 100644
--- a/src/math/polysat/conflict.cpp
+++ b/src/math/polysat/conflict.cpp
@@ -226,7 +226,7 @@ namespace polysat {
     }
 
     clause_builder conflict::build_lemma() {
-        SASSERT(std::all_of(m_vars.begin(), m_vars.end(), [&](pvar v) { return s.is_assigned(v); }));
+        // SASSERT(std::all_of(m_vars.begin(), m_vars.end(), [&](pvar v) { return s.is_assigned(v); }));
         SASSERT(std::all_of(m_constraints.begin(), m_constraints.end(), [](signed_constraint const& c) { return !c->has_bvar(); }));
 
         LOG_H3("Build lemma from core");
diff --git a/src/test/polysat.cpp b/src/test/polysat.cpp
index 1dff7bfb8..27dae3151 100644
--- a/src/test/polysat.cpp
+++ b/src/test/polysat.cpp
@@ -1076,9 +1076,6 @@ void tst_polysat() {
     polysat::test_ineq_axiom5();
     polysat::test_ineq_axiom6();
 
-    // not working
-    // polysat::test_fixed_point_arith_div_mul_inverse();    
-    // polysat::test_monot_bounds_simple(8);
 
     // working
     // NOT: polysat::test_fixed_point_arith_mul_div_inverse();
@@ -1127,6 +1124,14 @@ void tst_polysat() {
     polysat::test_ineq1();
     polysat::test_ineq2();
 #endif
+
+    // not working
+    polysat::test_monot_bounds_simple(8);
+    polysat::test_fixed_point_arith_div_mul_inverse();
+    polysat::test_monot();
+    polysat::test_ineq2();
+    polysat::test_ineq1();
+
 }
 
 
diff --git a/src/util/uint_set.h b/src/util/uint_set.h
index 2b7e36360..6e64cc7ae 100644
--- a/src/util/uint_set.h
+++ b/src/util/uint_set.h
@@ -192,7 +192,7 @@ public:
             m_set(&s), m_index(at_end?s.get_max_elem():0), m_last(s.get_max_elem()) {
             scan();
             SASSERT(invariant());
-          }
+        }
         unsigned operator*() const { return m_index; }
         bool operator==(iterator const& it) const { return m_index == it.m_index; }
         bool operator!=(iterator const& it) const { return m_index != it.m_index; }