| Commit message (Collapse) | Author | Age |
|---|
| |
|
|
|
| |
it. Don't use pretty warning signs since we can't diff them correctly in the
test output from the test run.
|
| | |
|
| |
|
|
|
|
| |
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).
|
| | |
|
| |
|
|
|
| |
This removes the need for special treatment of test input (/trace includes
timings in the output, which are not suitable for tests. /tracePO does not)
|
| | |
|
| |\
| |
| |
| |
| | |
Changes that were needed included preventing the InductionRewriter from
iterating on a SplitQuantifier and using the new error reporting engine.
|
| | |
| |
| |
| |
| |
| | |
z3 doesn't support byte-order marks; thus using the default UTF8Encoding object
(to allow printing nice warning signs) causes issues, as it sends a BOM before
anything else.
|
| | |
| |
| |
| |
| | |
This is useful because trigger-related messages can contain quite a bit of
information, especially if they include info about multiple split quantifiers.
|
| |/ |
|
| |
|
qunyanm
Clément Pit--Claudel