From: Kshitij Bansal <kshitij@cs.nyu.edu>
Date: Mon, 28 Apr 2014 15:31:29 +0000 (-0400)
Subject: minor fix
X-Git-Tag: cvc5-1.0.0~6956^2
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=ca423e291b1f7d67e1a325bb6d98663d6c0690c7;p=cvc5.git

minor fix
---

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