From 2c94a3a1b399e2536f1abdaa3d2a38d5a5a35b3e Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Mon, 30 Sep 2024 13:09:01 -0700
Subject: [PATCH] fix build warnings

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/smt/smt_context.cpp    | 1 -
 src/smt/smt_lookahead.cpp  | 5 +----
 src/test/cnf_backbones.cpp | 1 -
 3 files changed, 1 insertion(+), 6 deletions(-)

diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp
index deee05f6d..722782591 100644
--- a/src/smt/smt_context.cpp
+++ b/src/smt/smt_context.cpp
@@ -2942,7 +2942,6 @@ namespace smt {
 
         if (!e_internalized(var))
             return;
-        enode* n = get_enode(var);
         theory* th = m_theories.get_plugin(s->get_family_id());
         if (!th) {
             IF_VERBOSE(5, verbose_stream() << "No theory is attached to variable " << mk_pp(var, m) << " := " << mk_pp(value, m) << "\n");
diff --git a/src/smt/smt_lookahead.cpp b/src/smt/smt_lookahead.cpp
index 8de3f2f34..221c2d0ea 100644
--- a/src/smt/smt_lookahead.cpp
+++ b/src/smt/smt_lookahead.cpp
@@ -79,7 +79,7 @@ namespace smt {
         compare comp(ctx);
         std::sort(vars.begin(), vars.end(), comp);
         
-        unsigned nf = 0, nc = 0, ns = 0, n = 0;
+        unsigned ns = 0, n = 0;
         for (bool_var v : vars) {
             if (!ctx.bool_var2expr(v)) 
                 continue;
@@ -98,7 +98,6 @@ namespace smt {
             if (inconsistent) {
                 ctx.assign(~lit, b_justification::mk_axiom(), false);
                 ctx.propagate();           
-                ++nf;
                 continue;
             }
 
@@ -114,7 +113,6 @@ namespace smt {
             if (inconsistent) {
                 ctx.assign(lit, b_justification::mk_axiom(), false);
                 ctx.propagate(); 
-                ++nf;
                 continue;
             }
             double score = score1 + score2 + 1024*score1*score2;
@@ -132,7 +130,6 @@ namespace smt {
                 best_v = v;
                 ns = 0;
             } 
-            ++nc;
             ++ns;
             if (ns > budget) {
                 break;
diff --git a/src/test/cnf_backbones.cpp b/src/test/cnf_backbones.cpp
index 32a8149bd..a764ed9cf 100644
--- a/src/test/cnf_backbones.cpp
+++ b/src/test/cnf_backbones.cpp
@@ -86,7 +86,6 @@ static void track_clauses(sat::solver const& src,
         dst.mk_var(false, true);
     }
     sat::literal_vector lits;
-    sat::literal lit;
     sat::clause * const * it  = src.begin_clauses();
     sat::clause * const * end = src.end_clauses();
     svector<sat::solver::bin_clause> bin_clauses;