From: Tianyi Liang <tianyi-liang@uiowa.edu>
Date: Wed, 22 Jan 2014 19:50:39 +0000 (-0600)
Subject: solve string exp issue for regexp
X-Git-Tag: cvc5-1.0.0~7134
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=7e445cf997a695ca2726df50e3b2f6d5f4809c95;p=cvc5.git

solve string exp issue for regexp
---

diff --git a/src/theory/strings/theory_strings_preprocess.cpp b/src/theory/strings/theory_strings_preprocess.cpp
index 757ec56a2..288940838 100644
--- a/src/theory/strings/theory_strings_preprocess.cpp
+++ b/src/theory/strings/theory_strings_preprocess.cpp
@@ -119,6 +119,9 @@ int StringsPreprocess::checkFixLenVar( Node t ) {
 			ret = 2;
 		}
 	}
+	if(!options::stringExp()) {
+		ret = 2;
+	}
 	return ret;
 }
 Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) {