diff --git a/src/math/simplex/simplex_def.h b/src/math/simplex/simplex_def.h
index 0e00e368b..c3a2bef95 100644
--- a/src/math/simplex/simplex_def.h
+++ b/src/math/simplex/simplex_def.h
@@ -25,6 +25,9 @@ Notes:
 
 namespace simplex {
 
+    template<typename Ext>
+    const typename simplex<Ext>::var_t simplex<Ext>::null_var = UINT_MAX; 
+
     template<typename Ext>
     typename simplex<Ext>::row 
     simplex<Ext>::add_row(var_t base_var, unsigned num_vars, var_t const* vars, numeral const* coeffs) {
diff --git a/src/smt/theory_diff_logic.cpp b/src/smt/theory_diff_logic.cpp
index a68b7782b..cb1812f9f 100644
--- a/src/smt/theory_diff_logic.cpp
+++ b/src/smt/theory_diff_logic.cpp
@@ -28,5 +28,7 @@ template class theory_diff_logic<idl_ext>;
 template class theory_diff_logic<sidl_ext>;
 template class theory_diff_logic<rdl_ext>;
 template class theory_diff_logic<srdl_ext>;
+template class simplex::simplex<simplex::mpq_ext>;
+
 
 };
diff --git a/src/smt/theory_pb.cpp b/src/smt/theory_pb.cpp
index 7976e27b3..ef7d6aff8 100644
--- a/src/smt/theory_pb.cpp
+++ b/src/smt/theory_pb.cpp
@@ -61,6 +61,9 @@ namespace smt {
         };
     };
 
+    const unsigned theory_pb::null_index = UINT_MAX;
+
+
     unsigned theory_pb::arg_t::get_hash() const {
         return get_composite_hash<arg_t, arg_t::kind_hash, arg_t::child_hash>(*this, size());
     }
diff --git a/src/smt/theory_pb.h b/src/smt/theory_pb.h
index 46c68900a..595cf5e6e 100644
--- a/src/smt/theory_pb.h
+++ b/src/smt/theory_pb.h
@@ -272,7 +272,7 @@ namespace smt {
 
         // bool_var |-> index into m_lemma
         unsigned_vector   m_conseq_index;
-        static const unsigned null_index = UINT_MAX;
+        static const unsigned null_index;
         bool is_marked(bool_var v) const;
         void set_mark(bool_var v, unsigned idx);
         void unset_mark(bool_var v);