diff options
-rw-r--r-- | src/theory/datatypes/datatypes_rewriter.h | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/theory/datatypes/datatypes_rewriter.h b/src/theory/datatypes/datatypes_rewriter.h index dc85d0cd6..389bcca8b 100644 --- a/src/theory/datatypes/datatypes_rewriter.h +++ b/src/theory/datatypes/datatypes_rewriter.h @@ -266,7 +266,7 @@ public: if( dt.isParametric() ){ tn = TypeNode::fromType( tspec )[i]; } - nc = NodeManager::currentNM()->mkSkolem( "m_$$", tn, "created for inst cons" ); + nc = NodeManager::currentNM()->mkSkolem( "m", tn, "created for inst cons" ); } children.push_back( nc ); } |