From eb9c5b7cdb1f4798b2e77af2b5bf75b640f60a3d Mon Sep 17 00:00:00 2001
From: "Christoph M. Wintersteiger" <cwinter@microsoft.com>
Date: Fri, 1 Apr 2016 13:25:37 +0100
Subject: [PATCH] Disabled bogus assertions.

Fixes #489
---
 src/model/model.cpp                 | 1 -
 src/smt/proto_model/proto_model.cpp | 1 -
 2 files changed, 2 deletions(-)

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);
 }