# Unbounded-proof overlay: exclude the three expected-fail families (32 PCRs each) so the remaining
# assertions form a mutually inductive set. Run: bitlevel-compile project_prove.bl &&
# bitlevel-analyze .bitlevel_cache --prove --results-dir out_prove/ --timeout 30m --workers 3
exclude -asserts *.ast_pcr_clear_zeroes_entry
exclude -asserts *.ast_pcr_lock_blocks_clear
exclude -asserts *.ast_pcr_lock_sticky_across_warm_reset
