From 296a97d0d373941a8f646b46776e958de2129685 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sun, 5 Apr 2020 01:03:38 -0700
Subject: [PATCH] build

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/smt/dyn_ack.cpp            | 1 +
 src/smt/theory_lra.cpp         | 3 +--
 src/solver/parallel_tactic.cpp | 6 +++---
 src/test/lp/lp.cpp             | 2 +-
 4 files changed, 6 insertions(+), 6 deletions(-)

diff --git a/src/smt/dyn_ack.cpp b/src/smt/dyn_ack.cpp
index 835e0d09c..2fe547cf7 100644
--- a/src/smt/dyn_ack.cpp
+++ b/src/smt/dyn_ack.cpp
@@ -145,6 +145,7 @@ namespace smt {
             if (m_eq1->get_arg(1) == m_app1) p1 = m.mk_symmetry(p1);
             p2 = m.mk_hypothesis(m_eq2);
             if (m_eq2->get_arg(0) == m_app2) p2 = m.mk_symmetry(p2);
+            (void)m_r;
             SASSERT(m.is_eq(m.get_fact(p1), x, y) && x == m_app1 && y == m_r);
             SASSERT(m.is_eq(m.get_fact(p2), x, y) && x == m_r && y == m_app2);
             p3 = m.mk_transitivity(p1, p2);
diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp
index d22e46f19..402949c6f 100644
--- a/src/smt/theory_lra.cpp
+++ b/src/smt/theory_lra.cpp
@@ -2513,7 +2513,6 @@ public:
 
 
     void mk_bound_axiom(lp_api::bound& b1, lp_api::bound& b2) {
-        theory_var v = b1.get_var();
         literal   l1(b1.get_bv());
         literal   l2(b2.get_bv());
         rational const& k1 = b1.get_value();
@@ -2521,7 +2520,7 @@ public:
         lp_api::bound_kind kind1 = b1.get_bound_kind();
         lp_api::bound_kind kind2 = b2.get_bound_kind();
         bool v_is_int = b1.is_int();
-        SASSERT(v == b2.get_var());
+        SASSERT(b1.get_var() == b2.get_var());
         if (k1 == k2 && kind1 == kind2) return;
         SASSERT(k1 != k2 || kind1 != kind2);
         parameter coeffs[3] = { parameter(symbol("farkas")), 
diff --git a/src/solver/parallel_tactic.cpp b/src/solver/parallel_tactic.cpp
index b9bc77ad6..67e91d5f9 100644
--- a/src/solver/parallel_tactic.cpp
+++ b/src/solver/parallel_tactic.cpp
@@ -236,7 +236,7 @@ class parallel_tactic : public tactic {
         vector<cube_var> split_cubes(unsigned n) {
             vector<cube_var> result;
             while (n-- > 0 && !m_cubes.empty()) {
-                for (expr* c : m_cubes.back().cube()) SASSERT(c);
+                DEBUG_CODE(for (expr* c : m_cubes.back().cube()) SASSERT(c););
                 result.push_back(m_cubes.back());
 
                 m_cubes.pop_back();
@@ -246,7 +246,7 @@ class parallel_tactic : public tactic {
 
         void set_cubes(vector<cube_var>& c) {
             m_cubes.reset();
-            for (auto & cb : c) for (expr* e : cb.cube()) SASSERT(e);
+            DEBUG_CODE(for (auto & cb : c) for (expr* e : cb.cube()) SASSERT(e););
             m_cubes.append(c);
         }
 
@@ -517,7 +517,7 @@ private:
             if (conquer) {
                 is_sat = conquer->check_sat(c);
             }
-            for (expr* e : c) SASSERT(e);
+            DEBUG_CODE(for (expr* e : c) SASSERT(e););
             switch (is_sat) {
             case l_false: 
                 cutoff = c.size();
diff --git a/src/test/lp/lp.cpp b/src/test/lp/lp.cpp
index 1d2bef52d..2798d357c 100644
--- a/src/test/lp/lp.cpp
+++ b/src/test/lp/lp.cpp
@@ -43,7 +43,7 @@
 #include "math/lp/lar_solver.h"
 #include "math/lp/numeric_pair.h"
 #include "math/lp/binary_heap_upair_queue.h"
-#include "math/lp/stacked_value.h"
+#include "util/stacked_value.h"
 #include "math/lp/u_set.h"
 #include "util/stopwatch.h"
 #include <cstdlib>