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 )