Observe both compute and memory regression when upgrade to 4.15.3 from 4.14.1
Author: smoyCreated Aug 19, 2025Updated Aug 16, 2026
Labelsstring
SMT in question
(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")
(str.prefixof "arn:aws:s3:::public.acmecorp.com/" r)
(str.in_re p (re.* (re.range "!" "~")))
(= pa "arn:aws:s3:::public.acmecorp.com"))))
(let ((a!3 (re.union (re.++ a!1 (re.* (re.range "!" "~")))
(re.++ a!2 (re.* (re.range "!" "~"))))))
(let ((a!7 (or (and (or (= a "s3:getobject") (= a "s3:getobjecttagging"))
(str.in_re r a!3)
(= pa
"arn:aws:iam::012345678901:inline-policy/role/RoleInQuestion/PolicyInQuestion"))
a!4
a!5
a!6)))
(and (= an "012345678901") a!7)))))
(assert true)
(assert (or (= r "arn:aws:s3:::public.acmecorp.com")
(str.prefixof "arn:aws:s3:::public.acmecorp.com/" r)))
(check-sat)when we run z3 encoding=ascii -file regression008.smt -st -memory:128 on 4.14.1, we get the following:
sat
(:added-eqs 70590
:arith-eq-adapter 3308
:arith-bound-propagations-lp 390
:arith-conflicts 11
:arith-diseq 548
:arith-fixed-eqs 3192
:arith-lower 3023
:arith-make-feasible 1586
:arith-max-columns 2242
:arith-max-rows 2051
:arith-offset-eqs 18
:arith-upper 6487
:binary-propagations 5812
:conflicts 188
:decisions 4585
:del-clause 210030
:final-checks 62
:interface-eqs 2
:max-memory 34.91
:memory 18.41
:minimized-lits 58
:mk-bool-var 118082
:mk-clause 217022
:mk-clause-binary 1258
:num-allocs 282007734
:num-checks 2
:propagations 90280
:restarts 1
:rlimit-count 519942
:seq-add-axiom 7538
:seq-branch 36
:seq-char-ackerman 3
:seq-char2bit 1381
:seq-fixed-length 23
:seq-length-coherence 2
:seq-num-reductions 12370
:solve-eqs-elim-vars 2
:solve-eqs-steps 2
:time 0.24
:total-time 0.25)whereas when we run it on 4.15.3, we observe both compute takes longer and max-memory being larger
sat
(:added-eqs 81809
:arith-eq-adapter 9880
:arith-bound-propagations-lp 363
:arith-conflicts 23
:arith-diseq 1361
:arith-fixed-eqs 12594
:arith-lower 9570
:arith-make-feasible 2166
:arith-max-columns 4116
:arith-max-rows 2827
:arith-offset-eqs 3053
:arith-upper 11458
:binary-propagations 13029
:conflicts 269
:decisions 11937
:del-clause 107157
:final-checks 430
:interface-eqs 10
:max-memory 53.17
:memory 18.52
:minimized-lits 151
:mk-bool-var 84491
:mk-clause 116314
:mk-clause-binary 3217
:num-allocs 1387860201
:num-checks 2
:propagations 68502
:restarts 1
:rlimit-count 699063
:seq-add-axiom 8753
:seq-branch 390
:seq-char2bit 625
:seq-fixed-length 28
:seq-length-coherence 11
:seq-num-reductions 6692
:solve-eqs-elim-vars 2
:solve-eqs-steps 2
:time 0.81
:total-time 0.81)We appreciate any insight because upgrade to the later version will cost more in both cpu time and memory usage.
Thanks.
we run this on macbook pro (m2 pro)
Source: Z3Prover/z3