From 073ee2672169a40163615811994c2140c982ff36 Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Tue, 14 Apr 2020 18:19:06 -0500
Subject: [PATCH] Disable macros when higher-order (#4266)

Fixes #4160.
---
 src/smt/set_defaults.cpp | 6 ++++++
 1 file changed, 6 insertions(+)

diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp
index a0f1b2715..1384a2848 100644
--- a/src/smt/set_defaults.cpp
+++ b/src/smt/set_defaults.cpp
@@ -864,6 +864,12 @@ void setDefaults(SmtEngine& smte, LogicInfo& logic)
       // by default, use store axioms only if --ho-elim is set
       options::hoElimStoreAx.set(options::hoElim());
     }
+    // Cannot use macros, since lambda lifting and macro elimination are inverse
+    // operations.
+    if (options::macrosQuant())
+    {
+      options::macrosQuant.set(false);
+    }
   }
   if (options::fmfFunWellDefinedRelevant())
   {
-- 
2.30.2