; COMMAND-LINE: --lang=smt2.0
; EXPECT: sat
(set-logic ALL_SUPPORTED)
(set-info :status sat)
(set-option :strings-exp true)
(declare-fun value () String)
(declare-fun name () String)
(assert (not (not (not (= (ite (str.contains value "?") 1 0) 0))))) 
(assert (not (not (= (ite (str.contains value "#") 1 0) 0)))) 
(assert (not (not (= (ite (= (str.substr value 0 (- 2 0)) "//") 1 0) 0)))) 
(assert (not (not (= (ite (> (str.indexof value ":" 0) 0) 1 0) 0)))) 
(assert (not (= (ite (not (= (str.len value) 0)) 1 0) 0))) 
(assert (not (not (= (ite (str.contains value "'") 1 0) 0)))) 
(assert (not (not (= (ite (str.contains value "\"") 1 0) 0)))) 
(assert (not (not (= (ite (str.contains value ">") 1 0) 0)))) 
(assert (not (not (= (ite (str.contains value "<") 1 0) 0)))) 
(assert (not (not (= (ite (str.contains value "&") 1 0) 0)))) 
(assert (not (not (= (ite (str.contains name "'") 1 0) 0)))) 
(assert (not (not (= (ite (str.contains name "\"") 1 0) 0)))) 
(assert (not (not (= (ite (str.contains name ">") 1 0) 0)))) 
(assert (not (not (= (ite (str.contains name "<") 1 0) 0)))) 
(assert (not (not (= (ite (str.contains name "&") 1 0) 0)))) 
(assert (not (= (ite (not (= value "")) 1 0) 0))) 
(assert (not (= (ite (str.contains value "javascript:alert(1);") 1 0) 0))) 
(assert (not (not (= (ite (str.contains name "javascript:alert(1);") 1 0) 0)))) 
(check-sat)