Refactoring of strings preprocess module. When enabled, apply eager preprocess during ppRewrite instead of during processAssertions. Simplify reduction for contains. Fix bug in explanations for F_EndpointEq. Minor cleanup for sep.

2 files changed, 24 insertions, 1 deletions

diff --git a/test/regress/regress0/strings/Makefile.am b/test/regress/regress0/strings/Makefile.am
index 477d336e6..d23fd866d 100644
--- a/test/regress/regress0/strings/Makefile.am
+++ b/test/regress/regress0/strings/Makefile.am
@@ -78,7 +78,8 @@ TESTS = \
   norn-31.smt2 \
   strings-native-simple.cvc \
   cmu-2db2-extf-reg.smt2 \
-  norn-nel-bug-052116.smt2
+  norn-nel-bug-052116.smt2 \
+  cmu-disagree-0707-dd.smt2
 
 FAILING_TESTS =
 
diff --git a/test/regress/regress0/strings/cmu-disagree-0707-dd.smt2 b/test/regress/regress0/strings/cmu-disagree-0707-dd.smt2
new file mode 100644
index 000000000..c44dfa396
--- /dev/null
+++ b/test/regress/regress0/strings/cmu-disagree-0707-dd.smt2
@@ -0,0 +1,22 @@
+(set-logic ALL_SUPPORTED)
+(set-info :status sat)
+(set-option :strings-exp true)
+
+(declare-fun url () String)
+
+(assert 
+(and 
+(and 
+(and 
+(and 
+
+(= (str.len (str.substr (str.substr url (str.indexof url "#" 2) (- (str.len url) (str.indexof url "#" 2))) (+ (str.indexof (str.substr url (str.indexof url "#" 2) (- (str.len url) (str.indexof url "#" 2))) "#" 0) 1) (- (str.len (str.substr url (str.indexof url "#" 2) (- (str.len url) (str.indexof url "#" 2)))) (+ (str.indexof (str.substr url (str.indexof url "#" 2) (- (str.len url) (str.indexof url "#" 2))) "#" 0) 1)))) 0) 
+
+(not (= (str.substr url 0 (- (str.indexof url ":" 0) 0)) "http")))
+(> (str.indexof url ":" 0) 0))
+(>= (- (str.indexof url "#" 2) 2) 0)) 
+(>= (str.indexof url ":" 0) 0))
+)
+
+(check-sat)
+