From 5ae2dd9c747946535f1f05771161b19d0e03ccf6 Mon Sep 17 00:00:00 2001
From: "Christoph M. Wintersteiger" <cwinter@microsoft.com>
Date: Sat, 30 May 2015 15:20:07 +0100
Subject: [PATCH] Bugfix for QF_FP default tactic.

---
 src/tactic/fpa/qffp_tactic.cpp | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/tactic/fpa/qffp_tactic.cpp b/src/tactic/fpa/qffp_tactic.cpp
index 3bee224b3..fbce1668e 100644
--- a/src/tactic/fpa/qffp_tactic.cpp
+++ b/src/tactic/fpa/qffp_tactic.cpp
@@ -45,7 +45,7 @@ struct has_fp_to_real_predicate {
     void operator()(app * n) {
         sort * s = get_sort(n);
         if (au.is_real(s) && n->get_family_id() == fu.get_family_id() &&
-            is_app(n) && to_app(n)->get_kind() == OP_FPA_TO_REAL)
+            is_app(n) && to_app(n)->get_decl_kind() == OP_FPA_TO_REAL)
             throw found();
     }
 };