add back eager approach

diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index 7c3e7ebbc4f51a9c15f166e2d62cb358ba9da1f4..a50c295da6ebba4345e33415b0cb857817d08abb 100644 (file)
--- 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;