diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-08-21 16:38:26 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2018-08-21 16:38:26 -0500 |
commit | 0b04d88e3479d114d24173d71aa23992d620fe74 (patch) | |
tree | 0f788f906a9e010b7570f27d1610e9a0253a9af9 | |
parent | a1b769fcb9ecdab7c09d7d7f05e4f87f54133076 (diff) |
Warn and enable quantifiers when using sygus + logics with QF (#2352)
-rw-r--r-- | src/parser/smt2/smt2.cpp | 6 |
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(); |