From 39c3f34a304f6b04af275ac25643fd68a346f5f9 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 21 Jul 2021 09:25:08 -0700 Subject: [PATCH] remove unused dependency --- src/ast/macros/quasi_macros.cpp | 7 +++---- src/solver/assertions/CMakeLists.txt | 1 - 2 files changed, 3 insertions(+), 5 deletions(-) diff --git a/src/ast/macros/quasi_macros.cpp b/src/ast/macros/quasi_macros.cpp index 2faf736b8..a3e6c61e7 100644 --- a/src/ast/macros/quasi_macros.cpp +++ b/src/ast/macros/quasi_macros.cpp @@ -110,10 +110,9 @@ bool quasi_macros::fully_depends_on(app * a, quantifier * q) const { // direct argument of a, i.e., a->get_arg(i) == v for some i bit_vector bitset; bitset.resize(q->get_num_decls(), false); - for (unsigned i = 0 ; i < a->get_num_args() ; i++) { - if (is_var(a->get_arg(i))) - bitset.set(to_var(a->get_arg(i))->get_idx(), true); - } + for (expr* arg : *a) + if (is_var(arg)) + bitset.set(to_var(arg)->get_idx(), true); for (unsigned i = 0; i < bitset.size() ; i++) { if (!bitset.get(i)) diff --git a/src/solver/assertions/CMakeLists.txt b/src/solver/assertions/CMakeLists.txt index 3e1c1c0e3..7cc320458 100644 --- a/src/solver/assertions/CMakeLists.txt +++ b/src/solver/assertions/CMakeLists.txt @@ -2,7 +2,6 @@ z3_add_component(solver_assertions SOURCES asserted_formulas.cpp COMPONENT_DEPENDENCIES - solver smt2parser smt_params )