diff --git a/src/tactic/sine_filter.cpp b/src/tactic/sine_filter.cpp index f5ecc36a3..71ae58f8c 100644 --- a/src/tactic/sine_filter.cpp +++ b/src/tactic/sine_filter.cpp @@ -98,8 +98,8 @@ private: if (is_app(curr)) { app *a = to_app(curr); func_decl *f = a->get_decl(); - if (is_name(f) && !consts.contains(f)) { - consts.insert(f); + if (is_name(f)) { + consts.insert_if_not_there(f); } } }