Warn and enable quantifiers when using sygus + logics with QF (#2352)

diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index 0a93beb2e58d4beb42ccf9af24b3bcd3bc4a6548..778766a61b45723cf69c19508740256362a4c071 100644 (file)
--- 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();