summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--src/theory/datatypes/datatypes_rewriter.h2
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 );
}
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback