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

1 files changed, 6 insertions, 0 deletions

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