From 8a30128933a1cdc638fbadd0c89361a580fae45b Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Thu, 13 Oct 2022 15:20:24 +0200
Subject: [PATCH] formatting updates

---
 src/ast/macros/quasi_macros.cpp | 15 +++++++--------
 1 file changed, 7 insertions(+), 8 deletions(-)

diff --git a/src/ast/macros/quasi_macros.cpp b/src/ast/macros/quasi_macros.cpp
index 2920c9667..dff36278d 100644
--- a/src/ast/macros/quasi_macros.cpp
+++ b/src/ast/macros/quasi_macros.cpp
@@ -114,10 +114,9 @@ bool quasi_macros::fully_depends_on(app * a, quantifier * q) const {
         if (is_var(arg))
              bitset.set(to_var(arg)->get_idx(), true);
 
-    for (unsigned i = 0; i < bitset.size() ; i++) {
+    for (unsigned i = 0; i < bitset.size() ; i++) 
         if (!bitset.get(i))
-            return false;
-    }
+            return false;    
 
     return true;
 }
@@ -167,18 +166,18 @@ bool quasi_macros::is_quasi_macro(expr * e, app_ref & a, expr_ref & t) const {
         quantifier * q = to_quantifier(e);
         expr * qe = q->get_expr(), *lhs = nullptr, *rhs = nullptr;
         if (m.is_eq(qe, lhs, rhs)) {
-	  if (is_quasi_def(q, lhs, rhs)) {
+            if (is_quasi_def(q, lhs, rhs)) {
 	        a = to_app(lhs);
                 t = rhs;
                 return true;
-	  } else if (is_quasi_def(q, rhs, lhs)) {
+            } else if (is_quasi_def(q, rhs, lhs)) {
 	        a = to_app(rhs);
                 t = lhs;
                 return true;
             }
         }
 	else if (m.is_not(qe, lhs) && is_non_ground_uninterp(lhs) &&
-                   is_unique(to_app(lhs)->get_decl())) { // this is like f(...) = false
+                 is_unique(to_app(lhs)->get_decl())) { // this is like f(...) = false
             a = to_app(lhs);
             t = m.mk_false();
             return true;
@@ -189,8 +188,8 @@ bool quasi_macros::is_quasi_macro(expr * e, app_ref & a, expr_ref & t) const {
             return true;
         }
 	else if (m.is_not(qe, lhs) && m.is_eq(lhs, lhs, rhs) && m.is_bool(lhs)) {
-	  if (is_quasi_def(q, lhs, rhs)) {
-	        a = to_app(lhs);
+            if (is_quasi_def(q, lhs, rhs)) {
+                a = to_app(lhs);
                 t = m.mk_not(rhs);
                 return true;
             } else if (is_quasi_def(q, rhs, lhs)) {