From 9aa6386be94e96651b5c12065cb95a9e4dea74b8 Mon Sep 17 00:00:00 2001
From: Nuno Lopes <nlopes@microsoft.com>
Date: Fri, 6 Oct 2017 15:27:16 +0100
Subject: [PATCH] fix debug build

---
 src/util/lp/indexed_vector_instances.cpp | 1 +
 1 file changed, 1 insertion(+)

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;