From 04d709dae147542fee24656c8548259f9cd5dd92 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Mon, 19 Nov 2018 09:42:10 -0800
Subject: [PATCH] build errors on shrink

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

diff --git a/src/util/ref_vector.h b/src/util/ref_vector.h
index f45b44daed..d0a17116a2 100644
--- a/src/util/ref_vector.h
+++ b/src/util/ref_vector.h
@@ -321,6 +321,8 @@ class ref_vector : public ref_vector_core<T, ref_manager_wrapper<T, TManager> >
         return result;
     }
 
+#if 0
+    // TBD: not sure why some compilers complain here.
     ref_vector& filter_update(std::function<bool(T)>& predicate) {
         unsigned j = 0;
         for (auto& t : *this)
@@ -329,6 +331,7 @@ class ref_vector : public ref_vector_core<T, ref_manager_wrapper<T, TManager> >
         shrink(j);
         return *this;
     }
+#endif
 
     template <typename S>
     vector<S> mapv_pure(std::function<S(T)>& f) const {