fstarlang-smtprofiling

Invocation

This skill is used when:

• Verifying F* (.fst) or interface (.fsti) files
• Debugging verification failures and proof performance
• Especially when proofs require high rlimits or fail unpredictably

Core Operations

Collect an .smt2 file for problematic proof

Wrap the part of the program to diagnose proof failures with

#push-options "--log_queries --z3refresh --query_stats --split_queries always"
let definition_to_be_debugged ...
#pop-options

Run F* on the file (with appropriate include paths)