Disable macros when higher-order (#4266)

Fixes #4160.

diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp
index a0f1b271590a8b2a2269cd48aeba066fb6c57784..1384a28487ae01f7cf4cefdd475ae00f842bdee8 100644 (file)
--- 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())
   {