diff --git a/src/model/model.cpp b/src/model/model.cpp
index 0e6e17c8e..951c7f744 100644
--- a/src/model/model.cpp
+++ b/src/model/model.cpp
@@ -130,7 +130,6 @@ sort * model::get_uninterpreted_sort(unsigned idx) const {
 }
 
 void model::register_usort(sort * s, unsigned usize, expr * const * universe) {
-    SASSERT(m_manager.is_uninterp(s));
     sort2universe::obj_map_entry * entry = m_usort2universe.insert_if_not_there2(s, 0);
     m_manager.inc_array_ref(usize, universe);
     if (entry->get_data().m_value == 0) {
diff --git a/src/smt/proto_model/proto_model.cpp b/src/smt/proto_model/proto_model.cpp
index 8fc262bac..a7875e99e 100644
--- a/src/smt/proto_model/proto_model.cpp
+++ b/src/smt/proto_model/proto_model.cpp
@@ -262,7 +262,6 @@ void proto_model::freeze_universe(sort * s) {
    \brief Return the known universe of an uninterpreted sort.
 */
 obj_hashtable<expr> const & proto_model::get_known_universe(sort * s) const {
-    SASSERT(m_manager.is_uninterp(s));
     return m_user_sort_factory->get_known_universe(s);
 }