diff --git a/src/util/lp/indexed_vector_instances.cpp b/src/util/lp/indexed_vector_instances.cpp
index ee078f021..79c3ee1a1 100644
--- a/src/util/lp/indexed_vector_instances.cpp
+++ b/src/util/lp/indexed_vector_instances.cpp
@@ -33,6 +33,7 @@ template void indexed_vector<unsigned>::resize(unsigned int);
 template void indexed_vector<mpq>::set_value(const mpq&, unsigned int);
 template void indexed_vector<unsigned>::set_value(const unsigned&, unsigned int);
 #ifdef Z3DEBUG
+template bool indexed_vector<unsigned>::is_OK() const;
 template bool indexed_vector<double>::is_OK() const;
 template bool indexed_vector<mpq>::is_OK() const;
 template bool indexed_vector<lp::numeric_pair<mpq> >::is_OK() const;