#7800·z3

从 4.14.1 升级到 4.15.3 后,计算和内存均出现回退

作者: smoy创建于 2025年8月19日更新于 2026年8月16日
标签string

(declare-fun p () String) (declare-fun an () String) (declare-fun pa () String) (declare-fun r () String) (declare-fun a () String) (assert (= p "arn:AWS:iam::012345678901:role/RoleInQuestion")) (assert (let ((a!1 (re.++ (re.++ (str.to_re "arn:AWS:s3:::") (re.* (re.range "!" ""))) (str.to_re "cloudtrail"))) (a!2 (re.++ (re.++ (str.to_re "arn:AWS:s3:::") (re.* (re.range "!" ""))) (str.to_re "controltower"))) (a!4 (and (or (= a "s3:listallmybuckets") (= a "s3:listbucket") (= a "s3:listmultiregionaccesspoints")) (str.in_re r (re.* (re.range "!" ""))) (= pa "arn:AWS:iam::AWS:policy/job-function/ViewOnlyAccess"))) (a!5 (and (or (= a "s3:listaccessgrants") (= a "s3:listaccessgrantsinstances") (= a "s3:listaccesspoints") (= a "s3:listaccesspointsforobjectlambda") (= a "s3:listallmybuckets") (= a "s3:listbucket") (= a "s3:listcalleraccessgrants") (= a "s3:listjobs") (= a "s3:listmultiregionaccesspoints") (= a "s3:liststoragelensconfigurations") (= a "s3:liststoragelensgroups") (= a "s3:describejob") (= a "s3:getaccelerateconfiguration") (= a "s3:getaccessgrantsinstanceresourcepolicy") (= 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:getencryptionconfiguration") (= a "s3:getinventoryconfiguration") (= a "s3:getlifecycleconfiguration") (= a "s3:getmetricsconfiguration") (= a "s3:getmultiregionaccesspoint") (= a "s3:getmultiregionaccesspointpolicy") (= a "s3:getmultiregionaccesspointpolicystatus") (= a "s3:getobjectacl") (= a "s3:getobjecttagging") (= a "s3:getobjectversionacl") (= a "s3:getreplicationconfiguration") (= a "s3:getstoragelensconfiguration") (= a "s3:getstoragelensgroup") (str.prefixof "s3:getbucket" a)) (str.in_re r (re.* (re.range "!" ""))) (= pa "arn:AWS:iam::AWS:policy/SecurityAudit"))) (a!6 (and (= a "s3:getobject") …