Adding support for QF_UFLIA to the smt2 parser.

diff --git a/src/parser/smt/smt.cpp b/src/parser/smt/smt.cpp
index a6e716b77ebeab02b30b58d734d847ed86c4bb83..e0d1922c8ee0de2b2e4a5b525cf067e7bbaf7972 100644 (file)
--- a/src/parser/smt/smt.cpp
+++ b/src/parser/smt/smt.cpp
@@ -40,6 +40,7 @@ std::hash_map<const std::string, Smt::Logic, CVC4::StringHashFunction> Smt::newL
   logicMap["QF_UF"] = QF_UF;
   logicMap["QF_UFIDL"] = QF_UFIDL;
   logicMap["QF_UFLRA"] = QF_UFLRA;
+  logicMap["QF_UFLIA"] = QF_UFLIA;
   return logicMap;
 }
 

diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index 4bc90ec8f3340522281f291601a8550f2c7bc5be..08a824c0a40da525393ff90b499b2ea5c487e194 100644 (file)
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -126,11 +126,11 @@ void Smt2::setLogic(const std::string& name) {
     break;
 
   case Smt::QF_UFIDL:
+  case Smt::QF_UFLIA:
     addTheory(THEORY_INTS);
     addOperator(kind::APPLY_UF);
     break;
 
-  case Smt::QF_UFLIA:
   case Smt::QF_UFLRA:
   case Smt::QF_UFNRA:
     addTheory(THEORY_REALS);