From a44cf7a9bab5a50f00108519321098187b1ad14f Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 22 Sep 2019 10:15:20 -0700 Subject: [PATCH] unused variable warnings Signed-off-by: Nikolaj Bjorner --- src/smt/theory_datatype.cpp | 2 -- src/tactic/fd_solver/smtfd_solver.cpp | 1 - 2 files changed, 3 deletions(-) diff --git a/src/smt/theory_datatype.cpp b/src/smt/theory_datatype.cpp index 959ce6f14..6af48b823 100644 --- a/src/smt/theory_datatype.cpp +++ b/src/smt/theory_datatype.cpp @@ -565,7 +565,6 @@ namespace smt { // start exploring subgraph below `app` bool theory_datatype::occurs_check_enter(enode * app) { - context& ctx = get_context(); app = app->get_root(); theory_var v = app->get_th_var(get_id()); if (v == null_theory_var) { @@ -759,7 +758,6 @@ namespace smt { SASSERT(d->m_constructor); func_decl * c_decl = d->m_constructor->get_decl(); datatype_value_proc * result = alloc(datatype_value_proc, c_decl); - unsigned num = d->m_constructor->get_num_args(); for (enode* arg : enode::args(d->m_constructor)) { result->add_dependency(arg); } diff --git a/src/tactic/fd_solver/smtfd_solver.cpp b/src/tactic/fd_solver/smtfd_solver.cpp index 62058e0e9..33b66639b 100644 --- a/src/tactic/fd_solver/smtfd_solver.cpp +++ b/src/tactic/fd_solver/smtfd_solver.cpp @@ -860,7 +860,6 @@ namespace smtfd { Enforce M[x] == rewrite(M[x]) for every A[x] such that M = A under current model. */ void beta_reduce(expr* t) { - bool added = false; if (m_autil.is_map(t) || m_autil.is_const(t) || is_lambda(t)) {