| Commit message (Collapse) | Author | Age |
|
|
|
|
|
| |
Dafny now first looks for a z3 binary in z3/bin, and if it can't find one it
looks for one in Binaries/z3.exe (mostly for backwards-compatibility with
already set-up source installations).
|
| |
|
|\
| |
| |
| |
| | |
Changes that were needed included preventing the InductionRewriter from
iterating on a SplitQuantifier and using the new error reporting engine.
|
| |
| |
| |
| |
| | |
The new error reporting system has a simpler interface, isn't tied to the
resolver, and contains error source information.
|
|/ |
|
|
|