mirror of
https://github.com/Z3Prover/z3
synced 2025-04-06 01:24:08 +00:00
parent
852dc6d190
commit
eb9c5b7cdb
|
@ -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) {
|
||||
|
|
|
@ -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);
|
||||
}
|
||||
|
||||
|
|
Loading…
Reference in a new issue