From 559c5a26a32ff9e978bf11eaba5354e730411947 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sat, 7 Nov 2015 11:16:15 -0800
Subject: [PATCH] fix(library/congr_lemma_manager): take resulting type into
 account when computing congruence lemma

---
 src/library/congr_lemma_manager.cpp | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

diff --git a/src/library/congr_lemma_manager.cpp b/src/library/congr_lemma_manager.cpp
index 1b0b096e3..8913f71e1 100644
--- a/src/library/congr_lemma_manager.cpp
+++ b/src/library/congr_lemma_manager.cpp
@@ -148,12 +148,15 @@ public:
         if (r != m_cache.end())
             return optional<result>(r->second);
         fun_info finfo = m_fmanager.get(fn);
+        list<unsigned> const & result_deps = finfo.get_dependencies();
         buffer<congr_arg_kind> kinds;
         buffer<param_info>     pinfos;
         to_buffer(finfo.get_params_info(), pinfos);
         kinds.resize(pinfos.size(), congr_arg_kind::Eq);
         for (unsigned i = 0; i < pinfos.size(); i++) {
-            if (pinfos[i].is_subsingleton()) {
+            if (std::find(result_deps.begin(), result_deps.end(), i) != result_deps.end()) {
+                kinds[i] = congr_arg_kind::Fixed;
+            } else if (pinfos[i].is_subsingleton()) {
                 if (empty(pinfos[i].get_dependencies()))
                     kinds[i] = congr_arg_kind::Fixed;
                 else