From 7b845c71382124201e001205cd7c81443c78ea64 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Tue, 2 Nov 2021 19:26:48 -0700
Subject: [PATCH] build warnings

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/math/polysat/conflict.cpp  | 4 ++--
 src/math/polysat/fixplex_def.h | 4 ++--
 src/test/fixplex.cpp           | 6 +++---
 3 files changed, 7 insertions(+), 7 deletions(-)

diff --git a/src/math/polysat/conflict.cpp b/src/math/polysat/conflict.cpp
index 00659aa04..a7b17ddbd 100644
--- a/src/math/polysat/conflict.cpp
+++ b/src/math/polysat/conflict.cpp
@@ -191,7 +191,7 @@ namespace polysat {
 
         SASSERT(lit != sat::null_literal);
         SASSERT(~lit != sat::null_literal);
-        SASSERT(std::all_of(m_constraints.begin(), m_constraints.end(), [](auto c){ return !c->has_bvar(); }));
+        SASSERT(std::all_of(m_constraints.begin(), m_constraints.end(), [](signed_constraint const& c){ return !c->has_bvar(); }));
         SASSERT(contains_literal(lit));
         SASSERT(std::count(cl.begin(), cl.end(), lit) > 0);
         SASSERT(!contains_literal(~lit));
@@ -219,7 +219,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_constraints.begin(), m_constraints.end(), [](auto c) { return !c->has_bvar(); }));
+        SASSERT(std::all_of(m_constraints.begin(), m_constraints.end(), [](signed_constraint const& c) { return !c->has_bvar(); }));
 
         LOG_H3("Build lemma from core");
         LOG("core: " << *this);
diff --git a/src/math/polysat/fixplex_def.h b/src/math/polysat/fixplex_def.h
index fa251d355..1464811b7 100644
--- a/src/math/polysat/fixplex_def.h
+++ b/src/math/polysat/fixplex_def.h
@@ -1335,7 +1335,7 @@ namespace polysat {
     template<typename Ext>
     bool fixplex<Ext>::propagate_strict_bounds(ineq const& i) {
         var_t v = i.v, w = i.w;
-        bool s = i.strict;
+        //bool s = i.strict;
         auto* vlo = m_vars[v].m_lo_dep, *vhi = m_vars[v].m_hi_dep;
         auto* wlo = m_vars[w].m_lo_dep, *whi = m_vars[w].m_hi_dep;
 
@@ -1363,7 +1363,7 @@ namespace polysat {
     template<typename Ext>
     bool fixplex<Ext>::propagate_non_strict_bounds(ineq const& i) {
         var_t v = i.v, w = i.w;
-        bool s = i.strict;
+        // bool s = i.strict;
         auto* vlo = m_vars[v].m_lo_dep, *vhi = m_vars[v].m_hi_dep;
         auto* wlo = m_vars[w].m_lo_dep, *whi = m_vars[w].m_hi_dep;
 
diff --git a/src/test/fixplex.cpp b/src/test/fixplex.cpp
index c6c4bf925..e0667ee26 100644
--- a/src/test/fixplex.cpp
+++ b/src/test/fixplex.cpp
@@ -389,7 +389,7 @@ namespace polysat {
         std::cout << "    test_lp(rows, ineqs, bounds); \n }\n";
     }
 
-    static unsigned num_test = 0;
+    //    static unsigned num_test = 0;
 
     static void test_lp(
         vector<svector<std::pair<unsigned, uint64_t>>> const& rows,
@@ -566,9 +566,9 @@ namespace polysat {
 
     static void test_lps() {
         random_gen r;
-    	for (unsigned i = 0; i < 10000; ++i)
+    	for (unsigned i = 0; i < 10000; ++i) 
             test_lps(r, 6, 3, 3, 3);
-	    return;
+        return;
         for (unsigned i = 0; i < 10000; ++i)
             test_lps(r, 6, 3, 3, 0);
         return;