From db411eef25fae56f70d0ffd2ab8781824d3416b1 Mon Sep 17 00:00:00 2001
From: "Christoph M. Wintersteiger" <cwinter@microsoft.com>
Date: Tue, 19 May 2015 13:35:19 +0100
Subject: [PATCH] Improved supported logics checks for FPA logics.

---
 src/cmd_context/cmd_context.cpp | 18 ++++++++----------
 src/cmd_context/cmd_context.h   |  1 +
 2 files changed, 9 insertions(+), 10 deletions(-)

diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp
index 788a8affd..651a84110 100644
--- a/src/cmd_context/cmd_context.cpp
+++ b/src/cmd_context/cmd_context.cpp
@@ -550,9 +550,7 @@ bool cmd_context::logic_has_bv_core(symbol const & s) const {
 }
 
 bool cmd_context::logic_has_horn(symbol const& s) const {
-    return
-        s == "HORN";
-
+    return s == "HORN";
 }
 
 bool cmd_context::logic_has_bv() const {
@@ -560,19 +558,20 @@ bool cmd_context::logic_has_bv() const {
 }
 
 bool cmd_context::logic_has_seq_core(symbol const& s) const {
-    return 
-        s == "QF_BVRE";
-        
+    return s == "QF_BVRE";
 }
 
 bool cmd_context::logic_has_seq() const {
     return !has_logic() || logic_has_seq_core(m_logic);        
 }
 
-bool cmd_context::logic_has_fpa() const {
-    return !has_logic() || m_logic == "QF_FP" || m_logic == "QF_FPBV";
+bool cmd_context::logic_has_fpa_core(symbol const& s) const {
+    return s == "QF_FP" || s == "QF_FPBV" || s == "QF_BVFP";
 }
 
+bool cmd_context::logic_has_fpa() const {
+    return !has_logic() || logic_has_fpa_core(m_logic);
+}
 
 bool cmd_context::logic_has_array_core(symbol const & s) const {
     return 
@@ -682,8 +681,7 @@ bool cmd_context::supported_logic(symbol const & s) const {
     return s == "QF_UF" || s == "UF" || 
         logic_has_arith_core(s) || logic_has_bv_core(s) || 
         logic_has_array_core(s) || logic_has_seq_core(s) ||
-        logic_has_horn(s) ||
-        s == "QF_FP" || s == "QF_FPBV";
+        logic_has_horn(s) || logic_has_fpa_core(s);
 }
 
 bool cmd_context::set_logic(symbol const & s) {
diff --git a/src/cmd_context/cmd_context.h b/src/cmd_context/cmd_context.h
index 7758424e0..148bb61d9 100644
--- a/src/cmd_context/cmd_context.h
+++ b/src/cmd_context/cmd_context.h
@@ -250,6 +250,7 @@ protected:
     bool logic_has_bv_core(symbol const & s) const;
     bool logic_has_array_core(symbol const & s) const;
     bool logic_has_seq_core(symbol const & s) const;
+    bool logic_has_fpa_core(symbol const & s) const;
     bool logic_has_horn(symbol const& s) const;
     bool logic_has_arith() const;
     bool logic_has_bv() const;