diff --git a/src/ast/macros/quasi_macros.cpp b/src/ast/macros/quasi_macros.cpp
index 3a22758c7..1bc20d1b9 100644
--- a/src/ast/macros/quasi_macros.cpp
+++ b/src/ast/macros/quasi_macros.cpp
@@ -158,8 +158,7 @@ bool quasi_macros::is_quasi_macro(expr * e, app_ref & a, expr_ref & t) const {
     if (is_forall(e)) {
         quantifier * q = to_quantifier(e);
         expr * qe = q->get_expr(), *lhs = nullptr, *rhs = nullptr;
-        if ((m.is_eq(qe, lhs, rhs))) {
-
+        if (m.is_eq(qe, lhs, rhs)) {
             if (is_non_ground_uninterp(lhs) && is_unique(to_app(lhs)->get_decl()) &&
                 !depends_on(rhs, to_app(lhs)->get_decl()) && fully_depends_on(to_app(lhs), q)) {
                 a = to_app(lhs);
@@ -293,24 +292,22 @@ bool quasi_macros::find_macros(unsigned n, expr * const * exprs) {
 
 bool quasi_macros::find_macros(unsigned n, justified_expr const * exprs) {
     TRACE("quasi_macros", tout << "Finding quasi-macros in: " << std::endl;
-                          for (unsigned i = 0 ; i < n ; i++)
-                              tout << i << ": " << mk_pp(exprs[i].get_fml(), m) << std::endl; );
+          for (unsigned i = 0; i < n; i++)
+              tout << i << ": " << mk_pp(exprs[i].get_fml(), m) << std::endl; );
     bool res = false;
     m_occurrences.reset();
 
 
     // Find out how many non-ground appearances for each uninterpreted function there are
-    for ( unsigned i = 0 ; i < n ; i++ )
+    for (unsigned i = 0 ; i < n ; i++)
         find_occurrences(exprs[i].get_fml());
 
     TRACE("quasi_macros", tout << "Occurrences: " << std::endl;
-    for (occurrences_map::iterator it = m_occurrences.begin();
-         it != m_occurrences.end();
-         it++)
-        tout << it->m_key->get_name() << ": " << it->m_value << std::endl; );
+          for (auto kv : m_occurrences) 
+              tout << kv.m_key->get_name() << ": " << kv.m_value << std::endl; );
 
     // Find all macros
-    for ( unsigned i = 0 ; i < n ; i++ ) {
+    for (unsigned i = 0 ; i < n ; i++) {
         app_ref a(m);
         expr_ref t(m);
         quantifier_ref macro(m);
@@ -370,6 +367,7 @@ void quasi_macros::apply_macros(unsigned n, justified_expr const* fmls, vector<j
 }
 
 bool quasi_macros::operator()(unsigned n, justified_expr const* fmls, vector<justified_expr>& new_fmls) {
+    TRACE("quasi_macros", m_macro_manager.display(tout););
     if (find_macros(n, fmls)) {
         apply_macros(n, fmls, new_fmls);
         return true;
diff --git a/src/smt/asserted_formulas.h b/src/smt/asserted_formulas.h
index 570d0ffde..59f83a34f 100644
--- a/src/smt/asserted_formulas.h
+++ b/src/smt/asserted_formulas.h
@@ -88,7 +88,7 @@ class asserted_formulas {
     public:
         find_macros_fn(asserted_formulas& af): simplify_fmls(af, "find-macros") {}
         void operator()() override { af.find_macros_core(); }
-        bool should_apply() const override { return af.m_smt_params.m_macro_finder && af.has_quantifiers(); }
+        bool should_apply() const override { return (af.m_smt_params.m_quasi_macros || af.m_smt_params.m_macro_finder) && af.has_quantifiers(); }
         void simplify(justified_expr const& j, expr_ref& n, proof_ref& p) override { UNREACHABLE(); }
     };