Timeout Control (--verify-timeout-ms)

Set a wall-clock timeout for Viper/Silicon verification.

Syntax

sector9 --verify --verify-timeout-ms <milliseconds> file.sr9

The timeout is specified in milliseconds. A value of 0 disables the timeout (equivalent to not specifying the flag).

Examples

# 30 second timeout
sector9 --verify --verify-timeout-ms 30000 file.sr9

# 2 minute timeout
sector9 --verify --verify-timeout-ms 120000 file.sr9

# 5 minute timeout (recommended for CI)
sector9 --verify --verify-timeout-ms 300000 file.sr9

# No timeout
sector9 --verify --verify-timeout-ms 0 file.sr9

Behavior

When the timeout is exceeded:

1. The verifier prints an error message to stderr:

   [viper] verification timed out after 30000 ms

2. The process exits with code 124 (standard Unix timeout convention)

3. The entire solver tree (Silicon and Z3) is terminated cleanly

The timeout measures wall-clock time, not CPU time. It covers the full verification phase including SMT solving.

Exit Codes

Code	Meaning
0	Verification succeeded
1	Verification failed
2	Invalid arguments
124	Timeout exceeded

When to Adjust Timeout

Increase timeout for:

• Programs with many methods and extensive contracts
• Heavy use of quantifiers (forall, exists)
• Complex nested quantifier patterns
• CI/CD pipelines where reliability matters more than speed

Decrease timeout for:

• Development iteration (consider using --check instead)
• Identifying slow methods quickly
• Failing fast while you identify which files or methods need proof simplification

Recommended Values

Scenario	Timeout	Notes
Simple contracts	10-30 seconds	Few quantifiers, basic verification
Moderate complexity	30-60 seconds	Some quantifiers, multiple methods
Quantifier-heavy	2-5 minutes	Nested forall/exists patterns
CI pipelines	5 minutes	Balance reliability and build time

Combining with Other Flags

With parallelization

Using --cores can reduce verification time significantly:

sector9 --verify --cores 4 --verify-timeout-ms 60000 file.sr9

More cores generally means you can use shorter timeouts for the same programs.

With JSON output

For CI integration, combine timeout with structured output:

sector9 --verify --json --verify-timeout-ms 300000 file.sr9

The JSON output includes the timeout status when verification times out.

With counterexamples

When debugging slow verification, reduce timeout and enable counterexamples:

sector9 --verify --counterexample --verify-timeout-ms 10000 file.sr9

Use this only after the Viper server is available for counterexample extraction. Timeouts can still prevent models from being produced.

Troubleshooting Timeouts

If verification consistently times out:

1. Simplify quantifiers - Complex forall/exists patterns are expensive
2. Add explicit triggers - Use forallWith to guide solver instantiation
3. Break large methods - Split into smaller, independently verifiable helpers
4. Check for unbounded quantification - Ensure quantifiers are bounded (e.g., i < n ==> ...)
5. Use --cores - Parallelize verification across multiple methods
6. Run --check first - Remove frontend errors before spending timeout budget on Silicon

Implementation Notes

The timeout is enforced at the process level, not within the Silicon solver. When a timeout occurs:

• Silicon is spawned in its own process group using setsid
• On timeout, SIGTERM is sent first for graceful shutdown
• After 1 second, SIGKILL forces termination if needed
• This ensures Z3 child processes are also terminated

Summary

• --verify-timeout-ms <ms> sets wall-clock verification timeout
• Value of 0 disables timeout
• Exit code 124 indicates timeout
• Use --verify-timeout-ms 0 when you explicitly want no timeout
• Combine with --cores for faster verification
• Use shorter timeouts with --counterexample for debugging