diff --git a/src/ast/expr_abstract.cpp b/src/ast/expr_abstract.cpp
index d4dd8805f..d6593a2a3 100644
--- a/src/ast/expr_abstract.cpp
+++ b/src/ast/expr_abstract.cpp
@@ -58,7 +58,7 @@ void expr_abstractor::operator()(unsigned base, unsigned num_bound, expr* const*
             bool changed = false;
             m_args.reset();
             for (unsigned i = 0, e = a->get_num_args(); i < e; ++i) {
-                if (!m_map.find(a->get_arg(i), b)) {
+                if (!all_visited || !m_map.find(a->get_arg(i), b)) {
                     m_stack.push_back(a->get_arg(i));
                     all_visited = false;
                 }