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)

fstar.exe Module.fst

The log messages will show the name of the .smt2 file logged for each proof obligation

Verify .smt2 file independently of F*

Find z3 in the path. It might be named z3-4.13.3, z3-4.15.1 etc., with a version number suffix

z3 queries-myquery.smt2

You can add z3 options like smt.qi.profile=true to see which quantifiers were firing
too much and what to do about it

Interpreting a quantifier profile

Some quantifiers in F*'s SMT encoding always fire a lot---this is
by design. Typically, quantifiers with unqualified names
(Box_bool_proj_0) or those with names in Prims, or FStar.
Pervasives will fire a lot.

Look for quantifiers in modules that are in files that you
authored that are firing a lot---these might signify that you
should write a pattern for those quantifiers, or control their
instantiation explicitly.

More information on SMT profiling

Find the directory PoP-in-FStar on the local machine, or locate it here:
https://github.com/FStarLang/PoP-in-FStar

The section under_the_hood/uth_smt.rst contains information about F*'s SMT
encoding and how to profile.