From 2ef582ec2671a9d6e88aec576786b796e504e3cb Mon Sep 17 00:00:00 2001
From: Tim King <taking@cs.nyu.edu>
Date: Wed, 19 Oct 2011 18:50:41 +0000
Subject: [PATCH] Adding support for QF_UFLIA to the smt2 parser.

---
 src/parser/smt/smt.cpp   | 1 +
 src/parser/smt2/smt2.cpp | 2 +-
 2 files changed, 2 insertions(+), 1 deletion(-)

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