1 files changed, 10 insertions, 10 deletions
diff --git a/test/regress/regress0/strings/crash-1019.smt2 b/test/regress/regress0/strings/crash-1019.smt2
index 1a41ba715..9f2e99b02 100755
--- a/test/regress/regress0/strings/crash-1019.smt2
+++ b/test/regress/regress0/strings/crash-1019.smt2
@@ -1,10 +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)
+(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)