From 0b04d88e3479d114d24173d71aa23992d620fe74 Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Tue, 21 Aug 2018 16:38:26 -0500
Subject: [PATCH] Warn and enable quantifiers when using sygus + logics with QF
 (#2352)

---
 src/parser/smt2/smt2.cpp | 6 ++++++
 1 file changed, 6 insertions(+)

diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index 0a93beb2e..778766a61 100644
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -468,8 +468,14 @@ void Smt2::setLogic(std::string name) {
   // if sygus is enabled, we must enable UF, datatypes, integer arithmetic and
   // higher-order
   if(sygus()) {
+    if (!d_logic.isQuantified())
+    {
+      warning("Logics in sygus are assumed to contain quantifiers.");
+      warning("Omit QF_ from the logic to avoid this warning.");
+    }
     // get unlocked copy, modify, copy and relock
     LogicInfo log(d_logic.getUnlockedCopy());
+    log.enableQuantifiers();
     log.enableTheory(theory::THEORY_UF);
     log.enableTheory(theory::THEORY_DATATYPES);
     log.enableIntegers();
-- 
2.30.2