Enum ProofStrength

• Defined in File analyzer.h

Enum Documentation

enum class tvm::sym::ProofStrength : int

The strength used for top-level condition proofs.

Do not use level beyond kDefault in internal recursive rewriting in sym analysis and only use it at top-level simplification to avoid speed issues.

Note

The higher, the more time consuming it can be.

Values:

enumerator kDefault

Default analysis followed by the optional Z3 fallback.

enumerator kSymbolicBound

Prove using symbolic bound analysis.