summaryrefslogtreecommitdiff
path: root/src/theory
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory')
-rw-r--r--src/theory/strings/theory_strings.cpp2
1 files changed, 1 insertions, 1 deletions
diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index 7c3e7ebbc..a50c295da 100644
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -1451,7 +1451,7 @@ bool TheoryStrings::checkLengths() {
//if n is concat, and
//if n has not instantiatied the concat..length axiom
//then, add lemma
- if( n.getKind() == kind::CONST_STRING ) { // || n.getKind() == kind::STRING_CONCAT ){
+ if( n.getKind() == kind::CONST_STRING || n.getKind() == kind::STRING_CONCAT ) { // || n.getKind() == kind::STRING_CONCAT ){
if( d_length_inst.find(n)==d_length_inst.end() ){
d_length_inst[n] = true;
Trace("strings-debug") << "get n: " << n << endl;
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback