scanning error about stringfuzz HOT 9 CLOSED

(declare-const |aws:SourceArn| String)
(declare-const |aws:SourceArn_account| String)
(declare-const |aws:SourceArn_exists| Bool)
(declare-const |aws:SourceArn_partition| String)
(declare-const |aws:SourceArn_region| String)
(declare-const |aws:SourceArn_resource| String)
(declare-const |aws:SourceArn_service| String)

; Condition: p0.0.0.0
(declare-const p0.0.0.0.condition Bool)
;(assert (= p0.0.0.0.condition (and |aws:SourceArn_exists| (= "arn:aws:myService:myRegion:123456789012:myResource/part" |aws:SourceArn|))))
(assert (= p0.0.0.0.condition (and |aws:SourceArn_exists|
	; SourceArn = arn : partition : service : region : account : resource
	(= |aws:SourceArn_partition| "aws")
	(= |aws:SourceArn_service| "myService")
	(= |aws:SourceArn_region| "myRegion")
	(= |aws:SourceArn_account| "123456789012")
	(= |aws:SourceArn_resource| "myResource/part")
)))

; Statement: p0.0
(declare-const p0.0.statement.allows Bool)
(assert (= p0.0.statement.allows p0.0.0.0.condition))

; Policy: 0
(declare-const p0.allows Bool)
(declare-const p0.denies Bool)
(declare-const p0.neutral Bool)
(assert (= p0.allows p0.0.statement.allows))
(assert (not p0.denies))
(assert (= p0.neutral (not p0.0.statement.allows)))

; Condition: p1.0.0.0
(declare-const p1.0.0.0.condition Bool)
(assert (= p1.0.0.0.condition (and |aws:SourceArn_exists| (and
	(= "aws" |aws:SourceArn_partition|)
	(str.prefixof "my" |aws:SourceArn_service|)
	;(str.in.re |aws:SourceArn_service| (re.++ (str.to.re "my") re.all))
	(and
		(str.prefixof "myR" |aws:SourceArn_region|)
		;(str.in.re |aws:SourceArn_region| (re.++ (str.to.re "myR") re.all))
		(str.suffixof "on" |aws:SourceArn_region|)
		;(str.in.re |aws:SourceArn_region| (re.++ re.all (str.to.re "on")))
	)
	(str.suffixof "012" |aws:SourceArn_account|)
	;(str.in.re |aws:SourceArn_account| (re.++ re.all (str.to.re "012")))
	))))

; Statement: p1.0
(declare-const p1.0.statement.allows Bool)
(assert (= p1.0.statement.allows p1.0.0.0.condition))

; Policy: 1
(declare-const p1.allows Bool)
(declare-const p1.denies Bool)
(declare-const p1.neutral Bool)
(assert (= p1.allows p1.0.statement.allows))
(assert (not p1.denies))
(assert (= p1.neutral (not p1.0.statement.allows)))

; aws:SourceArn invariants
;(assert (= |aws:SourceArn| (str.++ (str.++ (str.++ (str.++ (str.++ (str.++ (str.++ (str.++ (str.++ "arn:" |aws:SourceArn_partition|) ":") |aws:SourceArn_service|) ":") |aws:SourceArn_region|) ":") |aws:SourceArn_account|) ":") |aws:SourceArn_resource|)))

; Goals
(assert (or p0.neutral p0.denies))
(assert p1.allows)
(check-sat)

(get-model)

(declare-const S String)
; S not in aaabbb*
(assert (not (str.in.re S (re.++ (str.to.re "aaabbb") re.all ))))
; S in aaa*bbb*
(assert (str.in.re S (re.++ (re.++ (re.++
 (str.to.re "aaa") re.all ))
 (str.to.re "bbb") re.all )))
(check-sat) ; should be SAT
(get-model)
(get-info :reason-unknown)

(set-logic QF_S)
(set-info :status sat)

(declare-const Username String)
(declare-const Domainname String)
(declare-const Email String)

; username at most 64 chars and can't be empty
(assert (<= (str.len Username) 64))
(assert (> (str.len Username) 0))
; domain at most 256 chars and can't be empty
(assert (<= (str.len Domainname) 256))
(assert (> (str.len Domainname) 0))

; Email = Username ++ "@" ++ Domainname
(assert (= Email (str.++ Username "@" Domainname)))

; Email is matched by the following (very simplistic) pattern:
; (non-empty alphanumeric string) @ (one or more alphanumeric strings separated by periods)
(assert (str.in.re Email (re.++
	;; Username part
	(re.+ (re.union (re.range "a" "z") (re.range "A" "Z") (re.range "0" "9")))
	(str.to.re "@")
	;; Domainname part
	(re.++
		(re.+ (re.++ (re.+ (re.union (re.range "a" "z") (re.range "A" "Z") (re.range "0" "9"))) (str.to.re ".")))
		(re.+ (re.union (re.range "a" "z") (re.range "A" "Z") (re.range "0" "9")))))))

; Domainname is not a FQDN (does not contain '.')
(assert (not (str.in.re Domainname (re.++ (re.* re.all) (str.to.re ".") (re.* re.all)))))

(check-sat)

(set-logic QF_S)
(set-info :status sat)

(declare-const key String)
(declare-const val String)

(define-fun QuoteRegex ((aRegex (RegEx String) )) ( RegEx String)
    (re.++ (re.++ (str.to.re """") aRegex) (str.to.re """")))

(assert (str.in.re key (QuoteRegex (re.* (str.to.re "a")))))

(assert (= (str.len key) 2)) 


(check-sat)
(get-model)

(set-logic QF_S)
(set-info :status unsat)
(declare-const x String)
(declare-const y String)
(assert (str.in.re x (re.+ (str.to.re "ab$!Pd"))))
(assert (str.in.re y (re.* (str.to.re "aAh'{:"))))
(assert (= (str.len x) -2))
(check-sat)
(get-model)