diff options
Diffstat (limited to 'src/theory/model.cpp')
-rw-r--r-- | src/theory/model.cpp | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/src/theory/model.cpp b/src/theory/model.cpp index 42654b74c..8aec39309 100644 --- a/src/theory/model.cpp +++ b/src/theory/model.cpp @@ -53,14 +53,14 @@ Node TheoryModel::getValue( TNode n ){ return getModelValue( nn ); } -Expr TheoryModel::getValue( const Expr& expr ){ +Expr TheoryModel::getValue( Expr expr ){ Node n = Node::fromExpr( expr ); Node ret = getValue( n ); return ret.toExpr(); } /** get cardinality for sort */ -Cardinality TheoryModel::getCardinality( const Type& t ){ +Cardinality TheoryModel::getCardinality( Type t ){ TypeNode tn = TypeNode::fromType( t ); //for now, we only handle cardinalities for uninterpreted sorts if( tn.isSort() ){ @@ -373,7 +373,7 @@ Node DefaultModel::getInterpretedValue( TNode n ){ } if( default_v.isNull() ){ //choose default value from model if none exists - default_v = getInterpretedValue( NodeManager::currentNM()->mkSkolem( type.getRangeType() ) ); + default_v = getInterpretedValue( NodeManager::currentNM()->mkSkolem( "defaultValue_$$", type.getRangeType(), "a default value term from model construction" ) ); } ufmt.setDefaultValue( this, default_v ); ufmt.simplify(); |