From a8b433e6ac860486871c3e394b06022618bcb682 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Mon, 19 Jul 2021 15:58:10 -0700
Subject: [PATCH] #5331

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/solver/assertions/asserted_formulas.cpp | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/src/solver/assertions/asserted_formulas.cpp b/src/solver/assertions/asserted_formulas.cpp
index 816ccb4e1..be931ccd6 100644
--- a/src/solver/assertions/asserted_formulas.cpp
+++ b/src/solver/assertions/asserted_formulas.cpp
@@ -424,7 +424,8 @@ void asserted_formulas::apply_quasi_macros() {
     TRACE("before_quasi_macros", display(tout););
     vector<justified_expr> new_fmls;
     quasi_macros proc(m, m_macro_manager);
-    while (proc(m_formulas.size() - m_qhead,
+    while (m_qhead == 0 && 
+           proc(m_formulas.size() - m_qhead,
                 m_formulas.data() + m_qhead,
                 new_fmls)) {
         swap_asserted_formulas(new_fmls);