Improve rewrite for string substr (#1337)

2 files changed, 22 insertions, 0 deletions

diff --git a/test/regress/regress0/strings/Makefile.am b/test/regress/regress0/strings/Makefile.am
index c4fb8dd94..99fd2b630 100644
--- a/test/regress/regress0/strings/Makefile.am
+++ b/test/regress/regress0/strings/Makefile.am
@@ -92,6 +92,7 @@ TESTS = \
   issue1105.smt2 \
   issue1189.smt2 \
   rewrites-v2.smt2 \
+  substr-rewrites.smt2 \
   norn-ab.smt2 \
   type002.smt2
 
diff --git a/test/regress/regress0/strings/substr-rewrites.smt2 b/test/regress/regress0/strings/substr-rewrites.smt2
new file mode 100644
index 000000000..c4f19b7b4
--- /dev/null
+++ b/test/regress/regress0/strings/substr-rewrites.smt2
@@ -0,0 +1,21 @@
+; COMMAND-LINE: --strings-exp
+; EXPECT: unsat
+(set-logic SLIA)
+(set-info :status unsat)
+
+(declare-fun x () String)
+(declare-fun y () String)
+(declare-fun z () String)
+
+; these should all rewrite to false
+(assert (or 
+
+(not (= (str.substr (str.++ x "abc" y) 0 (+ (str.len x) 1)) (str.++ x "a")))
+(not (= (str.substr (str.++ x "abc" y) (+ (str.len x) 1) (+ (* 2 (str.len y)) 7)) (str.++ "bc" y)))
+(not (= (str.substr (str.++ x y) 0 (+ (str.len z) (* 2 (str.len x)) (* 2 (str.len y)))) (str.substr (str.++ x y) 0 (+ (str.len x) (str.len y)))))
+(not (= (str.substr x (+ (str.len x) 1) 5) (str.substr y (- (- 1) (str.len z)) 5)))
+(not (= (str.substr "abc" 100000000000000000000000000000000000000000000000000000000000000000000000000 5) ""))
+
+))
+
+(check-sat)