Clean up explanations involving string length. Add regression.

2 files changed, 12 insertions, 1 deletions

diff --git a/test/regress/regress0/strings/Makefile.am b/test/regress/regress0/strings/Makefile.am
index 4d1da2efb..f5c6048e6 100644
--- a/test/regress/regress0/strings/Makefile.am
+++ b/test/regress/regress0/strings/Makefile.am
@@ -73,7 +73,8 @@ TESTS = \
   bug686dd.smt2 \
   idof-handg.smt2 \
   fmf001.smt2 \
-  type002.smt2
+  type002.smt2 \
+  crash-1019.smt2
 
 FAILING_TESTS =
 
diff --git a/test/regress/regress0/strings/crash-1019.smt2 b/test/regress/regress0/strings/crash-1019.smt2
new file mode 100755
index 000000000..1a41ba715
--- /dev/null
+++ b/test/regress/regress0/strings/crash-1019.smt2
@@ -0,0 +1,10 @@
+(set-logic ALL_SUPPORTED)

+(set-option :strings-exp true)

+(set-option :rewrite-divk true)

+(set-info :status unsat)

+ 

+(declare-fun s () String)

+ 

+(assert (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (not (not (not (= (ite (= (str.++ (str.replace (str.substr s 0 (- (+ (str.indexof s "o" 0) 1) 0)) "o" "a") (str.++ (str.replace (str.substr (str.substr s (+ (str.indexof s "o" 0) 1) (- (str.len s) (+ (str.indexof s "o" 0) 1))) 0 (- (+ (str.indexof (str.substr s (+ (str.indexof s "o" 0) 1) (- (str.len s) (+ (str.indexof s "o" 0) 1))) "o" 0) 1) 0)) "o" "a") (str.substr (str.substr s (+ (str.indexof s "o" 0) 1) (- (str.len s) (+ (str.indexof s "o" 0) 1))) (+ (str.indexof (str.substr s (+ (str.indexof s "o" 0) 1) (- (str.len s) (+ (str.indexof s "o" 0) 1))) "o" 0) 1) (- (str.len (str.substr s (+ (str.indexof s "o" 0) 1) (- (str.len s) (+ (str.indexof s "o" 0) 1)))) (+ (str.indexof (str.substr s (+ (str.indexof s "o" 0) 1) (- (str.len s) (+ (str.indexof s "o" 0) 1))) "o" 0) 1))))) "faa") 1 0) 0)))) (not (not (= (ite (str.contains (str.substr (str.substr s (+ (str.indexof s "o" 0) 1) (- (str.len s) (+ (str.indexof s "o" 0) 1))) (+ (str.indexof (str.substr s (+ (str.indexof s "o" 0) 1) (- (str.len s) (+ (str.indexof s "o" 0) 1))) "o" 0) 1) (- (str.len (str.substr s (+ (str.indexof s "o" 0) 1) (- (str.len s) (+ (str.indexof s "o" 0) 1)))) (+ (str.indexof (str.substr s (+ (str.indexof s "o" 0) 1) (- (str.len s) (+ (str.indexof s "o" 0) 1))) "o" 0) 1))) "o") 1 0) 0)))) (not (= (ite (str.contains (str.substr s (+ (str.indexof s "o" 0) 1) (- (str.len s) (+ (str.indexof s "o" 0) 1))) "o") 1 0) 0))) (not (= (ite (str.contains s "o") 1 0) 0))) (>= 0 0)) (> (- (+ (str.indexof s "o" 0) 1) 0) 0)) (> (str.len s) 0)) (>= (+ (str.indexof s "o" 0) 1) 0)) (> (- (str.len s) (+ (str.indexof s "o" 0) 1)) 0)) (> (str.len s) (+ (str.indexof s "o" 0) 1))) (>= (+ (str.indexof s "o" 0) 1) 0)) (> (- (str.len s) (+ (str.indexof s "o" 0) 1)) 0)) (> (str.len s) (+ (str.indexof s "o" 0) 1))) (>= 0 0)) (> (- (+ (str.indexof (str.substr s (+ (str.indexof s "o" 0) 1) (- (str.len s) (+ (str.indexof s "o" 0) 1))) "o" 0) 1) 0) 0)) (> (str.len (str.substr s (+ (str.indexof s "o" 0) 1) (- (str.len s) (+ (str.indexof s "o" 0) 1)))) 0)) (>= (+ (str.indexof s "o" 0) 1) 0)) (> (- (str.len s) (+ (str.indexof s "o" 0) 1)) 0)) (> (str.len s) (+ (str.indexof s "o" 0) 1))) (>= (+ (str.indexof s "o" 0) 1) 0)) (> (- (str.len s) (+ (str.indexof s "o" 0) 1)) 0)) (> (str.len s) (+ (str.indexof s "o" 0) 1))) (>= (+ (str.indexof s "o" 0) 1) 0)) (> (- (str.len s) (+ (str.indexof s "o" 0) 1)) 0)) (> (str.len s) (+ (str.indexof s "o" 0) 1))) (>= (+ (str.indexof (str.substr s (+ (str.indexof s "o" 0) 1) (- (str.len s) (+ (str.indexof s "o" 0) 1))) "o" 0) 1) 0)) (> (- (str.len (str.substr s (+ (str.indexof s "o" 0) 1) (- (str.len s) (+ (str.indexof s "o" 0) 1)))) (+ (str.indexof (str.substr s (+ (str.indexof s "o" 0) 1) (- (str.len s) (+ (str.indexof s "o" 0) 1))) "o" 0) 1)) 0)) (> (str.len (str.substr s (+ (str.indexof s "o" 0) 1) (- (str.len s) (+ (str.indexof s "o" 0) 1)))) (+ (str.indexof (str.substr s (+ (str.indexof s "o" 0) 1) (- (str.len s) (+ (str.indexof s "o" 0) 1))) "o" 0) 1))) (>= (+ (str.indexof s "o" 0) 1) 0)) (> (- (str.len s) (+ (str.indexof s "o" 0) 1)) 0)) (> (str.len s) (+ (str.indexof s "o" 0) 1))) (>= (+ (str.indexof s "o" 0) 1) 0)) (> (- (str.len s) (+ (str.indexof s "o" 0) 1)) 0)) (> (str.len s) (+ (str.indexof s "o" 0) 1))) (>= (+ (str.indexof s "o" 0) 1) 0)) (> (- (str.len s) (+ (str.indexof s "o" 0) 1)) 0)) (> (str.len s) (+ (str.indexof s "o" 0) 1))) (>= (+ (str.indexof (str.substr s (+ (str.indexof s "o" 0) 1) (- (str.len s) (+ (str.indexof s "o" 0) 1))) "o" 0) 1) 0)) (> (- (str.len (str.substr s (+ (str.indexof s "o" 0) 1) (- (str.len s) (+ (str.indexof s "o" 0) 1)))) (+ (str.indexof (str.substr s (+ (str.indexof s "o" 0) 1) (- (str.len s) (+ (str.indexof s "o" 0) 1))) "o" 0) 1)) 0)) (> (str.len (str.substr s (+ (str.indexof s "o" 0) 1) (- (str.len s) (+ (str.indexof s "o" 0) 1)))) (+ (str.indexof (str.substr s (+ (str.indexof s "o" 0) 1) (- (str.len s) (+ (str.indexof s "o" 0) 1))) "o" 0) 1))) (>= (+ (str.indexof s "o" 0) 1) 0)) (> (- (str.len s) (+ (str.indexof s "o" 0) 1)) 0)) (> (str.len s) (+ (str.indexof s "o" 0) 1))))

+ 

+(check-sat)