diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2015-10-20 00:34:50 +0200 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2015-10-20 00:34:50 +0200 |
commit | edae14eebd48cec77ce2bc7f5cdafd4840299a2f (patch) | |
tree | cf541e84cfbc64d1f057557559116b4cb9429dc2 /test/regress | |
parent | 497b027d87c0cdd9cf3da25acf3d9b0969020a57 (diff) |
Clean up explanations involving string length. Add regression.
Diffstat (limited to 'test/regress')
-rw-r--r-- | test/regress/regress0/strings/Makefile.am | 3 | ||||
-rwxr-xr-x | test/regress/regress0/strings/crash-1019.smt2 | 10 |
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)
|