From: Morgan Deters <mdeters@gmail.com>
Date: Wed, 18 Jul 2012 17:37:41 +0000 (+0000)
Subject: removing an obsolete assertion in model-generation framework, per Andy's request
X-Git-Tag: cvc5-1.0.0~7915
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=4228332c346147daa83c0c4123c8781909a23a03;p=cvc5.git

removing an obsolete assertion in model-generation framework, per Andy's request
---

diff --git a/src/theory/model.cpp b/src/theory/model.cpp
index 052051e83..19169efa3 100644
--- a/src/theory/model.cpp
+++ b/src/theory/model.cpp
@@ -331,7 +331,6 @@ DefaultModel::DefaultModel( context::Context* c, std::string name ) : TheoryMode
 }
 
 Node DefaultModel::getInterpretedValue( TNode n ){
-  Assert( !d_equalityEngine.hasTerm( n ) );
   TypeNode type = n.getType();
   if( type.isFunction() || type.isPredicate() ){
     //DO_THIS?