From fca44ff3f230301e36c9ffcfc2a3b256164a9ea9 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Tue, 19 May 2020 13:40:03 -0700
Subject: [PATCH] fix #4394

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/ast/recfun_decl_plugin.cpp | 8 +++-----
 1 file changed, 3 insertions(+), 5 deletions(-)

diff --git a/src/ast/recfun_decl_plugin.cpp b/src/ast/recfun_decl_plugin.cpp
index a26e486ce..99e0da198 100644
--- a/src/ast/recfun_decl_plugin.cpp
+++ b/src/ast/recfun_decl_plugin.cpp
@@ -355,11 +355,7 @@ namespace recfun {
                 util & u;
                 find(util & u) : u(u) {}
                 bool operator()(expr * e) override {
-                    //return is_app(e) ? u.owns_app(to_app(e)) : false;
-                    if (! is_app(e)) return false;
-
-                    app * a = to_app(e);
-                    return u.is_defined(a);
+                    return is_app(e) && u.is_defined(to_app(e));
                 }
             };
             find f(u);
@@ -467,6 +463,8 @@ namespace recfun {
             scores.insert(e, 0);
             // walk deepest terms first.
             for (unsigned i = max_depth; i > 0; --i) {
+                if (!by_depth.contains(i))
+                    continue;
                 for (expr* t : by_depth[i]) {
                     unsigned score = 0;
                     for (expr* parent : parents[t]) {