Add support for set-logic ALL, fix compiler error in GCC 6.1

3 files changed, 8 insertions, 6 deletions

diff --git a/src/parser/smt1/smt1.cpp b/src/parser/smt1/smt1.cpp
index 50f62009a..015129f10 100644
--- a/src/parser/smt1/smt1.cpp
+++ b/src/parser/smt1/smt1.cpp
@@ -62,6 +62,8 @@ std::hash_map<const std::string, Smt1::Logic, CVC4::StringHashFunction> Smt1::ne
   logicMap["UFLRA"] = UFLRA;
   logicMap["QF_ALL_SUPPORTED"] = QF_ALL_SUPPORTED;
   logicMap["ALL_SUPPORTED"] = ALL_SUPPORTED;
+  logicMap["QF_ALL"] = QF_ALL_SUPPORTED;
+  logicMap["ALL"] = ALL_SUPPORTED;
   return logicMap;
 }
 
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index 27c5a62bd..ff34fd9a3 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -272,7 +272,7 @@ command [CVC4::PtrCloser<CVC4::Command>* cmd]
       }
       PARSER_STATE->setLogic(name);
       if( PARSER_STATE->sygus() ){
-        cmd->reset(new SetBenchmarkLogicCommand("ALL_SUPPORTED"));
+        cmd->reset(new SetBenchmarkLogicCommand("ALL"));
       }else{
         cmd->reset(new SetBenchmarkLogicCommand(name));
       }
diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index 8db344f92..2e2481a6e 100644
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -370,7 +370,7 @@ void Smt2::setLogic(std::string name) {
       name = "UFSLIA";
     } else if(name == "SAT") {
       name = "UF";
-    } else if(name == "ALL_SUPPORTED") {
+    } else if(name == "ALL" || name == "ALL_SUPPORTED") {
       //no change
     } else {
       std::stringstream ss;
@@ -456,14 +456,14 @@ void Smt2::checkThatLogicIsSet() {
         setLogic("LIA");
       } else {
         warning("No set-logic command was given before this point.");
-        warning("CVC4 will assume the non-standard ALL_SUPPORTED logic.");
+        warning("CVC4 will make all theories available.");
         warning("Consider setting a stricter logic for (likely) better performance.");
-        warning("To suppress this warning in the future use (set-logic ALL_SUPPORTED).");
+        warning("To suppress this warning in the future use (set-logic ALL).");
 
-        setLogic("ALL_SUPPORTED");
+        setLogic("ALL");
       }
 
-      Command* c = new SetBenchmarkLogicCommand("ALL_SUPPORTED");
+      Command* c = new SetBenchmarkLogicCommand("ALL");
       c->setMuted(true);
       preemptCommand(c);
     }