From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Tue, 21 Aug 2018 21:38:26 +0000 (-0500)
Subject: Warn and enable quantifiers when using sygus + logics with QF (#2352)
X-Git-Tag: cvc5-1.0.0~4746
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=0b04d88e3479d114d24173d71aa23992d620fe74;p=cvc5.git

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