(declare-fun r () String) (declare-fun a () String) (assert (let ((a!1 (str.len (str.substr r 0 (+ (- 69) (str.len r))))) (a!2 (str.substr (str.substr r 0 (+ (- 69) (str.len r))) 0 13)) (a!4 (= ":role/aws-service-role/support.amazonaws.com/awsserviceroleforsupport" (str.substr r (+ (- 69) (str.len r)) 69))) (a!6 (str.len (str.substr r 0 (+ (- 10) (str.len r))))) (a!7 (str.substr (str.substr r 0 (+ (- 10) (str.len r))) 0 19)) (a!9 (= "::/account" (str.substr r (+ (- 10) (str.len r)) 10))) (a!11 (str.len (str.substr r 0 (+ (- 7) (str.len r))))) (a!12 (str.substr (str.substr r 0 (+ (- 7) (str.len r))) 0 19)) (a!14 (= "::/apis" (str.substr r (+ (- 7) (str.len r)) 7))) (a!16 (re.++ (re.++ (str.to_re "arn:aws:apigateway:") (re.* (re.range "!" "~"))) (str.to_re "::/apis/"))) (a!18 (= "/authorizers" (str.substr r (+ (- 12) (str.len r)) 12))) (a!19 (= "/deployments" (str.substr r (+ (- 12) (str.len r)) 12))) (a!21 (= "/integrations" (str.substr r (+ (- 13) (str.len r)) 13))) (a!24 (= "/integrationresponses" (str.substr r (+ (- 21) (str.len r)) 21))) (a!26 (= "/models" (str.substr r (+ (- 7) (str.len r)) 7))) (a!27 (= "/routes" (str.substr r (+ (- 7) (str.len r)) 7))) (a!30 (= "/routeresponses" (str.substr r (+ (- 15) (str.len r)) 15))) (a!31 (= "/stages" (str.substr r (+ (- 7) (str.len r)) 7))) (a!32 (str.len (str.substr r 0 (+ (- 21) (str.len r))))) (a!33 (str.substr (str.substr r 0 (+ (- 21) (str.len r))) 0 19)) (a!35 (= "::/clientcertificates" (str.substr r (+ (- 21) (str.len r)) 21))) (a!37 (str.len (str.substr r 0 (+ (- 14) (str.len r))))) (a!38 (str.substr (str.substr r 0 (+ (- 14) (str.len r))) 0 19)) (a!40 (= "::/domainnames" (str.substr r (+ (- 14) (str.len r)) 14))) (a!42 (re.++ (re.++ (str.to_re "arn:aws:apigateway:") (re.* (re.range "!" "~"))) (str.to_re "::/domainnames/"))) (a!44 (= "/apimappings" (str.substr r (+ (- 12) (str.len r)) 12))) (a!46 (= "/basepathmappings" (str.substr r (+ (- 17) (str.len r)) 17))) (a!47 (str.len (str.substr r 0 (+ (- 11) (str.len r))))) (a!48 (str.substr (str.substr r 0 (+ (- 11) (str.len r))) 0 19)) (a!50 (= "::/restapis" (str.substr r (+ (- 11) (str.len r)) 11))) (a!52 (re.++ (re.++ (str.to_re "arn:aws:apigateway:") (re.* (re.range "!" "~"))) (str.to_re "::/restapis/"))) (a!57 (= "/default_template" (str.substr r (+ (- 17) (str.len r)) 17))) (a!59 (= "/resources" (str.substr r (+ (- 10) (str.len r)) 10))) (a!63 (= "/integration" (str.substr r (+ (- 12) (str.len r)) 12))) (a!64 (str.len (str.substr r 0 (+ (- 13) (str.len r))))) (a!65 (str.substr (str.substr r 0 (+ (- 13) (str.len r))) 0 19)) (a!67 (= "::/usageplans" (str.substr r (+ (- 13) (str.len r)) 13))) (a!69 (= "::/vpclinks" (str.substr r (+ (- 11) (str.len r)) 11))) (a!77 (re.++ (re.++ (str.to_re "arn:aws:apigateway:") (re.* (re.range "!" "~"))) (str.to_re "::/clientcertificates/"))) (a!86 (re.++ (re.++ (str.to_re "arn:aws:apigateway:") (re.* (re.range "!" "~"))) (str.to_re "::/usageplans/"))) (a!87 (re.++ (re.++ (str.to_re "arn:aws:apigateway:") (re.* (re.range "!" "~"))) (str.to_re "::/vpclinks/"))) (a!113 (and (or (= a "s3:listaccesspoints") (= a "s3:listaccesspointsforobjectlambda") (= a "s3:listallmybuckets") (= a "s3:listbucket") (= a "s3:listbucketmultipartuploads") (= a "s3:listbucketversions") (= a "s3:listjobs") (= a "s3:listmultiregionaccesspoints") (= a "s3:listmultipartuploadparts") (= a "s3:liststoragelensconfigurations") (= a "s3:describejob") (= a "s3:describemultiregionaccesspointoperation") (= a "s3:getaccelerateconfiguration") (= a "s3:getaccesspoint") (= a "s3:getaccesspointconfigurationforobjectlambda") (= a "s3:getaccesspointforobjectlambda") (= a "s3:getaccesspointpolicy") (= a "s3:getaccesspointpolicyforobjectlambda") (= a "s3:getaccesspointpolicystatus") (= a "s3:getaccesspointpolicystatusforobjectlambda") (= a "s3:getaccountpublicaccessblock") (= a "s3:getanalyticsconfiguration") (= a "s3:getbucketacl") (= a "s3:getbucketcors") (= a "s3:getbucketlocation") (= a "s3:getbucketlogging") (= a "s3:getbucketnotification") (= a "s3:getbucketobjectlockconfiguration") (= a "s3:getbucketownershipcontrols") (= a "s3:getbucketpolicy") (= a "s3:getbucketpolicystatus") (= a "s3:getbucketpublicaccessblock") (= a "s3:getbucketrequestpayment") (= a "s3:getbucketversioning") (= a "s3:getbucketwebsite") (= a "s3:getencryptionconfiguration") (= a "s3:getintelligenttieringconfiguration") (= a "s3:getinventoryconfiguration") (= a "s3:getlifecycleconfiguration") (= a "s3:getmetricsconfiguration") (= a "s3:getmultiregionaccesspoint") (= a "s3:getmultiregionaccesspointpolicy") (= a "s3:getmultiregionaccesspointpolicystatus") (= a "s3:getmultiregionaccesspointroutes") (= a "s3:getobjectlegalhold") (= a "s3:getobjectretention") (= a "s3:getreplicationconfiguration") (= a "s3:getstoragelensconfiguration") (= a "appstream:describeimagebuilders") (= a "appsync:getresolver") (= a "athena:listqueryexecutions") (= a "appstream:describeimages") (= a "athena:listsessions") (= a "athena:listtagsforresource") (= a "access-analyzer:getfinding") (= a "athena:listdatacatalogs") (= a "athena:listengineversions") (= a "access-analyzer:getaccesspreview") (= a "acm-pca:listcertificateauthorities") (= a "access-analyzer:listanalyzers") (= a "amplify:listbackendenvironments") (= a "access-analyzer:listpolicygenerations") (= a "amplify:getbackendenvironment") (= a "amplify:getbranch") (= a "auditmanager:getaccountstatus") (= a "amplify:getjob") (= a "auditmanager:getdelegations") (= a "auditmanager:listassessmentframeworks") (= a "access-analyzer:getgeneratedpolicy") (= a "access-analyzer:listaccesspreviewfindings") (= a "aps:listworkspaces") (= a "aps:listrulegroupsnamespaces") (= a "athena:batchgetnamedquery") (= a "athena:batchgetqueryexecution") (= a "athena:getcalculationexecution") (= a "appsync:listdomainnames") (= a "aps:describeworkspace") (= a "access-analyzer:listfindings") (= a "appstream:describeentitlements") (= a "apprunner:describeservice") (= a "appsync:listtypes") (= a "appstream:listassociatedstacks") (= a "appstream:listentitledapplications") (= a "appstream:describefleets") (= a "application-autoscaling:describescalingactivities") (= a "application-autoscaling:describescalingpolicies") (= a "apprunner:listconnections") (= a "applicationinsights:describeapplication") (= a "apprunner:listoperations") (= a "apprunner:listservices") (= a "athena:listapplicationdpusizes") (= a "athena:listcalculationexecutions") (= a "appsync:getapiassociation") (= a "appsync:getapicache") (= a "appsync:getdomainname") (= a "appsync:getfunction") (= a "appsync:getgraphqlapi") (= a "appsync:getintrospectionschema") (= a "access-analyzer:listaccesspreviews") (= a "access-analyzer:listarchiverules") (= a "amplify:getdomainassociation") (= a "appflow:listflows") (= a "application-autoscaling:describescalabletargets") (= a "amplify:getwebhook") (= a "amplify:listapps") (= a "acm-pca:listtags") (= a "acm:describecertificate") (= a "acm:getaccountconfiguration") (= a "acm:getcertificate") (= a "acm:listcertificates") (= a "acm:listtagsforcertificate") (= a "appsync:gettype") (= a "appsync:listdatasources") (= a "amplify:listdomainassociations") (= a "appstream:listtagsforresource") (= a "appsync:listfunctions") (= a "appsync:listgraphqlapis") (= a "appsync:listresolvers") (= a "athena:getnotebookmetadata") (= a "athena:getnamedquery") (= a "athena:getqueryexecution") (= a "athena:getqueryruntimestatistics") (= a "athena:getsession") (= a "athena:listnotebooksessions") (= a "athena:getdatacatalog") (= a "appstream:describeappblockbuilderappblockassociations") (= a "appstream:describeappblockbuilders") (= a "appstream:describeappblocks") (= a "appstream:describeapplicationfleetassociations") (= a "appstream:describeapplications") (= a "appstream:describedirectoryconfigs") (= a "appsync:listresolversbyfunction") (= a "appsync:listsourceapiassociations") (= a "acm-pca:describecertificateauthority") (= a "acm-pca:getcertificate") (= a "acm-pca:getcertificateauthoritycertificate") (= a "acm-pca:getcertificateauthoritycsr") (= a "appstream:describeimagepermissions") (= a "athena:listexecutors") (= a "athena:listnamedqueries") (= a "athena:listnotebookmetadata") (= a "access-analyzer:listanalyzedresources") (= a "apprunner:describeautoscalingconfiguration") (= a "airflow:listenvironments") (= a "apprunner:describecustomdomains") (= a "apprunner:describeoperation") (= a "amplifyuibuilder:exportcomponents") (= a "amplifyuibuilder:exportthemes") (= a "appflow:describeconnectorentity") (= a "appflow:describeconnectorprofiles") (= a "appflow:describeconnectors") (= a "appflow:describeflow") (= a "athena:getsessionstatus") (= a "athena:getworkgroup") (= a "appsync:getschemacreationstatus") (= a "appsync:getsourceapiassociation") (= a "access-analyzer:getanalyzedresource") (= a "access-analyzer:getanalyzer") (= a "access-analyzer:getarchiverule") (= a "athena:getcalculationexecutionstatus") (= a "apprunner:listautoscalingconfigurations") (= a "acm-pca:describecertificateauthorityauditreport") (= a "amplify:listbranches") (= a "athena:listworkgroups") (= a "airflow:getenvironment") (= a "airflow:listtagsforresource") (= a "amplify:getapp") (= a "appsync:listtypesbyassociation") (= a "aps:describealertmanagerdefinition") (= a "aps:describerulegroupsnamespace") (= a "amplify:listwebhooks") (= a "application-autoscaling:describescheduledactions") (= a "applicationinsights:describecomponent") (= a "applicationinsights:describecomponentconfiguration") (= a "appstream:describeusagereportsubscriptions") (= a "appstream:describestacks") (= a "appstream:describeusers") (= a "appstream:describeuserstackassociations") (= a "appstream:listassociatedfleets") (= a "apprunner:listtagsforresource") (= a "appstream:describesessions") (= a "appflow:describeflowexecutionrecords") (= a "appflow:listconnectorentities") (= a "applicationinsights:describecomponentconfigurationrecommendation") (= a "applicationinsights:describelogpattern") (= a "applicationinsights:describeobservation") (= a "applicationinsights:describeproblem") (= a "applicationinsights:describeproblemobservations") (= a "applicationinsights:listapplications") (= a "applicationinsights:listcomponents") (= a "applicationinsights:listconfigurationhistory") (= a "applicationinsights:listlogpatterns") (= a "applicationinsights:listlogpatternsets") (= a "applicationinsights:listproblems") (= a "appmesh:describegatewayroute") (= a "appmesh:describemesh") (= a "appmesh:describeroute") (= a "appmesh:describevirtualgateway") (= a "appmesh:describevirtualnode") (= a "appmesh:describevirtualrouter") (= a "appmesh:describevirtualservice") (= a "appmesh:listgatewayroutes") (= a "appmesh:listmeshes") (= a "appmesh:listroutes") (= a "appmesh:listtagsforresource") (= a "appmesh:listvirtualgateways") (= a "appmesh:listvirtualnodes") (= a "appmesh:listvirtualrouters") (= a "appmesh:listvirtualservices") (= a "auditmanager:listassessmentreports") (= a "auditmanager:listassessments") (= a "auditmanager:listcontrols") (= a "auditmanager:listkeywordsfordatasource") (= a "auditmanager:listnotifications") (= a "autoscaling-plans:describescalingplanresources") (= a "autoscaling-plans:describescalingplans") (= a "autoscaling-plans:getscalingplanresourceforecastdata") (= a "autoscaling:describeaccountlimits") (= a "autoscaling:describeadjustmenttypes") (= a "autoscaling:describeautoscalinggroups") (= a "autoscaling:describeautoscalinginstances") (= a "autoscaling:describeautoscalingnotificationtypes") (= a "autoscaling:describeinstancerefreshes") (= a "autoscaling:describelaunchconfigurations") (= a "autoscaling:describelifecyclehooks") (= a "autoscaling:describelifecyclehooktypes") (= a "autoscaling:describeloadbalancers") (= a "autoscaling:describeloadbalancertargetgroups") (= a "autoscaling:describemetriccollectiontypes") (= a "autoscaling:describenotificationconfigurations") (= a "autoscaling:describepolicies") (= a "autoscaling:describescalingactivities") (= a "autoscaling:describescalingprocesstypes") (= a "autoscaling:describescheduledactions") (= a "autoscaling:describetags") (= a "autoscaling:describeterminationpolicytypes") (= a "autoscaling:describewarmpool") (= a "backup:describebackupjob") (= a "backup:describebackupvault") (= a "backup:describecopyjob") (= a "backup:describeframework") (= a "backup:describeglobalsettings") (= a "backup:describeprotectedresource") (= a "backup:describerecoverypoint") (= a "backup:describeregionsettings") (= a "backup:describereportjob") (= a "backup:describereportplan") (= a "backup:describerestorejob") (= a "backup:getbackupplan") (= a "backup:getbackupplanfromjson") (= a "backup:getbackupplanfromtemplate") (= a "backup:getbackupselection") (= a "backup:getbackupvaultaccesspolicy") (= a "backup:getbackupvaultnotifications") (= a "backup:getlegalhold") (= a "backup:getrecoverypointrestoremetadata") (= a "backup:getsupportedresourcetypes") (= a "backup:listbackupjobs") (= a "backup:listbackupplans") (= a "backup:listbackupplantemplates") (= a "backup:listbackupplanversions") (= a "backup:listbackupselections") (= a "backup:listbackupvaults") (= a "backup:listcopyjobs") (= a "backup:listframeworks") (= a "backup:listlegalholds") (= a "backup:listprotectedresources") (= a "backup:listrecoverypointsbybackupvault") (= a "backup:listrecoverypointsbylegalhold") (= a "backup:listrecoverypointsbyresource") (= a "backup:listreportjobs") (= a "backup:listreportplans") (= a "backup:listrestorejobs") (= a "backup:listtags") (= a "backup-gateway:getgateway") (= a "backup-gateway:gethypervisor") (= a "backup-gateway:gethypervisorpropertymappings") (= a "backup-gateway:getvirtualmachine") (= a "backup-gateway:listgateways") (= a "backup-gateway:listhypervisors") (= a "backup-gateway:listvirtualmachines") (= a "batch:describecomputeenvironments") (= a "batch:describejobdefinitions") (= a "batch:describejobqueues") (= a "batch:describejobs") (= a "batch:listjobs") (= a "braket:getdevice") (= a "braket:getquantumtask") (= a "braket:searchdevices") (= a "braket:searchquantumtasks") (= a "budgets:viewbudget") (= a "ce:getcostandusage") (= a "ce:getcostandusagewithresources") (= a "ce:getcostforecast") (= a "ce:getdimensionvalues") (= a "ce:getreservationcoverage") (= a "ce:getreservationpurchaserecommendation") (= a "ce:getreservationutilization") (= a "ce:getrightsizingrecommendation") (= a "ce:getsavingsplanscoverage") (= a "ce:getsavingsplanspurchaserecommendation") (= a "ce:getsavingsplansutilization") (= a "ce:getsavingsplansutilizationdetails") (= a "ce:gettags") (= a "chime:describeappinstance") (= a "chime:getattendee") (= a "chime:getglobalsettings") (= a "chime:getmediacapturepipeline") (= a "chime:getmediapipeline") (= a "chime:getmeeting") (= a "chime:getproxysession") (= a "chime:getsipmediaapplication") (= a "chime:getsiprule") (= a "chime:getvoiceconnector") (= a "chime:getvoiceconnectorgroup") (= a "chime:getvoiceconnectorloggingconfiguration") (= a "chime:listappinstances") (= a "chime:listattendees") (= a "chime:listchannelbans") (= a "chime:listchannels") (= a "chime:listchannelsmoderatedbyappinstanceuser") (= a "chime:listmediacapturepipelines") (= a "chime:listmediapipelines") (= a "chime:listmeetings") (= a "chime:listsipmediaapplications") (= a "chime:listsiprules") (= a "chime:listvoiceconnectorgroups") (= a "chime:listvoiceconnectors") (= a "cleanrooms:batchgetcollaborationanalysistemplate") (= a "cleanrooms:batchgetschema") (= a "cleanrooms:getanalysistemplate") (= a "cleanrooms:getcollaboration") (= a "cleanrooms:getcollaborationanalysistemplate") (= a "cleanrooms:getconfiguredtable") (= a "cleanrooms:getconfiguredtableassociation") (= a "cleanrooms:getmembership") (= a "cleanrooms:getschema") (= a "cleanrooms:listanalysistemplates") (= a "cleanrooms:listcollaborationanalysistemplates") (= a "cleanrooms:listcollaborations") (= a "cleanrooms:listconfiguredtableassociations") (= a "cleanrooms:listconfiguredtables") (= a "cleanrooms:listmembers") (= a "cleanrooms:listmemberships") (= a "cleanrooms:listschemas") (= a "cloud9:describeenvironmentmemberships") (= a "cloud9:describeenvironments") (= a "cloud9:listenvironments") (= a "clouddirectory:getdirectory") (= a "clouddirectory:listdirectories") (= a "cloudformation:batchdescribetypeconfigurations") (= a "cloudformation:describeaccountlimits") (= a "cloudformation:describechangeset") (= a "cloudformation:describechangesethooks") (= a "cloudformation:describepublisher") (= a "cloudformation:describestackevents") (= a "cloudformation:describestackinstance") (= a "cloudformation:describestackresource") (= a "cloudformation:describestackresources") (= a "cloudformation:describestacks") (= a "cloudformation:describestackset") (= a "cloudformation:describestacksetoperation") (= a "cloudformation:describetype") (= a "cloudformation:describetyperegistration") (= a "cloudformation:estimatetemplatecost") (= a "cloudformation:getstackpolicy") (= a "cloudformation:gettemplate") (= a "cloudformation:gettemplatesummary") (= a "cloudformation:listchangesets") (= a "cloudformation:listexports") (= a "cloudformation:listimports") (= a "cloudformation:liststackinstances") (= a "cloudformation:liststackresources") (= a "cloudformation:liststacks") (= a "cloudformation:liststacksetoperationresults") (= a "cloudformation:liststacksetoperations") (= a "cloudformation:liststacksets") (= a "cloudformation:listtyperegistrations") (= a "cloudformation:listtypes") (= a "cloudformation:listtypeversions") (= a "cloudfront:describefunction") (= a "cloudfront:getcachepolicy") (= a "cloudfront:getcachepolicyconfig") (= a "cloudfront:getcloudfrontoriginaccessidentity") (= a "cloudfront:getcloudfrontoriginaccessidentityconfig") (= a "cloudfront:getcontinuousdeploymentpolicy") (= a "cloudfront:getcontinuousdeploymentpolicyconfig") (= a "cloudfront:getdistribution") (= a "cloudfront:getdistributionconfig") (= a "cloudfront:getinvalidation") (= a "cloudfront:getkeygroup") (= a "cloudfront:getkeygroupconfig") (= a "cloudfront:getmonitoringsubscription") (= a "cloudfront:getoriginaccesscontrol") (= a "cloudfront:getoriginaccesscontrolconfig") (= a "cloudfront:getoriginrequestpolicy") (= a "cloudfront:getoriginrequestpolicyconfig") (= a "cloudfront:getpublickey") (= a "cloudfront:getpublickeyconfig") (= a "cloudfront:getrealtimelogconfig") (= a "cloudfront:getstreamingdistribution") (= a "cloudfront:getstreamingdistributionconfig") (= a "cloudfront:listcachepolicies") (= a "cloudfront:listcloudfrontoriginaccessidentities") (= a "cloudfront:listcontinuousdeploymentpolicies") (= a "cloudfront:listdistributions") (= a "cloudfront:listdistributionsbycachepolicyid") (= a "cloudfront:listdistributionsbykeygroup") (= a "cloudfront:listdistributionsbyoriginrequestpolicyid") (= a "cloudfront:listdistributionsbyrealtimelogconfig") (= a "cloudfront:listdistributionsbyresponseheaderspolicyid") (= a "cloudfront:listdistributionsbywebaclid") (= a "cloudfront:listfunctions") (= a "cloudfront:listinvalidations") (= a "cloudfront:listkeygroups") (= a "cloudfront:listoriginaccesscontrols") (= a "cloudfront:listoriginrequestpolicies") (= a "cloudfront:listpublickeys") (= a "cloudfront:listrealtimelogconfigs") (= a "cloudfront:liststreamingdistributions") (= a "cloudhsm:describebackups") (= a "cloudhsm:describeclusters") (= a "cloudsearch:describeanalysisschemes") (= a "cloudsearch:describeavailabilityoptions") (= a "cloudsearch:describedomains") (= a "cloudsearch:describeexpressions") (= a "cloudsearch:describeindexfields") (= a "cloudsearch:describescalingparameters") (= a "cloudsearch:describeserviceaccesspolicies") (= a "cloudsearch:describesuggesters") (= a "cloudsearch:listdomainnames") (= a "cloudtrail:describetrails") (= a "cloudtrail:geteventselectors") (= a "cloudtrail:getinsightselectors") (= a "cloudtrail:gettrail") (= a "cloudtrail:gettrailstatus") (= a "cloudtrail:listpublickeys") (= a "cloudtrail:listtags") (= a "cloudtrail:listtrails") (= a "cloudtrail:lookupevents") (= a "cloudwatch:describealarmhistory") (= a "cloudwatch:describealarms") (= a "cloudwatch:describealarmsformetric") (= a "cloudwatch:describeanomalydetectors") (= a "cloudwatch:describeinsightrules") (= a "cloudwatch:getdashboard") (= a "cloudwatch:getinsightrulereport") (= a "cloudwatch:getmetricdata") (= a "cloudwatch:getmetricstatistics") (= a "cloudwatch:getmetricstream") (= a "cloudwatch:listdashboards") (= a "cloudwatch:listmanagedinsightrules") (= a "cloudwatch:listmetrics") (= a "cloudwatch:listmetricstreams") (= a "codeartifact:describedomain") (= a "codeartifact:describepackageversion") (= a "codeartifact:describerepository") (= a "codeartifact:getdomainpermissionspolicy") (= a "codeartifact:getrepositoryendpoint") (= a "codeartifact:getrepositorypermissionspolicy") (= a "codeartifact:listdomains") (= a "codeartifact:listpackages") (= a "codeartifact:listpackageversionassets") (= a "codeartifact:listpackageversions") (= a "codeartifact:listrepositories") (= a "codeartifact:listrepositoriesindomain") (= a "codebuild:batchgetbuildbatches") (= a "codebuild:batchgetbuilds") (= a "codebuild:batchgetprojects") (= a "codebuild:listbuildbatches") (= a "codebuild:listbuildbatchesforproject") (= a "codebuild:listbuilds") (= a "codebuild:listbuildsforproject") (= a "codebuild:listcuratedenvironmentimages") (= a "codebuild:listprojects") (= a "codebuild:listsourcecredentials") (= a "codecommit:batchgetrepositories") (= a "codecommit:getbranch") (= a "codecommit:getrepository") (= a "codecommit:getrepositorytriggers") (= a "codecommit:listbranches") (= a "codecommit:listrepositories") (= a "codedeploy:batchgetapplicationrevisions") (= a "codedeploy:batchgetapplications") (= a "codedeploy:batchgetdeploymentgroups") (= a "codedeploy:batchgetdeploymentinstances") (= a "codedeploy:batchgetdeployments") (= a "codedeploy:batchgetdeploymenttargets") (= a "codedeploy:batchgetonpremisesinstances") (= a "codedeploy:getapplication") (= a "codedeploy:getapplicationrevision") (= a "codedeploy:getdeployment") (= a "codedeploy:getdeploymentconfig") (= a "codedeploy:getdeploymentgroup") (= a "codedeploy:getdeploymentinstance") (= a "codedeploy:getdeploymenttarget") (= a "codedeploy:getonpremisesinstance") (= a "codedeploy:listapplicationrevisions") (= a "codedeploy:listapplications") (= a "codedeploy:listdeploymentconfigs") (= a "codedeploy:listdeploymentgroups") (= a "codedeploy:listdeploymentinstances") (= a "codedeploy:listdeployments") (= a "codedeploy:listdeploymenttargets") (= a "codedeploy:listgithubaccounttokennames") (= a "codedeploy:listonpremisesinstances") (= a "codepipeline:getjobdetails") (= a "codepipeline:getpipeline") (= a "codepipeline:getpipelineexecution") (= a "codepipeline:getpipelinestate") (= a "codepipeline:listactionexecutions") (= a "codepipeline:listactiontypes") (= a "codepipeline:listpipelineexecutions") (= a "codepipeline:listpipelines") (= a "codepipeline:listwebhooks") (= a "codestar:describeproject") (= a "codestar:listprojects") (= a "codestar:listresources") (= a "codestar:listteammembers") (= a "codestar:listuserprofiles") (= a "codestar-connections:getconnection") (= a "codestar-connections:gethost") (= a "codestar-connections:listconnections") (= a "codestar-connections:listhosts") (= a "cognito-identity:describeidentitypool") (= a "cognito-identity:getidentitypoolroles") (= a "cognito-identity:listidentities") (= a "cognito-identity:listidentitypools") (= a "cognito-idp:describeidentityprovider") (= a "cognito-idp:describeresourceserver") (= a "cognito-idp:describeriskconfiguration") (= a "cognito-idp:describeuserimportjob") (= a "cognito-idp:describeuserpool") (= a "cognito-idp:describeuserpoolclient") (= a "cognito-idp:describeuserpooldomain") (= a "cognito-idp:getgroup") (= a "cognito-idp:getuicustomization") (= a "cognito-idp:getuserpoolmfaconfig") (= a "cognito-idp:listgroups") (= a "cognito-idp:listidentityproviders") (= a "cognito-idp:listresourceservers") (= a "cognito-idp:listuserimportjobs") (= a "cognito-idp:listuserpoolclients") (= a "cognito-idp:listuserpools") (= a "cognito-sync:describedataset") (= a "cognito-sync:describeidentitypoolusage") (= a "cognito-sync:describeidentityusage") (= a "cognito-sync:getcognitoevents") (= a "cognito-sync:getidentitypoolconfiguration") (= a "cognito-sync:listdatasets") (= a "cognito-sync:listidentitypoolusage") (= a "comprehend:describedocumentclassificationjob") (= a "comprehend:describedocumentclassifier") (= a "comprehend:describedominantlanguagedetectionjob") (= a "comprehend:describeendpoint") (= a "comprehend:describeentitiesdetectionjob") (= a "comprehend:describeentityrecognizer") (= a "comprehend:describeeventsdetectionjob") (= a "comprehend:describeflywheel") (= a "comprehend:describeflywheeliteration") (= a "comprehend:describekeyphrasesdetectionjob") (= a "comprehend:describepiientitiesdetectionjob") (= a "comprehend:describesentimentdetectionjob") (= a "comprehend:describetargetedsentimentdetectionjob") (= a "comprehend:describetopicsdetectionjob") (= a "comprehend:listdocumentclassificationjobs") (= a "comprehend:listdocumentclassifiers") (= a "comprehend:listdominantlanguagedetectionjobs") (= a "comprehend:listendpoints") (= a "comprehend:listentitiesdetectionjobs") (= a "comprehend:listentityrecognizers") (= a "comprehend:listeventsdetectionjobs") (= a "comprehend:listflywheeliterationhistory") (= a "comprehend:listflywheels") (= a "comprehend:listkeyphrasesdetectionjobs") (= a "comprehend:listpiientitiesdetectionjobs") (= a "comprehend:listsentimentdetectionjobs") (= a "comprehend:listtargetedsentimentdetectionjobs") (= a "comprehend:listtopicsdetectionjobs") (= a "compute-optimizer:getautoscalinggrouprecommendations") (= a "compute-optimizer:getebsvolumerecommendations") (= a "compute-optimizer:getec2instancerecommendations") (= a "compute-optimizer:getec2recommendationprojectedmetrics") (= a "compute-optimizer:getecsservicerecommendations") (= a "compute-optimizer:getecsservicerecommendationprojectedmetrics") (= a "compute-optimizer:getenrollmentstatus") (= a "compute-optimizer:getrecommendationsummaries") (= a "config:batchgetaggregateresourceconfig") (= a "config:batchgetresourceconfig") (= a "config:describeaggregatecompliancebyconfigrules") (= a "config:describeaggregationauthorizations") (= a "config:describecompliancebyconfigrule") (= a "config:describecompliancebyresource") (= a "config:describeconfigruleevaluationstatus") (= a "config:describeconfigrules") (= a "config:describeconfigurationaggregators") (= a "config:describeconfigurationaggregatorsourcesstatus") (= a "config:describeconfigurationrecorders") (= a "config:describeconfigurationrecorderstatus") (= a "config:describeconformancepackcompliance") (= a "config:describeconformancepacks") (= a "config:describeconformancepackstatus") (= a "config:describedeliverychannels") (= a "config:describedeliverychannelstatus") (= a "config:describeorganizationconfigrules") (= a "config:describeorganizationconfigrulestatuses") (= a "config:describeorganizationconformancepacks") (= a "config:describeorganizationconformancepackstatuses") (= a "config:describependingaggregationrequests") (= a "config:describeremediationconfigurations") (= a "config:describeremediationexceptions") (= a "config:describeremediationexecutionstatus") (= a "config:describeretentionconfigurations") (= a "config:getaggregatecompliancedetailsbyconfigrule") (= a "config:getaggregateconfigrulecompliancesummary") (= a "config:getaggregatediscoveredresourcecounts") (= a "config:getaggregateresourceconfig") (= a "config:getcompliancedetailsbyconfigrule") (= a "config:getcompliancedetailsbyresource") (= a "config:getcompliancesummarybyconfigrule") (= a "config:getcompliancesummarybyresourcetype") (= a "config:getconformancepackcompliancedetails") (= a "config:getconformancepackcompliancesummary") (= a "config:getdiscoveredresourcecounts") (= a "config:getorganizationconfigruledetailedstatus") (= a "config:getorganizationconformancepackdetailedstatus") (= a "config:getresourceconfighistory") (= a "config:listaggregatediscoveredresources") (= a "config:listdiscoveredresources") (= a "config:listtagsforresource") (= a "connect:describecontact") (= a "connect:describephonenumber") (= a "connect:describequickconnect") (= a "connect:describeuser") (= a "connect:getcurrentmetricdata") (= a "connect:getmetricdata") (= a "connect:listcontactevaluations") (= a "connect:listevaluationforms") (= a "connect:listevaluationformversions") (= a "connect:listphonenumbersv2") (= a "connect:listquickconnects") (= a "connect:listroutingprofiles") (= a "connect:listsecurityprofiles") (= a "connect:listusers") (= a "connect:listviews") (= a "connect:listviewversions") (=... (= a "storagegateway:listtagsforresource") (= a "storagegateway:listtapes") (= a "storagegateway:listvolumeinitiators") (= a "storagegateway:listvolumerecoverypoints") (= a "storagegateway:listvolumes") (= a "swf:countclosedworkflowexecutions") (= a "swf:countopenworkflowexecutions") (= a "swf:countpendingactivitytasks") (= a "swf:countpendingdecisiontasks") (= a "swf:describeactivitytype") (= a "swf:describedomain") (= a "swf:describeworkflowexecution") (= a "swf:describeworkflowtype") (= a "swf:getworkflowexecutionhistory") (= a "swf:listactivitytypes") (= a "swf:listclosedworkflowexecutions") (= a "swf:listdomains") (= a "swf:listopenworkflowexecutions") (= a "swf:listworkflowtypes") (= a "synthetics:describecanaries") (= a "synthetics:describecanarieslastrun") (= a "synthetics:describeruntimeversions") (= a "synthetics:getcanary") (= a "synthetics:getcanaryruns") (= a "synthetics:getgroup") (= a "synthetics:listassociatedgroups") (= a "synthetics:listgroupresources") (= a "synthetics:listgroups") (= a "tiros:createquery") (= a "tiros:getqueryanswer") (= a "tiros:getqueryexplanation") (= a "transcribe:describelanguagemodel") (= a "transcribe:getcallanalyticscategory") (= a "transcribe:getcallanalyticsjob") (= a "transcribe:getmedicaltranscriptionjob") (= a "transcribe:getmedicalvocabulary") (= a "transcribe:gettranscriptionjob") (= a "transcribe:getvocabulary") (= a "transcribe:getvocabularyfilter") (= a "transcribe:listcallanalyticscategories") (= a "transcribe:listcallanalyticsjobs") (= a "transcribe:listlanguagemodels") (= a "transcribe:listmedicaltranscriptionjobs") (= a "transcribe:listmedicalvocabularies") (= a "transcribe:listtranscriptionjobs") (= a "transcribe:listvocabularies") (= a "transcribe:listvocabularyfilters") (= a "transfer:describeaccess") (= a "transfer:describeagreement") (= a "transfer:describeconnector") (= a "transfer:describeexecution") (= a "transfer:describeprofile") (= a "transfer:describeserver") (= a "transfer:describeuser") (= a "transfer:describeworkflow") (= a "transfer:listaccesses") (= a "transfer:listagreements") (= a "transfer:listconnectors") (= a "transfer:listexecutions") (= a "transfer:listhostkeys") (= a "transfer:listprofiles") (= a "transfer:listservers") (= a "transfer:listtagsforresource") (= a "transfer:listusers") (= a "transfer:listworkflows") (= a "transfer:sendworkflowstepstate") (= a "trustedadvisor:getorganizationrecommendation") (= a "trustedadvisor:getrecommendation") (= a "trustedadvisor:listchecks") (= a "trustedadvisor:listorganizationrecommendationaccounts") (= a "trustedadvisor:listorganizationrecommendationresources") (= a "trustedadvisor:listorganizationrecommendations") (= a "trustedadvisor:listrecommendationresources") (= a "trustedadvisor:listrecommendations") (= a "verifiedpermissions:getidentitysource") (= a "verifiedpermissions:getpolicy") (= a "verifiedpermissions:getpolicystore") (= a "verifiedpermissions:getpolicytemplate") (= a "verifiedpermissions:getschema") (= a "verifiedpermissions:listidentitysources") (= a "verifiedpermissions:listpolicies") (= a "verifiedpermissions:listpolicystores") (= a "verifiedpermissions:listpolicytemplates") (= a "vpc-lattice:getaccesslogsubscription") (= a "vpc-lattice:getauthpolicy") (= a "vpc-lattice:getlistener") (= a "vpc-lattice:getresourcepolicy") (= a "vpc-lattice:getrule") (= a "vpc-lattice:getservice") (= a "vpc-lattice:getservicenetwork") (= a "vpc-lattice:getservicenetworkserviceassociation") (= a "vpc-lattice:getservicenetworkvpcassociation") (= a "vpc-lattice:gettargetgroup") (= a "vpc-lattice:listaccesslogsubscriptions") (= a "vpc-lattice:listlisteners") (= a "vpc-lattice:listrules") (= a "vpc-lattice:listservicenetworks") (= a "vpc-lattice:listservicenetworkserviceassociations") (= a "vpc-lattice:listservicenetworkvpcassociations") (= a "vpc-lattice:listservices") (= a "vpc-lattice:listtargetgroups") (= a "vpc-lattice:listtargets") (= a "waf-regional:getbytematchset") (= a "waf-regional:getchangetokenstatus") (= a "waf-regional:getgeomatchset") (= a "waf-regional:getipset") (= a "waf-regional:getloggingconfiguration") (= a "waf-regional:getratebasedrule") (= a "waf-regional:getregexmatchset") (= a "waf-regional:getregexpatternset") (= a "waf-regional:getrule") (= a "waf-regional:getrulegroup") (= a "waf-regional:getsqlinjectionmatchset") (= a "waf-regional:getwebacl") (= a "waf-regional:getwebaclforresource") (= a "waf-regional:listactivatedrulesinrulegroup") (= a "waf-regional:listbytematchsets") (= a "waf-regional:listgeomatchsets") (= a "waf-regional:listipsets") (= a "waf-regional:listloggingconfigurations") (= a "waf-regional:listratebasedrules") (= a "waf-regional:listregexmatchsets") (= a "waf-regional:listregexpatternsets") (= a "waf-regional:listresourcesforwebacl") (= a "waf-regional:listrulegroups") (= a "waf-regional:listrules") (= a "waf-regional:listsqlinjectionmatchsets") (= a "waf-regional:listwebacls") (= a "waf:getbytematchset") (= a "waf:getchangetokenstatus") (= a "waf:getgeomatchset") (= a "waf:getipset") (= a "waf:getloggingconfiguration") (= a "waf:getratebasedrule") (= a "waf:getregexmatchset") (= a "waf:getregexpatternset") (= a "waf:getrule") (= a "waf:getrulegroup") (= a "waf:getsampledrequests") (= a "waf:getsizeconstraintset") (= a "waf:getsqlinjectionmatchset") (= a "waf:getwebacl") (= a "waf:getxssmatchset") (= a "waf:listactivatedrulesinrulegroup") (= a "waf:listbytematchsets") (= a "waf:listgeomatchsets") (= a "waf:listipsets") (= a "waf:listloggingconfigurations") (= a "waf:listratebasedrules") (= a "waf:listregexmatchsets") (= a "waf:listregexpatternsets") (= a "waf:listrulegroups") (= a "waf:listrules") (= a "waf:listsizeconstraintsets") (= a "waf:listsqlinjectionmatchsets") (= a "waf:listwebacls") (= a "waf:listxssmatchsets") (= a "wafv2:checkcapacity") (= a "wafv2:describemanagedrulegroup") (= a "wafv2:getipset") (= a "wafv2:getloggingconfiguration") (= a "wafv2:getpermissionpolicy") (= a "wafv2:getratebasedstatementmanagedkeys") (= a "wafv2:getregexpatternset") (= a "wafv2:getrulegroup") (= a "wafv2:getsampledrequests") (= a "wafv2:getwebacl") (= a "wafv2:getwebaclforresource") (= a "wafv2:listavailablemanagedrulegroups") (= a "wafv2:listipsets") (= a "wafv2:listloggingconfigurations") (= a "wafv2:listregexpatternsets") (= a "wafv2:listresourcesforwebacl") (= a "wafv2:listrulegroups") (= a "wafv2:listtagsforresource") (= a "wafv2:listwebacls") (= a "workdocs:checkalias") (= a "workdocs:describeavailabledirectories") (= a "workdocs:describeinstances") (= a "workmail:describegroup") (= a "workmail:describeorganization") (= a "workmail:describeresource") (= a "workmail:describeuser") (= a "workmail:listaliases") (= a "workmail:listgroupmembers") (= a "workmail:listgroups") (= a "workmail:listmailboxpermissions") (= a "workmail:listorganizations") (= a "workmail:listresourcedelegates") (= a "workmail:listresources") (= a "workmail:listusers") (= a "workspaces-web:getbrowsersettings") (= a "workspaces-web:getidentityprovider") (= a "workspaces-web:getnetworksettings") (= a "workspaces-web:getportal") (= a "workspaces-web:getportalserviceprovidermetadata") (= a "workspaces-web:gettruststorecertificate") (= a "workspaces-web:getusersettings") (= a "workspaces-web:listbrowsersettings") (= a "workspaces-web:listidentityproviders") (= a "workspaces-web:listnetworksettings") (= a "workspaces-web:listportals") (= a "workspaces-web:listtagsforresource") (= a "workspaces-web:listtruststorecertificates") (= a "workspaces-web:listtruststores") (= a "workspaces-web:listusersettings") (= a "workspaces:describeaccount") (= a "workspaces:describeaccountmodifications") (= a "workspaces:describeipgroups") (= a "workspaces:describetags") (= a "workspaces:describeworkspacebundles") (= a "workspaces:describeworkspacedirectories") (= a "workspaces:describeworkspaceimages") (= a "workspaces:describeworkspaces") (= a "workspaces:describeworkspacesconnectionstatus")) (str.in_re r (re.* (re.range "!" "~")))))) (let ((a!3 (str.substr (str.substr r 0 (+ (- 69) (str.len r))) 13 (+ (- 13) a!1))) (a!8 (str.substr (str.substr r 0 (+ (- 10) (str.len r))) 19 (+ (- 19) a!6))) (a!13 (str.substr (str.substr r 0 (+ (- 7) (str.len r))) 19 (+ (- 19) a!11))) (a!17 (str.in_re (str.substr r 0 (+ (- 12) (str.len r))) (re.++ a!16 (re.* (re.range "!" "~"))))) (a!20 (str.in_re (str.substr r 0 (+ (- 13) (str.len r))) (re.++ a!16 (re.* (re.range "!" "~"))))) (a!22 (re.++ (re.++ a!16 (re.* (re.range "!" "~"))) (str.to_re "/integrations/"))) (a!25 (str.in_re (str.substr r 0 (+ (- 7) (str.len r))) (re.++ a!16 (re.* (re.range "!" "~"))))) (a!28 (re.++ (re.++ a!16 (re.* (re.range "!" "~"))) (str.to_re "/routes/"))) (a!34 (str.substr (str.substr r 0 (+ (- 21) (str.len r))) 19 (+ (- 19) a!32))) (a!39 (str.substr (str.substr r 0 (+ (- 14) (str.len r))) 19 (+ (- 19) a!37))) (a!43 (str.in_re (str.substr r 0 (+ (- 12) (str.len r))) (re.++ a!42 (re.* (re.range "!" "~"))))) (a!45 (str.in_re (str.substr r 0 (+ (- 17) (str.len r))) (re.++ a!42 (re.* (re.range "!" "~"))))) (a!49 (str.substr (str.substr r 0 (+ (- 11) (str.len r))) 19 (+ (- 19) a!47))) (a!53 (str.in_re (str.substr r 0 (+ (- 12) (str.len r))) (re.++ a!52 (re.* (re.range "!" "~"))))) (a!54 (str.in_re (str.substr r 0 (+ (- 7) (str.len r))) (re.++ a!52 (re.* (re.range "!" "~"))))) (a!55 (re.++ (re.++ a!52 (re.* (re.range "!" "~"))) (str.to_re "/models/"))) (a!58 (str.in_re (str.substr r 0 (+ (- 10) (str.len r))) (re.++ a!52 (re.* (re.range "!" "~"))))) (a!60 (re.++ (re.++ a!52 (re.* (re.range "!" "~"))) (str.to_re "/resources/"))) (a!66 (str.substr (str.substr r 0 (+ (- 13) (str.len r))) 19 (+ (- 19) a!64))) (a!71 (re.++ (re.++ a!16 (re.* (re.range "!" "~"))) (str.to_re "/authorizers/"))) (a!72 (re.++ (re.++ a!16 (re.* (re.range "!" "~"))) (str.to_re "/deployments/"))) (a!74 (re.++ (re.++ a!16 (re.* (re.range "!" "~"))) (str.to_re "/models/"))) (a!76 (re.++ (re.++ a!16 (re.* (re.range "!" "~"))) (str.to_re "/stages/"))) (a!78 (re.++ (re.++ a!42 (re.* (re.range "!" "~"))) (str.to_re "/apimappings/"))) (a!79 (re.++ (re.++ a!42 (re.* (re.range "!" "~"))) (str.to_re "/basepathmappings/"))) (a!80 (re.++ (re.++ a!52 (re.* (re.range "!" "~"))) (str.to_re "/authorizers/"))) (a!81 (re.++ (re.++ a!52 (re.* (re.range "!" "~"))) (str.to_re "/deployments/"))) (a!84 (re.++ (re.++ a!52 (re.* (re.range "!" "~"))) (str.to_re "/stages/"))) (a!88 (re.union (re.++ a!86 (re.* (re.range "!" "~"))) (re.++ a!87 (re.* (re.range "!" "~")))))) (let ((a!5 (and (= a "iam:deleterole") (>= (str.len r) 69) (>= a!1 13) (= a!2 "arn:aws:iam::") (str.in_re a!3 (re.* (re.range "!" "~"))) a!4)) (a!10 (and (>= (str.len r) 10) (>= a!6 19) (= a!7 "arn:aws:apigateway:") (str.in_re a!8 (re.* (re.range "!" "~"))) a!9)) (a!15 (and (>= (str.len r) 7) (>= a!11 19) (= a!12 "arn:aws:apigateway:") (str.in_re a!13 (re.* (re.range "!" "~"))) a!14)) (a!23 (str.in_re (str.substr r 0 (+ (- 21) (str.len r))) (re.++ a!22 (re.* (re.range "!" "~"))))) (a!29 (str.in_re (str.substr r 0 (+ (- 15) (str.len r))) (re.++ a!28 (re.* (re.range "!" "~"))))) (a!36 (and (>= (str.len r) 21) (>= a!32 19) (= a!33 "arn:aws:apigateway:") (str.in_re a!34 (re.* (re.range "!" "~"))) a!35)) (a!41 (and (>= (str.len r) 14) (>= a!37 19) (= a!38 "arn:aws:apigateway:") (str.in_re a!39 (re.* (re.range "!" "~"))) a!40)) (a!51 (and (>= (str.len r) 11) (>= a!47 19) (= a!48 "arn:aws:apigateway:") (str.in_re a!49 (re.* (re.range "!" "~"))) a!50)) (a!56 (str.in_re (str.substr r 0 (+ (- 17) (str.len r))) (re.++ a!55 (re.* (re.range "!" "~"))))) (a!61 (re.++ (re.++ a!60 (re.* (re.range "!" "~"))) (str.to_re "/methods/"))) (a!68 (and (>= (str.len r) 13) (>= a!64 19) (= a!65 "arn:aws:apigateway:") (str.in_re a!66 (re.* (re.range "!" "~"))) a!67)) (a!70 (and (>= (str.len r) 11) (>= a!47 19) (= a!48 "arn:aws:apigateway:") (str.in_re a!49 (re.* (re.range "!" "~"))) a!69)) (a!73 (re.++ (re.++ a!22 (re.* (re.range "!" "~"))) (str.to_re "/integrationresponses/"))) (a!75 (re.++ (re.++ a!28 (re.* (re.range "!" "~"))) (str.to_re "/routeresponses/"))) (a!85 (re.++ (re.++ a!84 (re.* (re.range "!" "~"))) (str.to_re "/sdks/")))) (let ((a!62 (str.in_re (str.substr r 0 (+ (- 12) (str.len r))) (re.++ a!61 (re.* (re.range "!" "~"))))) (a!82 (re.++ (re.++ a!61 (re.* (re.range "!" "~"))) (str.to_re "/integration/responses/"))) (a!83 (re.++ (re.++ a!61 (re.* (re.range "!" "~"))) (str.to_re "/responses/"))) (a!89 (re.union (re.++ a!85 (re.* (re.range "!" "~"))) a!88))) (let ((a!90 (re.union (re.++ a!84 (re.* (re.range "!" "~"))) a!89))) (let ((a!91 (re.union (re.++ a!83 (re.* (re.range "!" "~"))) a!90))) (let ((a!92 (re.union (re.++ a!82 (re.* (re.range "!" "~"))) a!91))) (let ((a!93 (re.union (re.++ a!61 (re.* (re.range "!" "~"))) a!92))) (let ((a!94 (re.union (re.++ a!60 (re.* (re.range "!" "~"))) a!93))) (let ((a!95 (re.union (re.++ a!55 (re.* (re.range "!" "~"))) a!94))) (let ((a!96 (re.union (re.++ a!81 (re.* (re.range "!" "~"))) a!95))) (let ((a!97 (re.union (re.++ a!80 (re.* (re.range "!" "~"))) a!96))) (let ((a!98 (re.union (re.++ a!52 (re.* (re.range "!" "~"))) a!97))) (let ((a!99 (re.union (re.++ a!79 (re.* (re.range "!" "~"))) a!98))) (let ((a!100 (re.union (re.++ a!78 (re.* (re.range "!" "~"))) a!99))) (let ((a!101 (re.union (re.++ a!42 (re.* (re.range "!" "~"))) a!100))) (let ((a!102 (re.union (re.++ a!77 (re.* (re.range "!" "~"))) a!101))) (let ((a!103 (re.union (re.++ a!76 (re.* (re.range "!" "~"))) a!102))) (let ((a!104 (re.union (re.++ a!75 (re.* (re.range "!" "~"))) a!103))) (let ((a!105 (re.union (re.++ a!28 (re.* (re.range "!" "~"))) a!104))) (let ((a!106 (re.union (re.++ a!74 (re.* (re.range "!" "~"))) a!105))) (let ((a!107 (re.union (re.++ a!73 (re.* (re.range "!" "~"))) a!106))) (let ((a!108 (re.union (re.++ a!22 (re.* (re.range "!" "~"))) a!107))) (let ((a!109 (re.union (re.++ a!72 (re.* (re.range "!" "~"))) a!108))) (let ((a!110 (re.union (re.++ a!71 (re.* (re.range "!" "~"))) a!109))) (let ((a!111 (re.union (re.++ a!16 (re.* (re.range "!" "~"))) a!110))) (let ((a!112 (or a!10 a!15 (and (>= (str.len r) 12) a!17 a!18) (and (>= (str.len r) 12) a!17 a!19) (and (>= (str.len r) 13) a!20 a!21) (and (>= (str.len r) 21) a!23 a!24) (and (>= (str.len r) 7) a!25 a!26) (and (>= (str.len r) 7) a!25 a!27) (and (>= (str.len r) 15) a!29 a!30) (and (>= (str.len r) 7) a!25 a!31) a!36 a!41 (and (>= (str.len r) 12) a!43 a!44) (and (>= (str.len r) 17) a!45 a!46) a!51 (and (>= (str.len r) 12) a!53 a!18) (and (>= (str.len r) 12) a!53 a!19) (and (>= (str.len r) 7) a!54 a!26) (and (>= (str.len r) 17) a!56 a!57) (and (>= (str.len r) 10) a!58 a!59) (and (>= (str.len r) 12) a!62 a!63) (and (>= (str.len r) 7) a!54 a!31) a!68 a!70 (str.in_re r a!111)))) (or a!5 (and (= a "apigateway:get") a!112) a!113))))))))))))))))))))))))))))) (assert (str.prefixof "s3:" a)) (model-add r () String "") (model-add a () String "s3:listaccesspoints") (declare-fun r () String) (declare-fun a () String) (assert (let ((a!1 (str.len (str.substr r 0 (+ (- 69) (str.len r))))) (a!2 (str.substr (str.substr r 0 (+ (- 69) (str.len r))) 0 13)) (a!4 (= ":role/aws-service-role/support.amazonaws.com/awsserviceroleforsupport" (str.substr r (+ (- 69) (str.len r)) 69))) (a!6 (str.len (str.substr r 0 (+ (- 10) (str.len r))))) (a!7 (str.substr (str.substr r 0 (+ (- 10) (str.len r))) 0 19)) (a!9 (= "::/account" (str.substr r (+ (- 10) (str.len r)) 10))) (a!11 (str.len (str.substr r 0 (+ (- 7) (str.len r))))) (a!12 (str.substr (str.substr r 0 (+ (- 7) (str.len r))) 0 19)) (a!14 (= "::/apis" (str.substr r (+ (- 7) (str.len r)) 7))) (a!16 (re.++ (re.++ (str.to_re "arn:aws:apigateway:") (re.* (re.range "!" "~"))) (str.to_re "::/apis/"))) (a!18 (= "/authorizers" (str.substr r (+ (- 12) (str.len r)) 12))) (a!19 (= "/deployments" (str.substr r (+ (- 12) (str.len r)) 12))) (a!21 (= "/integrations" (str.substr r (+ (- 13) (str.len r)) 13))) (a!24 (= "/integrationresponses" (str.substr r (+ (- 21) (str.len r)) 21))) (a!26 (= "/models" (str.substr r (+ (- 7) (str.len r)) 7))) (a!27 (= "/routes" (str.substr r (+ (- 7) (str.len r)) 7))) (a!30 (= "/routeresponses" (str.substr r (+ (- 15) (str.len r)) 15))) (a!31 (= "/stages" (str.substr r (+ (- 7) (str.len r)) 7))) (a!32 (str.len (str.substr r 0 (+ (- 21) (str.len r))))) (a!33 (str.substr (str.substr r 0 (+ (- 21) (str.len r))) 0 19)) (a!35 (= "::/clientcertificates" (str.substr r (+ (- 21) (str.len r)) 21))) (a!37 (str.len (str.substr r 0 (+ (- 14) (str.len r))))) (a!38 (str.substr (str.substr r 0 (+ (- 14) (str.len r))) 0 19)) (a!40 (= "::/domainnames" (str.substr r (+ (- 14) (str.len r)) 14))) (a!42 (re.++ (re.++ (str.to_re "arn:aws:apigateway:") (re.* (re.range "!" "~"))) (str.to_re "::/domainnames/"))) (a!44 (= "/apimappings" (str.substr r (+ (- 12) (str.len r)) 12))) (a!46 (= "/basepathmappings" (str.substr r (+ (- 17) (str.len r)) 17))) (a!47 (str.len (str.substr r 0 (+ (- 11) (str.len r))))) (a!48 (str.substr (str.substr r 0 (+ (- 11) (str.len r))) 0 19)) (a!50 (= "::/restapis" (str.substr r (+ (- 11) (str.len r)) 11))) (a!52 (re.++ (re.++ (str.to_re "arn:aws:apigateway:") (re.* (re.range "!" "~"))) (str.to_re "::/restapis/"))) (a!57 (= "/default_template" (str.substr r (+ (- 17) (str.len r)) 17))) (a!59 (= "/resources" (str.substr r (+ (- 10) (str.len r)) 10))) (a!63 (= "/integration" (str.substr r (+ (- 12) (str.len r)) 12))) (a!64 (str.len (str.substr r 0 (+ (- 13) (str.len r))))) (a!65 (str.substr (str.substr r 0 (+ (- 13) (str.len r))) 0 19)) (a!67 (= "::/usageplans" (str.substr r (+ (- 13) (str.len r)) 13))) (a!69 (= "::/vpclinks" (str.substr r (+ (- 11) (str.len r)) 11))) (a!77 (re.++ (re.++ (str.to_re "arn:aws:apigateway:") (re.* (re.range "!" "~"))) (str.to_re "::/clientcertificates/"))) (a!86 (re.++ (re.++ (str.to_re "arn:aws:apigateway:") (re.* (re.range "!" "~"))) (str.to_re "::/usageplans/"))) (a!87 (re.++ (re.++ (str.to_re "arn:aws:apigateway:") (re.* (re.range "!" "~"))) (str.to_re "::/vpclinks/"))) (a!113 (and (or (= a "s3:listaccesspoints") (= a "s3:listaccesspointsforobjectlambda") (= a "s3:listallmybuckets") (= a "s3:listbucket") (= a "s3:listbucketmultipartuploads") (= a "s3:listbucketversions") (= a "s3:listjobs") (= a "s3:listmultiregionaccesspoints") (= a "s3:listmultipartuploadparts") (= a "s3:liststoragelensconfigurations") (= a "s3:describejob") (= a "s3:describemultiregionaccesspointoperation") (= a "s3:getaccelerateconfiguration") (= a "s3:getaccesspoint") (= a "s3:getaccesspointconfigurationforobjectlambda") (= a "s3:getaccesspointforobjectlambda") (= a "s3:getaccesspointpolicy") (= a "s3:getaccesspointpolicyforobjectlambda") (= a "s3:getaccesspointpolicystatus") (= a "s3:getaccesspointpolicystatusforobjectlambda") (= a "s3:getaccountpublicaccessblock") (= a "s3:getanalyticsconfiguration") (= a "s3:getbucketacl") (= a "s3:getbucketcors") (= a "s3:getbucketlocation") (= a "s3:getbucketlogging") (= a "s3:getbucketnotification") (= a "s3:getbucketobjectlockconfiguration") (= a "s3:getbucketownershipcontrols") (= a "s3:getbucketpolicy") (= a "s3:getbucketpolicystatus") (= a "s3:getbucketpublicaccessblock") (= a "s3:getbucketrequestpayment") (= a "s3:getbucketversioning") (= a "s3:getbucketwebsite") (= a "s3:getencryptionconfiguration") (= a "s3:getintelligenttieringconfiguration") (= a "s3:getinventoryconfiguration") (= a "s3:getlifecycleconfiguration") (= a "s3:getmetricsconfiguration") (= a "s3:getmultiregionaccesspoint") (= a "s3:getmultiregionaccesspointpolicy") (= a "s3:getmultiregionaccesspointpolicystatus") (= a "s3:getmultiregionaccesspointroutes") (= a "s3:getobjectlegalhold") (= a "s3:getobjectretention") (= a "s3:getreplicationconfiguration") (= a "s3:getstoragelensconfiguration") (= a "appstream:describeimagebuilders") (= a "appsync:getresolver") (= a "athena:listqueryexecutions") (= a "appstream:describeimages") (= a "athena:listsessions") (= a "athena:listtagsforresource") (= a "access-analyzer:getfinding") (= a "athena:listdatacatalogs") (= a "athena:listengineversions") (= a "access-analyzer:getaccesspreview") (= a "acm-pca:listcertificateauthorities") (= a "access-analyzer:listanalyzers") (= a "amplify:listbackendenvironments") (= a "access-analyzer:listpolicygenerations") (= a "amplify:getbackendenvironment") (= a "amplify:getbranch") (= a "auditmanager:getaccountstatus") (= a "amplify:getjob") (= a "auditmanager:getdelegations") (= a "auditmanager:listassessmentframeworks") (= a "access-analyzer:getgeneratedpolicy") (= a "access-analyzer:listaccesspreviewfindings") (= a "aps:listworkspaces") (= a "aps:listrulegroupsnamespaces") (= a "athena:batchgetnamedquery") (= a "athena:batchgetqueryexecution") (= a "athena:getcalculationexecution") (= a "appsync:listdomainnames") (= a "aps:describeworkspace") (= a "access-analyzer:listfindings") (= a "appstream:describeentitlements") (= a "apprunner:describeservice") (= a "appsync:listtypes") (= a "appstream:listassociatedstacks") (= a "appstream:listentitledapplications") (= a "appstream:describefleets") (= a "application-autoscaling:describescalingactivities") (= a "application-autoscaling:describescalingpolicies") (= a "apprunner:listconnections") (= a "applicationinsights:describeapplication") (= a "apprunner:listoperations") (= a "apprunner:listservices") (= a "athena:listapplicationdpusizes") (= a "athena:listcalculationexecutions") (= a "appsync:getapiassociation") (= a "appsync:getapicache") (= a "appsync:getdomainname") (= a "appsync:getfunction") (= a "appsync:getgraphqlapi") (= a "appsync:getintrospectionschema") (= a "access-analyzer:listaccesspreviews") (= a "access-analyzer:listarchiverules") (= a "amplify:getdomainassociation") (= a "appflow:listflows") (= a "application-autoscaling:describescalabletargets") (= a "amplify:getwebhook") (= a "amplify:listapps") (= a "acm-pca:listtags") (= a "acm:describecertificate") (= a "acm:getaccountconfiguration") (= a "acm:getcertificate") (= a "acm:listcertificates") (= a "acm:listtagsforcertificate") (= a "appsync:gettype") (= a "appsync:listdatasources") (= a "amplify:listdomainassociations") (= a "appstream:listtagsforresource") (= a "appsync:listfunctions") (= a "appsync:listgraphqlapis") (= a "appsync:listresolvers") (= a "athena:getnotebookmetadata") (= a "athena:getnamedquery") (= a "athena:getqueryexecution") (= a "athena:getqueryruntimestatistics") (= a "athena:getsession") (= a "athena:listnotebooksessions") (= a "athena:getdatacatalog") (= a "appstream:describeappblockbuilderappblockassociations") (= a "appstream:describeappblockbuilders") (= a "appstream:describeappblocks") (= a "appstream:describeapplicationfleetassociations") (= a "appstream:describeapplications") (= a "appstream:describedirectoryconfigs") (= a "appsync:listresolversbyfunction") (= a "appsync:listsourceapiassociations") (= a "acm-pca:describecertificateauthority") (= a "acm-pca:getcertificate") (= a "acm-pca:getcertificateauthoritycertificate") (= a "acm-pca:getcertificateauthoritycsr") (= a "appstream:describeimagepermissions") (= a "athena:listexecutors") (= a "athena:listnamedqueries") (= a "athena:listnotebookmetadata") (= a "access-analyzer:listanalyzedresources") (= a "apprunner:describeautoscalingconfiguration") (= a "airflow:listenvironments") (= a "apprunner:describecustomdomains") (= a "apprunner:describeoperation") (= a "amplifyuibuilder:exportcomponents") (= a "amplifyuibuilder:exportthemes") (= a "appflow:describeconnectorentity") (= a "appflow:describeconnectorprofiles") (= a "appflow:describeconnectors") (= a "appflow:describeflow") (= a "athena:getsessionstatus") (= a "athena:getworkgroup") (= a "appsync:getschemacreationstatus") (= a "appsync:getsourceapiassociation") (= a "access-analyzer:getanalyzedresource") (= a "access-analyzer:getanalyzer") (= a "access-analyzer:getarchiverule") (= a "athena:getcalculationexecutionstatus") (= a "apprunner:listautoscalingconfigurations") (= a "acm-pca:describecertificateauthorityauditreport") (= a "amplify:listbranches") (= a "athena:listworkgroups") (= a "airflow:getenvironment") (= a "airflow:listtagsforresource") (= a "amplify:getapp") (= a "appsync:listtypesbyassociation") (= a "aps:describealertmanagerdefinition") (= a "aps:describerulegroupsnamespace") (= a "amplify:listwebhooks") (= a "application-autoscaling:describescheduledactions") (= a "applicationinsights:describecomponent") (= a "applicationinsights:describecomponentconfiguration") (= a "appstream:describeusagereportsubscriptions") (= a "appstream:describestacks") (= a "appstream:describeusers") (= a "appstream:describeuserstackassociations") (= a "appstream:listassociatedfleets") (= a "apprunner:listtagsforresource") (= a "appstream:describesessions") (= a "appflow:describeflowexecutionrecords") (= a "appflow:listconnectorentities") (= a "applicationinsights:describecomponentconfigurationrecommendation") (= a "applicationinsights:describelogpattern") (= a "applicationinsights:describeobservation") (= a "applicationinsights:describeproblem") (= a "applicationinsights:describeproblemobservations") (= a "applicationinsights:listapplications") (= a "applicationinsights:listcomponents") (= a "applicationinsights:listconfigurationhistory") (= a "applicationinsights:listlogpatterns") (= a "applicationinsights:listlogpatternsets") (= a "applicationinsights:listproblems") (= a "appmesh:describegatewayroute") (= a "appmesh:describemesh") (= a "appmesh:describeroute") (= a "appmesh:describevirtualgateway") (= a "appmesh:describevirtualnode") (= a "appmesh:describevirtualrouter") (= a "appmesh:describevirtualservice") (= a "appmesh:listgatewayroutes") (= a "appmesh:listmeshes") (= a "appmesh:listroutes") (= a "appmesh:listtagsforresource") (= a "appmesh:listvirtualgateways") (= a "appmesh:listvirtualnodes") (= a "appmesh:listvirtualrouters") (= a "appmesh:listvirtualservices") (= a "auditmanager:listassessmentreports") (= a "auditmanager:listassessments") (= a "auditmanager:listcontrols") (= a "auditmanager:listkeywordsfordatasource") (= a "auditmanager:listnotifications") (= a "autoscaling-plans:describescalingplanresources") (= a "autoscaling-plans:describescalingplans") (= a "autoscaling-plans:getscalingplanresourceforecastdata") (= a "autoscaling:describeaccountlimits") (= a "autoscaling:describeadjustmenttypes") (= a "autoscaling:describeautoscalinggroups") (= a "autoscaling:describeautoscalinginstances") (= a "autoscaling:describeautoscalingnotificationtypes") (= a "autoscaling:describeinstancerefreshes") (= a "autoscaling:describelaunchconfigurations") (= a "autoscaling:describelifecyclehooks") (= a "autoscaling:describelifecyclehooktypes") (= a "autoscaling:describeloadbalancers") (= a "autoscaling:describeloadbalancertargetgroups") (= a "autoscaling:describemetriccollectiontypes") (= a "autoscaling:describenotificationconfigurations") (= a "autoscaling:describepolicies") (= a "autoscaling:describescalingactivities") (= a "autoscaling:describescalingprocesstypes") (= a "autoscaling:describescheduledactions") (= a "autoscaling:describetags") (= a "autoscaling:describeterminationpolicytypes") (= a "autoscaling:describewarmpool") (= a "backup:describebackupjob") (= a "backup:describebackupvault") (= a "backup:describecopyjob") (= a "backup:describeframework") (= a "backup:describeglobalsettings") (= a "backup:describeprotectedresource") (= a "backup:describerecoverypoint") (= a "backup:describeregionsettings") (= a "backup:describereportjob") (= a "backup:describereportplan") (= a "backup:describerestorejob") (= a "backup:getbackupplan") (= a "backup:getbackupplanfromjson") (= a "backup:getbackupplanfromtemplate") (= a "backup:getbackupselection") (= a "backup:getbackupvaultaccesspolicy") (= a "backup:getbackupvaultnotifications") (= a "backup:getlegalhold") (= a "backup:getrecoverypointrestoremetadata") (= a "backup:getsupportedresourcetypes") (= a "backup:listbackupjobs") (= a "backup:listbackupplans") (= a "backup:listbackupplantemplates") (= a "backup:listbackupplanversions") (= a "backup:listbackupselections") (= a "backup:listbackupvaults") (= a "backup:listcopyjobs") (= a "backup:listframeworks") (= a "backup:listlegalholds") (= a "backup:listprotectedresources") (= a "backup:listrecoverypointsbybackupvault") (= a "backup:listrecoverypointsbylegalhold") (= a "backup:listrecoverypointsbyresource") (= a "backup:listreportjobs") (= a "backup:listreportplans") (= a "backup:listrestorejobs") (= a "backup:listtags") (= a "backup-gateway:getgateway") (= a "backup-gateway:gethypervisor") (= a "backup-gateway:gethypervisorpropertymappings") (= a "backup-gateway:getvirtualmachine") (= a "backup-gateway:listgateways") (= a "backup-gateway:listhypervisors") (= a "backup-gateway:listvirtualmachines") (= a "batch:describecomputeenvironments") (= a "batch:describejobdefinitions") (= a "batch:describejobqueues") (= a "batch:describejobs") (= a "batch:listjobs") (= a "braket:getdevice") (= a "braket:getquantumtask") (= a "braket:searchdevices") (= a "braket:searchquantumtasks") (= a "budgets:viewbudget") (= a "ce:getcostandusage") (= a "ce:getcostandusagewithresources") (= a "ce:getcostforecast") (= a "ce:getdimensionvalues") (= a "ce:getreservationcoverage") (= a "ce:getreservationpurchaserecommendation") (= a "ce:getreservationutilization") (= a "ce:getrightsizingrecommendation") (= a "ce:getsavingsplanscoverage") (= a "ce:getsavingsplanspurchaserecommendation") (= a "ce:getsavingsplansutilization") (= a "ce:getsavingsplansutilizationdetails") (= a "ce:gettags") (= a "chime:describeappinstance") (= a "chime:getattendee") (= a "chime:getglobalsettings") (= a "chime:getmediacapturepipeline") (= a "chime:getmediapipeline") (= a "chime:getmeeting") (= a "chime:getproxysession") (= a "chime:getsipmediaapplication") (= a "chime:getsiprule") (= a "chime:getvoiceconnector") (= a "chime:getvoiceconnectorgroup") (= a "chime:getvoiceconnectorloggingconfiguration") (= a "chime:listappinstances") (= a "chime:listattendees") (= a "chime:listchannelbans") (= a "chime:listchannels") (= a "chime:listchannelsmoderatedbyappinstanceuser") (= a "chime:listmediacapturepipelines") (= a "chime:listmediapipelines") (= a "chime:listmeetings") (= a "chime:listsipmediaapplications") (= a "chime:listsiprules") (= a "chime:listvoiceconnectorgroups") (= a "chime:listvoiceconnectors") (= a "cleanrooms:batchgetcollaborationanalysistemplate") (= a "cleanrooms:batchgetschema") (= a "cleanrooms:getanalysistemplate") (= a "cleanrooms:getcollaboration") (= a "cleanrooms:getcollaborationanalysistemplate") (= a "cleanrooms:getconfiguredtable") (= a "cleanrooms:getconfiguredtableassociation") (= a "cleanrooms:getmembership") (= a "cleanrooms:getschema") (= a "cleanrooms:listanalysistemplates") (= a "cleanrooms:listcollaborationanalysistemplates") (= a "cleanrooms:listcollaborations") (= a "cleanrooms:listconfiguredtableassociations") (= a "cleanrooms:listconfiguredtables") (= a "cleanrooms:listmembers") (= a "cleanrooms:listmemberships") (= a "cleanrooms:listschemas") (= a "cloud9:describeenvironmentmemberships") (= a "cloud9:describeenvironments") (= a "cloud9:listenvironments") (= a "clouddirectory:getdirectory") (= a "clouddirectory:listdirectories") (= a "cloudformation:batchdescribetypeconfigurations") (= a "cloudformation:describeaccountlimits") (= a "cloudformation:describechangeset") (= a "cloudformation:describechangesethooks") (= a "cloudformation:describepublisher") (= a "cloudformation:describestackevents") (= a "cloudformation:describestackinstance") (= a "cloudformation:describestackresource") (= a "cloudformation:describestackresources") (= a "cloudformation:describestacks") (= a "cloudformation:describestackset") (= a "cloudformation:describestacksetoperation") (= a "cloudformation:describetype") (= a "cloudformation:describetyperegistration") (= a "cloudformation:estimatetemplatecost") (= a "cloudformation:getstackpolicy") (= a "cloudformation:gettemplate") (= a "cloudformation:gettemplatesummary") (= a "cloudformation:listchangesets") (= a "cloudformation:listexports") (= a "cloudformation:listimports") (= a "cloudformation:liststackinstances") (= a "cloudformation:liststackresources") (= a "cloudformation:liststacks") (= a "cloudformation:liststacksetoperationresults") (= a "cloudformation:liststacksetoperations") (= a "cloudformation:liststacksets") (= a "cloudformation:listtyperegistrations") (= a "cloudformation:listtypes") (= a "cloudformation:listtypeversions") (= a "cloudfront:describefunction") (= a "cloudfront:getcachepolicy") (= a "cloudfront:getcachepolicyconfig") (= a "cloudfront:getcloudfrontoriginaccessidentity") (= a "cloudfront:getcloudfrontoriginaccessidentityconfig") (= a "cloudfront:getcontinuousdeploymentpolicy") (= a "cloudfront:getcontinuousdeploymentpolicyconfig") (= a "cloudfront:getdistribution") (= a "cloudfront:getdistributionconfig") (= a "cloudfront:getinvalidation") (= a "cloudfront:getkeygroup") (= a "cloudfront:getkeygroupconfig") (= a "cloudfront:getmonitoringsubscription") (= a "cloudfront:getoriginaccesscontrol") (= a "cloudfront:getoriginaccesscontrolconfig") (= a "cloudfront:getoriginrequestpolicy") (= a "cloudfront:getoriginrequestpolicyconfig") (= a "cloudfront:getpublickey") (= a "cloudfront:getpublickeyconfig") (= a "cloudfront:getrealtimelogconfig") (= a "cloudfront:getstreamingdistribution") (= a "cloudfront:getstreamingdistributionconfig") (= a "cloudfront:listcachepolicies") (= a "cloudfront:listcloudfrontoriginaccessidentities") (= a "cloudfront:listcontinuousdeploymentpolicies") (= a "cloudfront:listdistributions") (= a "cloudfront:listdistributionsbycachepolicyid") (= a "cloudfront:listdistributionsbykeygroup") (= a "cloudfront:listdistributionsbyoriginrequestpolicyid") (= a "cloudfront:listdistributionsbyrealtimelogconfig") (= a "cloudfront:listdistributionsbyresponseheaderspolicyid") (= a "cloudfront:listdistributionsbywebaclid") (= a "cloudfront:listfunctions") (= a "cloudfront:listinvalidations") (= a "cloudfront:listkeygroups") (= a "cloudfront:listoriginaccesscontrols") (= a "cloudfront:listoriginrequestpolicies") (= a "cloudfront:listpublickeys") (= a "cloudfront:listrealtimelogconfigs") (= a "cloudfront:liststreamingdistributions") (= a "cloudhsm:describebackups") (= a "cloudhsm:describeclusters") (= a "cloudsearch:describeanalysisschemes") (= a "cloudsearch:describeavailabilityoptions") (= a "cloudsearch:describedomains") (= a "cloudsearch:describeexpressions") (= a "cloudsearch:describeindexfields") (= a "cloudsearch:describescalingparameters") (= a "cloudsearch:describeserviceaccesspolicies") (= a "cloudsearch:describesuggesters") (= a "cloudsearch:listdomainnames") (= a "cloudtrail:describetrails") (= a "cloudtrail:geteventselectors") (= a "cloudtrail:getinsightselectors") (= a "cloudtrail:gettrail") (= a "cloudtrail:gettrailstatus") (= a "cloudtrail:listpublickeys") (= a "cloudtrail:listtags") (= a "cloudtrail:listtrails") (= a "cloudtrail:lookupevents") (= a "cloudwatch:describealarmhistory") (= a "cloudwatch:describealarms") (= a "cloudwatch:describealarmsformetric") (= a "cloudwatch:describeanomalydetectors") (= a "cloudwatch:describeinsightrules") (= a "cloudwatch:getdashboard") (= a "cloudwatch:getinsightrulereport") (= a "cloudwatch:getmetricdata") (= a "cloudwatch:getmetricstatistics") (= a "cloudwatch:getmetricstream") (= a "cloudwatch:listdashboards") (= a "cloudwatch:listmanagedinsightrules") (= a "cloudwatch:listmetrics") (= a "cloudwatch:listmetricstreams") (= a "codeartifact:describedomain") (= a "codeartifact:describepackageversion") (= a "codeartifact:describerepository") (= a "codeartifact:getdomainpermissionspolicy") (= a "codeartifact:getrepositoryendpoint") (= a "codeartifact:getrepositorypermissionspolicy") (= a "codeartifact:listdomains") (= a "codeartifact:listpackages") (= a "codeartifact:listpackageversionassets") (= a "codeartifact:listpackageversions") (= a "codeartifact:listrepositories") (= a "codeartifact:listrepositoriesindomain") (= a "codebuild:batchgetbuildbatches") (= a "codebuild:batchgetbuilds") (= a "codebuild:batchgetprojects") (= a "codebuild:listbuildbatches") (= a "codebuild:listbuildbatchesforproject") (= a "codebuild:listbuilds") (= a "codebuild:listbuildsforproject") (= a "codebuild:listcuratedenvironmentimages") (= a "codebuild:listprojects") (= a "codebuild:listsourcecredentials") (= a "codecommit:batchgetrepositories") (= a "codecommit:getbranch") (= a "codecommit:getrepository") (= a "codecommit:getrepositorytriggers") (= a "codecommit:listbranches") (= a "codecommit:listrepositories") (= a "codedeploy:batchgetapplicationrevisions") (= a "codedeploy:batchgetapplications") (= a "codedeploy:batchgetdeploymentgroups") (= a "codedeploy:batchgetdeploymentinstances") (= a "codedeploy:batchgetdeployments") (= a "codedeploy:batchgetdeploymenttargets") (= a "codedeploy:batchgetonpremisesinstances") (= a "codedeploy:getapplication") (= a "codedeploy:getapplicationrevision") (= a "codedeploy:getdeployment") (= a "codedeploy:getdeploymentconfig") (= a "codedeploy:getdeploymentgroup") (= a "codedeploy:getdeploymentinstance") (= a "codedeploy:getdeploymenttarget") (= a "codedeploy:getonpremisesinstance") (= a "codedeploy:listapplicationrevisions") (= a "codedeploy:listapplications") (= a "codedeploy:listdeploymentconfigs") (= a "codedeploy:listdeploymentgroups") (= a "codedeploy:listdeploymentinstances") (= a "codedeploy:listdeployments") (= a "codedeploy:listdeploymenttargets") (= a "codedeploy:listgithubaccounttokennames") (= a "codedeploy:listonpremisesinstances") (= a "codepipeline:getjobdetails") (= a "codepipeline:getpipeline") (= a "codepipeline:getpipelineexecution") (= a "codepipeline:getpipelinestate") (= a "codepipeline:listactionexecutions") (= a "codepipeline:listactiontypes") (= a "codepipeline:listpipelineexecutions") (= a "codepipeline:listpipelines") (= a "codepipeline:listwebhooks") (= a "codestar:describeproject") (= a "codestar:listprojects") (= a "codestar:listresources") (= a "codestar:listteammembers") (= a "codestar:listuserprofiles") (= a "codestar-connections:getconnection") (= a "codestar-connections:gethost") (= a "codestar-connections:listconnections") (= a "codestar-connections:listhosts") (= a "cognito-identity:describeidentitypool") (= a "cognito-identity:getidentitypoolroles") (= a "cognito-identity:listidentities") (= a "cognito-identity:listidentitypools") (= a "cognito-idp:describeidentityprovider") (= a "cognito-idp:describeresourceserver") (= a "cognito-idp:describeriskconfiguration") (= a "cognito-idp:describeuserimportjob") (= a "cognito-idp:describeuserpool") (= a "cognito-idp:describeuserpoolclient") (= a "cognito-idp:describeuserpooldomain") (= a "cognito-idp:getgroup") (= a "cognito-idp:getuicustomization") (= a "cognito-idp:getuserpoolmfaconfig") (= a "cognito-idp:listgroups") (= a "cognito-idp:listidentityproviders") (= a "cognito-idp:listresourceservers") (= a "cognito-idp:listuserimportjobs") (= a "cognito-idp:listuserpoolclients") (= a "cognito-idp:listuserpools") (= a "cognito-sync:describedataset") (= a "cognito-sync:describeidentitypoolusage") (= a "cognito-sync:describeidentityusage") (= a "cognito-sync:getcognitoevents") (= a "cognito-sync:getidentitypoolconfiguration") (= a "cognito-sync:listdatasets") (= a "cognito-sync:listidentitypoolusage") (= a "comprehend:describedocumentclassificationjob") (= a "comprehend:describedocumentclassifier") (= a "comprehend:describedominantlanguagedetectionjob") (= a "comprehend:describeendpoint") (= a "comprehend:describeentitiesdetectionjob") (= a "comprehend:describeentityrecognizer") (= a "comprehend:describeeventsdetectionjob") (= a "comprehend:describeflywheel") (= a "comprehend:describeflywheeliteration") (= a "comprehend:describekeyphrasesdetectionjob") (= a "comprehend:describepiientitiesdetectionjob") (= a "comprehend:describesentimentdetectionjob") (= a "comprehend:describetargetedsentimentdetectionjob") (= a "comprehend:describetopicsdetectionjob") (= a "comprehend:listdocumentclassificationjobs") (= a "comprehend:listdocumentclassifiers") (= a "comprehend:listdominantlanguagedetectionjobs") (= a "comprehend:listendpoints") (= a "comprehend:listentitiesdetectionjobs") (= a "comprehend:listentityrecognizers") (= a "comprehend:listeventsdetectionjobs") (= a "comprehend:listflywheeliterationhistory") (= a "comprehend:listflywheels") (= a "comprehend:listkeyphrasesdetectionjobs") (= a "comprehend:listpiientitiesdetectionjobs") (= a "comprehend:listsentimentdetectionjobs") (= a "comprehend:listtargetedsentimentdetectionjobs") (= a "comprehend:listtopicsdetectionjobs") (= a "compute-optimizer:getautoscalinggrouprecommendations") (= a "compute-optimizer:getebsvolumerecommendations") (= a "compute-optimizer:getec2instancerecommendations") (= a "compute-optimizer:getec2recommendationprojectedmetrics") (= a "compute-optimizer:getecsservicerecommendations") (= a "compute-optimizer:getecsservicerecommendationprojectedmetrics") (= a "compute-optimizer:getenrollmentstatus") (= a "compute-optimizer:getrecommendationsummaries") (= a "config:batchgetaggregateresourceconfig") (= a "config:batchgetresourceconfig") (= a "config:describeaggregatecompliancebyconfigrules") (= a "config:describeaggregationauthorizations") (= a "config:describecompliancebyconfigrule") (= a "config:describecompliancebyresource") (= a "config:describeconfigruleevaluationstatus") (= a "config:describeconfigrules") (= a "config:describeconfigurationaggregators") (= a "config:describeconfigurationaggregatorsourcesstatus") (= a "config:describeconfigurationrecorders") (= a "config:describeconfigurationrecorderstatus") (= a "config:describeconformancepackcompliance") (= a "config:describeconformancepacks") (= a "config:describeconformancepackstatus") (= a "config:describedeliverychannels") (= a "config:describedeliverychannelstatus") (= a "config:describeorganizationconfigrules") (= a "config:describeorganizationconfigrulestatuses") (= a "config:describeorganizationconformancepacks") (= a "config:describeorganizationconformancepackstatuses") (= a "config:describependingaggregationrequests") (= a "config:describeremediationconfigurations") (= a "config:describeremediationexceptions") (= a "config:describeremediationexecutionstatus") (= a "config:describeretentionconfigurations") (= a "config:getaggregatecompliancedetailsbyconfigrule") (= a "config:getaggregateconfigrulecompliancesummary") (= a "config:getaggregatediscoveredresourcecounts") (= a "config:getaggregateresourceconfig") (= a "config:getcompliancedetailsbyconfigrule") (= a "config:getcompliancedetailsbyresource") (= a "config:getcompliancesummarybyconfigrule") (= a "config:getcompliancesummarybyresourcetype") (= a "config:getconformancepackcompliancedetails") (= a "config:getconformancepackcompliancesummary") (= a "config:getdiscoveredresourcecounts") (= a "config:getorganizationconfigruledetailedstatus") (= a "config:getorganizationconformancepackdetailedstatus") (= a "config:getresourceconfighistory") (= a "config:listaggregatediscoveredresources") (= a "config:listdiscoveredresources") (= a "config:listtagsforresource") (= a "connect:describecontact") (= a "connect:describephonenumber") (= a "connect:describequickconnect") (= a "connect:describeuser") (= a "connect:getcurrentmetricdata") (= a "connect:getmetricdata") (= a "connect:listcontactevaluations") (= a "connect:listevaluationforms") (= a "connect:listevaluationformversions") (= a "connect:listphonenumbersv2") (= a "connect:listquickconnects") (= a "connect:listroutingprofiles") (= a "connect:listsecurityprofiles") (= a "connect:listusers") (= a "connect:listviews") (= a "connect:listviewversions") (=... (= a "storagegateway:listtagsforresource") (= a "storagegateway:listtapes") (= a "storagegateway:listvolumeinitiators") (= a "storagegateway:listvolumerecoverypoints") (= a "storagegateway:listvolumes") (= a "swf:countclosedworkflowexecutions") (= a "swf:countopenworkflowexecutions") (= a "swf:countpendingactivitytasks") (= a "swf:countpendingdecisiontasks") (= a "swf:describeactivitytype") (= a "swf:describedomain") (= a "swf:describeworkflowexecution") (= a "swf:describeworkflowtype") (= a "swf:getworkflowexecutionhistory") (= a "swf:listactivitytypes") (= a "swf:listclosedworkflowexecutions") (= a "swf:listdomains") (= a "swf:listopenworkflowexecutions") (= a "swf:listworkflowtypes") (= a "synthetics:describecanaries") (= a "synthetics:describecanarieslastrun") (= a "synthetics:describeruntimeversions") (= a "synthetics:getcanary") (= a "synthetics:getcanaryruns") (= a "synthetics:getgroup") (= a "synthetics:listassociatedgroups") (= a "synthetics:listgroupresources") (= a "synthetics:listgroups") (= a "tiros:createquery") (= a "tiros:getqueryanswer") (= a "tiros:getqueryexplanation") (= a "transcribe:describelanguagemodel") (= a "transcribe:getcallanalyticscategory") (= a "transcribe:getcallanalyticsjob") (= a "transcribe:getmedicaltranscriptionjob") (= a "transcribe:getmedicalvocabulary") (= a "transcribe:gettranscriptionjob") (= a "transcribe:getvocabulary") (= a "transcribe:getvocabularyfilter") (= a "transcribe:listcallanalyticscategories") (= a "transcribe:listcallanalyticsjobs") (= a "transcribe:listlanguagemodels") (= a "transcribe:listmedicaltranscriptionjobs") (= a "transcribe:listmedicalvocabularies") (= a "transcribe:listtranscriptionjobs") (= a "transcribe:listvocabularies") (= a "transcribe:listvocabularyfilters") (= a "transfer:describeaccess") (= a "transfer:describeagreement") (= a "transfer:describeconnector") (= a "transfer:describeexecution") (= a "transfer:describeprofile") (= a "transfer:describeserver") (= a "transfer:describeuser") (= a "transfer:describeworkflow") (= a "transfer:listaccesses") (= a "transfer:listagreements") (= a "transfer:listconnectors") (= a "transfer:listexecutions") (= a "transfer:listhostkeys") (= a "transfer:listprofiles") (= a "transfer:listservers") (= a "transfer:listtagsforresource") (= a "transfer:listusers") (= a "transfer:listworkflows") (= a "transfer:sendworkflowstepstate") (= a "trustedadvisor:getorganizationrecommendation") (= a "trustedadvisor:getrecommendation") (= a "trustedadvisor:listchecks") (= a "trustedadvisor:listorganizationrecommendationaccounts") (= a "trustedadvisor:listorganizationrecommendationresources") (= a "trustedadvisor:listorganizationrecommendations") (= a "trustedadvisor:listrecommendationresources") (= a "trustedadvisor:listrecommendations") (= a "verifiedpermissions:getidentitysource") (= a "verifiedpermissions:getpolicy") (= a "verifiedpermissions:getpolicystore") (= a "verifiedpermissions:getpolicytemplate") (= a "verifiedpermissions:getschema") (= a "verifiedpermissions:listidentitysources") (= a "verifiedpermissions:listpolicies") (= a "verifiedpermissions:listpolicystores") (= a "verifiedpermissions:listpolicytemplates") (= a "vpc-lattice:getaccesslogsubscription") (= a "vpc-lattice:getauthpolicy") (= a "vpc-lattice:getlistener") (= a "vpc-lattice:getresourcepolicy") (= a "vpc-lattice:getrule") (= a "vpc-lattice:getservice") (= a "vpc-lattice:getservicenetwork") (= a "vpc-lattice:getservicenetworkserviceassociation") (= a "vpc-lattice:getservicenetworkvpcassociation") (= a "vpc-lattice:gettargetgroup") (= a "vpc-lattice:listaccesslogsubscriptions") (= a "vpc-lattice:listlisteners") (= a "vpc-lattice:listrules") (= a "vpc-lattice:listservicenetworks") (= a "vpc-lattice:listservicenetworkserviceassociations") (= a "vpc-lattice:listservicenetworkvpcassociations") (= a "vpc-lattice:listservices") (= a "vpc-lattice:listtargetgroups") (= a "vpc-lattice:listtargets") (= a "waf-regional:getbytematchset") (= a "waf-regional:getchangetokenstatus") (= a "waf-regional:getgeomatchset") (= a "waf-regional:getipset") (= a "waf-regional:getloggingconfiguration") (= a "waf-regional:getratebasedrule") (= a "waf-regional:getregexmatchset") (= a "waf-regional:getregexpatternset") (= a "waf-regional:getrule") (= a "waf-regional:getrulegroup") (= a "waf-regional:getsqlinjectionmatchset") (= a "waf-regional:getwebacl") (= a "waf-regional:getwebaclforresource") (= a "waf-regional:listactivatedrulesinrulegroup") (= a "waf-regional:listbytematchsets") (= a "waf-regional:listgeomatchsets") (= a "waf-regional:listipsets") (= a "waf-regional:listloggingconfigurations") (= a "waf-regional:listratebasedrules") (= a "waf-regional:listregexmatchsets") (= a "waf-regional:listregexpatternsets") (= a "waf-regional:listresourcesforwebacl") (= a "waf-regional:listrulegroups") (= a "waf-regional:listrules") (= a "waf-regional:listsqlinjectionmatchsets") (= a "waf-regional:listwebacls") (= a "waf:getbytematchset") (= a "waf:getchangetokenstatus") (= a "waf:getgeomatchset") (= a "waf:getipset") (= a "waf:getloggingconfiguration") (= a "waf:getratebasedrule") (= a "waf:getregexmatchset") (= a "waf:getregexpatternset") (= a "waf:getrule") (= a "waf:getrulegroup") (= a "waf:getsampledrequests") (= a "waf:getsizeconstraintset") (= a "waf:getsqlinjectionmatchset") (= a "waf:getwebacl") (= a "waf:getxssmatchset") (= a "waf:listactivatedrulesinrulegroup") (= a "waf:listbytematchsets") (= a "waf:listgeomatchsets") (= a "waf:listipsets") (= a "waf:listloggingconfigurations") (= a "waf:listratebasedrules") (= a "waf:listregexmatchsets") (= a "waf:listregexpatternsets") (= a "waf:listrulegroups") (= a "waf:listrules") (= a "waf:listsizeconstraintsets") (= a "waf:listsqlinjectionmatchsets") (= a "waf:listwebacls") (= a "waf:listxssmatchsets") (= a "wafv2:checkcapacity") (= a "wafv2:describemanagedrulegroup") (= a "wafv2:getipset") (= a "wafv2:getloggingconfiguration") (= a "wafv2:getpermissionpolicy") (= a "wafv2:getratebasedstatementmanagedkeys") (= a "wafv2:getregexpatternset") (= a "wafv2:getrulegroup") (= a "wafv2:getsampledrequests") (= a "wafv2:getwebacl") (= a "wafv2:getwebaclforresource") (= a "wafv2:listavailablemanagedrulegroups") (= a "wafv2:listipsets") (= a "wafv2:listloggingconfigurations") (= a "wafv2:listregexpatternsets") (= a "wafv2:listresourcesforwebacl") (= a "wafv2:listrulegroups") (= a "wafv2:listtagsforresource") (= a "wafv2:listwebacls") (= a "workdocs:checkalias") (= a "workdocs:describeavailabledirectories") (= a "workdocs:describeinstances") (= a "workmail:describegroup") (= a "workmail:describeorganization") (= a "workmail:describeresource") (= a "workmail:describeuser") (= a "workmail:listaliases") (= a "workmail:listgroupmembers") (= a "workmail:listgroups") (= a "workmail:listmailboxpermissions") (= a "workmail:listorganizations") (= a "workmail:listresourcedelegates") (= a "workmail:listresources") (= a "workmail:listusers") (= a "workspaces-web:getbrowsersettings") (= a "workspaces-web:getidentityprovider") (= a "workspaces-web:getnetworksettings") (= a "workspaces-web:getportal") (= a "workspaces-web:getportalserviceprovidermetadata") (= a "workspaces-web:gettruststorecertificate") (= a "workspaces-web:getusersettings") (= a "workspaces-web:listbrowsersettings") (= a "workspaces-web:listidentityproviders") (= a "workspaces-web:listnetworksettings") (= a "workspaces-web:listportals") (= a "workspaces-web:listtagsforresource") (= a "workspaces-web:listtruststorecertificates") (= a "workspaces-web:listtruststores") (= a "workspaces-web:listusersettings") (= a "workspaces:describeaccount") (= a "workspaces:describeaccountmodifications") (= a "workspaces:describeipgroups") (= a "workspaces:describetags") (= a "workspaces:describeworkspacebundles") (= a "workspaces:describeworkspacedirectories") (= a "workspaces:describeworkspaceimages") (= a "workspaces:describeworkspaces") (= a "workspaces:describeworkspacesconnectionstatus")) (str.in_re r (re.* (re.range "!" "~")))))) (let ((a!3 (str.substr (str.substr r 0 (+ (- 69) (str.len r))) 13 (+ (- 13) a!1))) (a!8 (str.substr (str.substr r 0 (+ (- 10) (str.len r))) 19 (+ (- 19) a!6))) (a!13 (str.substr (str.substr r 0 (+ (- 7) (str.len r))) 19 (+ (- 19) a!11))) (a!17 (str.in_re (str.substr r 0 (+ (- 12) (str.len r))) (re.++ a!16 (re.* (re.range "!" "~"))))) (a!20 (str.in_re (str.substr r 0 (+ (- 13) (str.len r))) (re.++ a!16 (re.* (re.range "!" "~"))))) (a!22 (re.++ (re.++ a!16 (re.* (re.range "!" "~"))) (str.to_re "/integrations/"))) (a!25 (str.in_re (str.substr r 0 (+ (- 7) (str.len r))) (re.++ a!16 (re.* (re.range "!" "~"))))) (a!28 (re.++ (re.++ a!16 (re.* (re.range "!" "~"))) (str.to_re "/routes/"))) (a!34 (str.substr (str.substr r 0 (+ (- 21) (str.len r))) 19 (+ (- 19) a!32))) (a!39 (str.substr (str.substr r 0 (+ (- 14) (str.len r))) 19 (+ (- 19) a!37))) (a!43 (str.in_re (str.substr r 0 (+ (- 12) (str.len r))) (re.++ a!42 (re.* (re.range "!" "~"))))) (a!45 (str.in_re (str.substr r 0 (+ (- 17) (str.len r))) (re.++ a!42 (re.* (re.range "!" "~"))))) (a!49 (str.substr (str.substr r 0 (+ (- 11) (str.len r))) 19 (+ (- 19) a!47))) (a!53 (str.in_re (str.substr r 0 (+ (- 12) (str.len r))) (re.++ a!52 (re.* (re.range "!" "~"))))) (a!54 (str.in_re (str.substr r 0 (+ (- 7) (str.len r))) (re.++ a!52 (re.* (re.range "!" "~"))))) (a!55 (re.++ (re.++ a!52 (re.* (re.range "!" "~"))) (str.to_re "/models/"))) (a!58 (str.in_re (str.substr r 0 (+ (- 10) (str.len r))) (re.++ a!52 (re.* (re.range "!" "~"))))) (a!60 (re.++ (re.++ a!52 (re.* (re.range "!" "~"))) (str.to_re "/resources/"))) (a!66 (str.substr (str.substr r 0 (+ (- 13) (str.len r))) 19 (+ (- 19) a!64))) (a!71 (re.++ (re.++ a!16 (re.* (re.range "!" "~"))) (str.to_re "/authorizers/"))) (a!72 (re.++ (re.++ a!16 (re.* (re.range "!" "~"))) (str.to_re "/deployments/"))) (a!74 (re.++ (re.++ a!16 (re.* (re.range "!" "~"))) (str.to_re "/models/"))) (a!76 (re.++ (re.++ a!16 (re.* (re.range "!" "~"))) (str.to_re "/stages/"))) (a!78 (re.++ (re.++ a!42 (re.* (re.range "!" "~"))) (str.to_re "/apimappings/"))) (a!79 (re.++ (re.++ a!42 (re.* (re.range "!" "~"))) (str.to_re "/basepathmappings/"))) (a!80 (re.++ (re.++ a!52 (re.* (re.range "!" "~"))) (str.to_re "/authorizers/"))) (a!81 (re.++ (re.++ a!52 (re.* (re.range "!" "~"))) (str.to_re "/deployments/"))) (a!84 (re.++ (re.++ a!52 (re.* (re.range "!" "~"))) (str.to_re "/stages/"))) (a!88 (re.union (re.++ a!86 (re.* (re.range "!" "~"))) (re.++ a!87 (re.* (re.range "!" "~")))))) (let ((a!5 (and (= a "iam:deleterole") (>= (str.len r) 69) (>= a!1 13) (= a!2 "arn:aws:iam::") (str.in_re a!3 (re.* (re.range "!" "~"))) a!4)) (a!10 (and (>= (str.len r) 10) (>= a!6 19) (= a!7 "arn:aws:apigateway:") (str.in_re a!8 (re.* (re.range "!" "~"))) a!9)) (a!15 (and (>= (str.len r) 7) (>= a!11 19) (= a!12 "arn:aws:apigateway:") (str.in_re a!13 (re.* (re.range "!" "~"))) a!14)) (a!23 (str.in_re (str.substr r 0 (+ (- 21) (str.len r))) (re.++ a!22 (re.* (re.range "!" "~"))))) (a!29 (str.in_re (str.substr r 0 (+ (- 15) (str.len r))) (re.++ a!28 (re.* (re.range "!" "~"))))) (a!36 (and (>= (str.len r) 21) (>= a!32 19) (= a!33 "arn:aws:apigateway:") (str.in_re a!34 (re.* (re.range "!" "~"))) a!35)) (a!41 (and (>= (str.len r) 14) (>= a!37 19) (= a!38 "arn:aws:apigateway:") (str.in_re a!39 (re.* (re.range "!" "~"))) a!40)) (a!51 (and (>= (str.len r) 11) (>= a!47 19) (= a!48 "arn:aws:apigateway:") (str.in_re a!49 (re.* (re.range "!" "~"))) a!50)) (a!56 (str.in_re (str.substr r 0 (+ (- 17) (str.len r))) (re.++ a!55 (re.* (re.range "!" "~"))))) (a!61 (re.++ (re.++ a!60 (re.* (re.range "!" "~"))) (str.to_re "/methods/"))) (a!68 (and (>= (str.len r) 13) (>= a!64 19) (= a!65 "arn:aws:apigateway:") (str.in_re a!66 (re.* (re.range "!" "~"))) a!67)) (a!70 (and (>= (str.len r) 11) (>= a!47 19) (= a!48 "arn:aws:apigateway:") (str.in_re a!49 (re.* (re.range "!" "~"))) a!69)) (a!73 (re.++ (re.++ a!22 (re.* (re.range "!" "~"))) (str.to_re "/integrationresponses/"))) (a!75 (re.++ (re.++ a!28 (re.* (re.range "!" "~"))) (str.to_re "/routeresponses/"))) (a!85 (re.++ (re.++ a!84 (re.* (re.range "!" "~"))) (str.to_re "/sdks/")))) (let ((a!62 (str.in_re (str.substr r 0 (+ (- 12) (str.len r))) (re.++ a!61 (re.* (re.range "!" "~"))))) (a!82 (re.++ (re.++ a!61 (re.* (re.range "!" "~"))) (str.to_re "/integration/responses/"))) (a!83 (re.++ (re.++ a!61 (re.* (re.range "!" "~"))) (str.to_re "/responses/"))) (a!89 (re.union (re.++ a!85 (re.* (re.range "!" "~"))) a!88))) (let ((a!90 (re.union (re.++ a!84 (re.* (re.range "!" "~"))) a!89))) (let ((a!91 (re.union (re.++ a!83 (re.* (re.range "!" "~"))) a!90))) (let ((a!92 (re.union (re.++ a!82 (re.* (re.range "!" "~"))) a!91))) (let ((a!93 (re.union (re.++ a!61 (re.* (re.range "!" "~"))) a!92))) (let ((a!94 (re.union (re.++ a!60 (re.* (re.range "!" "~"))) a!93))) (let ((a!95 (re.union (re.++ a!55 (re.* (re.range "!" "~"))) a!94))) (let ((a!96 (re.union (re.++ a!81 (re.* (re.range "!" "~"))) a!95))) (let ((a!97 (re.union (re.++ a!80 (re.* (re.range "!" "~"))) a!96))) (let ((a!98 (re.union (re.++ a!52 (re.* (re.range "!" "~"))) a!97))) (let ((a!99 (re.union (re.++ a!79 (re.* (re.range "!" "~"))) a!98))) (let ((a!100 (re.union (re.++ a!78 (re.* (re.range "!" "~"))) a!99))) (let ((a!101 (re.union (re.++ a!42 (re.* (re.range "!" "~"))) a!100))) (let ((a!102 (re.union (re.++ a!77 (re.* (re.range "!" "~"))) a!101))) (let ((a!103 (re.union (re.++ a!76 (re.* (re.range "!" "~"))) a!102))) (let ((a!104 (re.union (re.++ a!75 (re.* (re.range "!" "~"))) a!103))) (let ((a!105 (re.union (re.++ a!28 (re.* (re.range "!" "~"))) a!104))) (let ((a!106 (re.union (re.++ a!74 (re.* (re.range "!" "~"))) a!105))) (let ((a!107 (re.union (re.++ a!73 (re.* (re.range "!" "~"))) a!106))) (let ((a!108 (re.union (re.++ a!22 (re.* (re.range "!" "~"))) a!107))) (let ((a!109 (re.union (re.++ a!72 (re.* (re.range "!" "~"))) a!108))) (let ((a!110 (re.union (re.++ a!71 (re.* (re.range "!" "~"))) a!109))) (let ((a!111 (re.union (re.++ a!16 (re.* (re.range "!" "~"))) a!110))) (let ((a!112 (or a!10 a!15 (and (>= (str.len r) 12) a!17 a!18) (and (>= (str.len r) 12) a!17 a!19) (and (>= (str.len r) 13) a!20 a!21) (and (>= (str.len r) 21) a!23 a!24) (and (>= (str.len r) 7) a!25 a!26) (and (>= (str.len r) 7) a!25 a!27) (and (>= (str.len r) 15) a!29 a!30) (and (>= (str.len r) 7) a!25 a!31) a!36 a!41 (and (>= (str.len r) 12) a!43 a!44) (and (>= (str.len r) 17) a!45 a!46) a!51 (and (>= (str.len r) 12) a!53 a!18) (and (>= (str.len r) 12) a!53 a!19) (and (>= (str.len r) 7) a!54 a!26) (and (>= (str.len r) 17) a!56 a!57) (and (>= (str.len r) 10) a!58 a!59) (and (>= (str.len r) 12) a!62 a!63) (and (>= (str.len r) 7) a!54 a!31) a!68 a!70 (str.in_re r a!111)))) (or a!5 (and (= a "apigateway:get") a!112) a!113))))))))))))))))))))))))))))) (assert (str.prefixof "s3:" a)) (model-add r () String "") (model-add a () String "s3:listaccesspoints")