mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-06 09:34:08 +00:00
Code Activity

unused variable warnings

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2019-09-22 10:15:20 -07:00
parent 5919bc0531
commit a44cf7a9ba
2 changed files with 0 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/smt/theory_datatype.cpp
View file

@ -565,7 +565,6 @@ namespace smt {
// start exploring subgraph below `app` // start exploring subgraph below `app`
bool theory_datatype::occurs_check_enter(enode * app) { bool theory_datatype::occurs_check_enter(enode * app) {
context& ctx = get_context();
app = app->get_root(); app = app->get_root();
theory_var v = app->get_th_var(get_id()); theory_var v = app->get_th_var(get_id());
if (v == null_theory_var) { if (v == null_theory_var) {
@ -759,7 +758,6 @@ namespace smt {
SASSERT(d->m_constructor); SASSERT(d->m_constructor);
func_decl * c_decl = d->m_constructor->get_decl(); func_decl * c_decl = d->m_constructor->get_decl();
datatype_value_proc * result = alloc(datatype_value_proc, c_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)) { for (enode* arg : enode::args(d->m_constructor)) {
result->add_dependency(arg); result->add_dependency(arg);
} }

1
src/tactic/fd_solver/smtfd_solver.cpp
View file

@ -860,7 +860,6 @@ namespace smtfd {
Enforce M[x] == rewrite(M[x]) for every A[x] such that M = A under current model. Enforce M[x] == rewrite(M[x]) for every A[x] such that M = A under current model.
*/ */
void beta_reduce(expr* t) { void beta_reduce(expr* t) {
bool added = false;
if (m_autil.is_map(t) || if (m_autil.is_map(t) ||
m_autil.is_const(t) || m_autil.is_const(t) ||
is_lambda(t)) { is_lambda(t)) {