From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Tue, 14 Apr 2020 23:19:06 +0000 (-0500)
Subject: Disable macros when higher-order (#4266)
X-Git-Tag: cvc5-1.0.0~3374
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=073ee2672169a40163615811994c2140c982ff36;p=cvc5.git

Disable macros when higher-order (#4266)

Fixes #4160.
---

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())
   {