fix build warnings

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

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");

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;

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;