From: Tianyi Liang <tianyi-liang@uiowa.edu>
Date: Wed, 23 Oct 2013 18:52:24 +0000 (-0500)
Subject: add back eager approach
X-Git-Tag: cvc5-1.0.0~7275^2~1
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=496c5489a5073ef1aa9306e165ac4dc4aaeb69a9;p=cvc5.git

add back eager approach
---

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;