From f62609d9eca8086d5c68b77cfd0a5d717d24aeab Mon Sep 17 00:00:00 2001 From: ajreynol Date: Thu, 7 Jul 2016 15:22:40 -0500 Subject: 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. --- test/regress/regress0/strings/Makefile.am | 3 ++- .../regress0/strings/cmu-disagree-0707-dd.smt2 | 22 ++++++++++++++++++++++ 2 files changed, 24 insertions(+), 1 deletion(-) create mode 100644 test/regress/regress0/strings/cmu-disagree-0707-dd.smt2 (limited to 'test/regress') 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) + -- cgit v1.2.3