search

dafny-lang / dafny

Dafny is a verification-aware programming language
https://dafny.org
Other
2.92k stars 262 forks source link

Investigate Z3 arithmetic mode configuration #3501

Closed atomb closed 11 months ago

atomb commented 1 year ago

Summary

We may want to change the default arithmetic mode used with Z3, or provide a means for users to choose it.

Background and Motivation

Historically, Dafny has specified the Z3 option smt.arith.solver=2, which differs from the default. This typically results in fewer proof failures with Z3 4.8.5. With 4.12.1, it still seems like it's probably the setting least likely to lead to proof failures but there are cases that only succeed with smt.arith.solver=6 (the default).

Proposed Feature

We should more thoroughly investigate the performance and completeness of each mode with recent Z3 versions and real-world Dafny code. After doing so, we might change the default or we might provide a way to configure it in a less cryptic way for specific proofs.

Alternatives

No response

atomb commented 11 months ago

This will be supported when #4841 is merged.