From 4a9f12dd3431e9df0ae9b8578df73ccfca943c69 Mon Sep 17 00:00:00 2001
From: "Christoph M. Wintersteiger" <cwinter@microsoft.com>
Date: Mon, 24 Feb 2014 13:57:15 +0000
Subject: [PATCH] bugfix for FPA

---
 src/tactic/fpa/qffpa_tactic.cpp | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/src/tactic/fpa/qffpa_tactic.cpp b/src/tactic/fpa/qffpa_tactic.cpp
index 90cfc8c92..73faa5b50 100644
--- a/src/tactic/fpa/qffpa_tactic.cpp
+++ b/src/tactic/fpa/qffpa_tactic.cpp
@@ -52,6 +52,8 @@ struct is_non_qffpa_predicate {
         sort * s = get_sort(n);
         if (!m.is_bool(s) && !(u.is_float(s) || u.is_rm(s)))
             throw found();
+        if (is_uninterp(n))
+            throw found();
         family_id fid = s->get_family_id();
         if (fid == m.get_basic_family_id())
             return;
@@ -78,6 +80,8 @@ struct is_non_qffpabv_predicate {
         sort * s = get_sort(n);
         if (!m.is_bool(s) && !(fu.is_float(s) || fu.is_rm(s) || bu.is_bv_sort(s)))
             throw found();
+        if (is_uninterp(n))
+            throw found();
         family_id fid = s->get_family_id();
         if (fid == m.get_basic_family_id())
             return;