summaryrefslogtreecommitdiff
path: root/src/theory/quantifiers/bounded_integers.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/quantifiers/bounded_integers.cpp')
-rw-r--r--src/theory/quantifiers/bounded_integers.cpp2
1 files changed, 1 insertions, 1 deletions
diff --git a/src/theory/quantifiers/bounded_integers.cpp b/src/theory/quantifiers/bounded_integers.cpp
index bec8ea350..a294eec5a 100644
--- a/src/theory/quantifiers/bounded_integers.cpp
+++ b/src/theory/quantifiers/bounded_integers.cpp
@@ -277,7 +277,7 @@ void BoundedIntegers::registerQuantifier( Node f ) {
Node r = d_range[f][v];
if( r.hasBoundVar() ){
//introduce a new bound
- Node new_range = NodeManager::currentNM()->mkSkolem( "bir_$$", r.getType(), "bound for term" );
+ Node new_range = NodeManager::currentNM()->mkSkolem( "bir", r.getType(), "bound for term" );
d_nground_range[f][v] = d_range[f][v];
d_range[f][v] = new_range;
r = new_range;
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback