From a738f5af12ff14312254c7024dc253358e4b6f83 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Fri, 2 Mar 2018 20:14:59 +0900
Subject: [PATCH] fix #1512

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/model/func_interp.cpp | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/src/model/func_interp.cpp b/src/model/func_interp.cpp
index accb45a25..2eb687dae 100644
--- a/src/model/func_interp.cpp
+++ b/src/model/func_interp.cpp
@@ -112,7 +112,8 @@ bool func_interp::is_fi_entry_expr(expr * e, ptr_vector<expr> & args) {
         return false;
     }
 
-    if ((m_arity == 0) ||
+    if (!is_ground(t) ||
+        (m_arity == 0) ||
         (m_arity == 1 && !m().is_eq(c, a0, a1)) ||
         (m_arity > 1 && (!m().is_and(c) || to_app(c)->get_num_args() != m_arity)))
         return false;