summaryrefslogtreecommitdiff
path: root/Source/DafnyServer/DafnyHelper.cs
Commit message (Collapse)AuthorAge
* Look for z3 in Binaries/z3/bin (but keep the vendored version for convenience)Gravatar Clément Pit--Claudel2015-08-27
| | | | | | 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).
* Cleanup a number of FIXMEs that I had left in the codeGravatar Clément Pit--Claudel2015-08-20
|
* Merge.Gravatar Clément Pit--Claudel2015-08-19
|\ | | | | | | | | Changes that were needed included preventing the InductionRewriter from iterating on a SplitQuantifier and using the new error reporting engine.
* | Refactor the error reporting codeGravatar Clément Pit--Claudel2015-08-18
| | | | | | | | | | The new error reporting system has a simpler interface, isn't tied to the resolver, and contains error source information.
| * Add a UniqueIdPrefix in the server and bump up the prover kill timeGravatar Clément Pit--Claudel2015-08-13
|/
* Split the server source into multiple filesGravatar Clément Pit--Claudel2015-07-31