We present a tool that supports the understanding and validation of mechanisms that
numerically aggregate trust evidence { which may stem from heterogenous sources such as
geographical information, reputation, and threat levels. The tool is based on a policy com-
position language Peal [3] and can declare Peal expressions and intended analyses of such
expressions as input. The analyses include vacuity checking, sensitivity analysis of thresh-
olds, and policy re nement. We develop and implement two methods for generating veri -
cation conditions for analyses, using the SMT solver Z3 as backend. One method is explicit
and space intense, the other one is symbolic and so linear in the analysis expressions. We
experimentally investigate this space-time tradeo by observing the Z3 code generation and
its running time on randomly generated analyses and on a non-random benchmark modeling
majority voting. Our ndings suggest both methods have complementary value and may
scale up su ciently for the analysis of most realistic case studies.