From: Tim King <taking@cs.nyu.edu>
Date: Wed, 19 Oct 2011 18:50:41 +0000 (+0000)
Subject: Adding support for QF_UFLIA to the smt2 parser.
X-Git-Tag: cvc5-1.0.0~8415
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=2ef582ec2671a9d6e88aec576786b796e504e3cb;p=cvc5.git

Adding support for QF_UFLIA to the smt2 parser.
---

diff --git a/src/parser/smt/smt.cpp b/src/parser/smt/smt.cpp
index a6e716b77..e0d1922c8 100644
--- 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 4bc90ec8f..08a824c0a 100644
--- 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);