na

Signed-off-by: Nikolaj Bjorner <[email protected]>

src/math/lp/lp_bound_propagator.h

@@ -190,7 +190,7 @@ class lp_bound_propagator {
     void try_add_equation_with_lp_fixed_tables(const vertex *v) {
         SASSERT(m_fixed_vertex);
         unsigned v_j = v->column();
-        unsigned j;
+        unsigned j = null_lpvar;
         if (!lp().find_in_fixed_tables(val(v_j), is_int(v_j), j)) 
             return;
         TRACE("cheap_eq", tout << "found j=" << j << " for v=";

src/smt/smt_quantifier.cpp

@@ -206,9 +206,9 @@ namespace smt {
         }
 
         void log_causality(
-                fingerprint* f,
-                app * pat,
-                vector<std::tuple<enode *, enode *>> & used_enodes) {
+            fingerprint* f,
+            app * pat,
+            vector<std::tuple<enode *, enode *>> & used_enodes) {
 
             if (pat != nullptr) {
                 if (used_enodes.size() > 0) {
@@ -219,6 +219,7 @@ namespace smt {
                 for (auto n : used_enodes) {
                     enode *orig = std::get<0>(n);
                     enode *substituted = std::get<1>(n);
+                    (void) substituted;
                     if (orig == nullptr) {
                         STRACE("causality", tout << " #" << substituted->get_owner_id(););
                     }

src/smt/theory_bv.cpp

@@ -1139,7 +1139,6 @@ namespace smt {
             bool_var watch_var = null_bool_var;
             it1 = bits1.begin();
             it2 = bits2.begin();
-            unsigned h = hash_u_u(v1, v2);
             unsigned act = m_diseq_activity[hash_u_u(v1, v2) & 0xFF]++;
 
             for (; it1 != end1 && ((act & 0x3) != 0x3); ++it1, ++it2) {

src/test/egraph.cpp

@@ -3,6 +3,7 @@ Copyright (c) 2020 Microsoft Corporation
 
 --*/
 
+#include "util/util.h"
 #include "util/timer.h"
 #include "ast/euf/euf_egraph.h"
 #include "ast/reg_decl_plugins.h"
@@ -15,13 +16,13 @@ static expr_ref mk_const(ast_manager& m, char const* name, sort* s) {
 static expr_ref mk_app(char const* name, expr_ref const& arg, sort* s) {
     ast_manager& m = arg.m();
     func_decl_ref f(m.mk_func_decl(symbol(name), m.get_sort(arg), s), m);
-    return expr_ref(m.mk_app(f, arg), m);
+    return expr_ref(m.mk_app(f, arg.get()), m);
 }
 
 static expr_ref mk_app(char const* name, expr_ref const& arg1, expr_ref const& arg2, sort* s) {
     ast_manager& m = arg1.m();
     func_decl_ref f(m.mk_func_decl(symbol(name), m.get_sort(arg1), m.get_sort(arg2), s), m);
-    return expr_ref(m.mk_app(f, arg1, arg2), m);
+    return expr_ref(m.mk_app(f, arg1.get(), arg2.get()), m);
 }
 
 static void test1() {