summaryrefslogtreecommitdiff
path: root/src/theory/strings/theory_strings.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/strings/theory_strings.cpp')
-rw-r--r--src/theory/strings/theory_strings.cpp1
1 files changed, 1 insertions, 0 deletions
diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index bb5e3718a..99d64270b 100644
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -51,6 +51,7 @@ TheoryStrings::TheoryStrings(context::Context* c, context::UserContext* u, Outpu
//d_equalityEngine.addFunctionKind(kind::STRING_IN_REGEXP);
d_equalityEngine.addFunctionKind(kind::STRING_LENGTH);
d_equalityEngine.addFunctionKind(kind::STRING_CONCAT);
+ d_equalityEngine.addFunctionKind(kind::STRING_STRCTN);
d_zero = NodeManager::currentNM()->mkConst( Rational( 0 ) );
d_emptyString = NodeManager::currentNM()->mkConst( ::CVC4::String("") );
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback