blob: 140c7c659f046a1ce354010d976fc2fff6adde36 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
|
(set-logic ALL_SUPPORTED)
(set-info :status sat)
(set-option :strings-exp true)
(set-option :strings-fmf 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)
|
