From d07f2d45e740b10ba96ee4e98bd04f3562febe14 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Thu, 18 Jul 2019 08:33:58 -0700
Subject: [PATCH] fix #2409

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

diff --git a/src/model/model.cpp b/src/model/model.cpp
index 88137dd2e..bd327d8b5 100644
--- a/src/model/model.cpp
+++ b/src/model/model.cpp
@@ -335,6 +335,9 @@ void model::collect_occs(top_sort& ts, func_decl* f) {
                collect_occs(ts, e);
             for (auto const& fe : *fi) {
                 collect_occs(ts, fe->get_result());
+                for (unsigned i = 0; i < fi->get_arity(); ++i) {
+                    collect_occs(ts, fe->get_arg(i));
+                }
             }
         }
     }