From 81d322b79f0c5ce23e484834af10bb4ea1287ece Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sun, 10 Feb 2019 11:12:26 -0800
Subject: [PATCH] fix bug in model compression that skips dependencies in
 function entries. Exposed in t171.smt2

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

diff --git a/src/model/model.cpp b/src/model/model.cpp
index de6bb4db8..e6a3ffedf 100644
--- a/src/model/model.cpp
+++ b/src/model/model.cpp
@@ -277,6 +277,13 @@ model::func_decl_set* model::collect_deps(top_sort& ts, func_interp * fi) {
     fi->compress();
     expr* e = fi->get_else();
     if (e) for_each_expr(collector, e);
+    unsigned num_args = fi->get_arity();
+    for (func_entry* fe : *fi) {
+        for (unsigned i = 0; i < num_args; ++i) {
+            for_each_expr(collector, fe->get_arg(i));
+        }
+        for_each_expr(collector, fe->get_result());
+    }
     return s;
 }