From 4dfdabc80f4f5d91ebfff2a1b1e3e9efb8ada0ce Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sun, 31 Jan 2021 16:36:55 -0800
Subject: [PATCH] na

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/sat/smt/q_ematch.h  | 2 +-
 src/sat/smt/q_queue.cpp | 3 +--
 src/util/zstring.cpp    | 8 --------
 3 files changed, 2 insertions(+), 11 deletions(-)

diff --git a/src/sat/smt/q_ematch.h b/src/sat/smt/q_ematch.h
index e3db84d4e..9cc7b4baa 100644
--- a/src/sat/smt/q_ematch.h
+++ b/src/sat/smt/q_ematch.h
@@ -127,7 +127,7 @@ namespace q {
         void on_binding(quantifier* q, app* pat, euf::enode* const* binding, unsigned max_generation, unsigned min_gen, unsigned max_gen);
 
         // callback from queue
-        lbool eval(euf::enode* const* binding, clause& c) { return m_eval(binding, c); }
+        lbool evaluate(euf::enode* const* binding, clause& c) { return m_eval(binding, c); }
         void add_instantiation(clause& c, binding& b, sat::literal lit);
         bool propagate(euf::enode* const* binding, unsigned max_generation, clause& c);
 
diff --git a/src/sat/smt/q_queue.cpp b/src/sat/smt/q_queue.cpp
index 68a81a20d..8730a9b67 100644
--- a/src/sat/smt/q_queue.cpp
+++ b/src/sat/smt/q_queue.cpp
@@ -137,7 +137,6 @@ namespace q {
     void queue::instantiate(entry& ent) {
         fingerprint & f          = *ent.m_qb;
         quantifier * q           = f.q();
-        unsigned generation      = f.m_max_generation;
         unsigned num_bindings    = f.size();
         euf::enode * const * bindings = f.nodes();
         q::quantifier_stat * stat = f.c->m_stat;
@@ -181,7 +180,7 @@ namespace q {
 
             if (curr.m_cost <= m_eager_cost_threshold) 
                 instantiate(curr);
-            else if (m_params.m_qi_promote_unsat && l_false == em.eval(f.nodes(), *f.c)) {
+            else if (m_params.m_qi_promote_unsat && l_false == em.evaluate(f.nodes(), *f.c)) {
                 // do not delay instances that produce a conflict.
                 TRACE("q", tout << "promoting instance that produces a conflict\n" << mk_pp(f.q(), m) << "\n";);
                 instantiate(curr);
diff --git a/src/util/zstring.cpp b/src/util/zstring.cpp
index a980bc1d0..c837ab6cb 100644
--- a/src/util/zstring.cpp
+++ b/src/util/zstring.cpp
@@ -33,14 +33,6 @@ static bool is_hex_digit(char ch, unsigned& d) {
     return false;
 }
 
-static bool is_octal_digit(char ch, unsigned& d) {
-    if ('0' <= ch && ch <= '7') {
-        d = ch - '0';
-        return true;
-    }
-    return false;
-}
-
 bool zstring::is_escape_char(char const *& s, unsigned& result) {
     unsigned d;
     if (*s == '\\' && *(s+1) == 'u' && *(s+2) == '{') {