summaryrefslogtreecommitdiff
Commit message (Expand)AuthorAge
...
* | | | Package Boogie programs for experimentalGravatar Benjamin Barenblat2016-04-01
* | | | Package Boogie library for experimentalGravatar Benjamin Barenblat2016-04-01
|/ / /
* | | Make DFSG-cleanGravatar Benjamin Barenblat2016-03-31
| | * modified floating point syntax and modified floating point constants to use b...Gravatar Checkmate502016-03-17
| * | Improve support for identifying unnecessary assumes.Gravatar Valentin Wüstholz2016-03-09
| * | Add support for weights on soft assumes.Gravatar Valentin Wüstholz2016-03-07
| * | Improve support for optimization and identifying unnecessary assumes.Gravatar Valentin Wüstholz2016-03-03
| | * Modified BigFloat and parser to accept correct SMT-LIB syntaxGravatar Checkmate502016-02-20
| * | Merge branch 'master' of https://github.com/boogie-org/boogieGravatar Rustan Leino2016-02-12
| |\ \
| | * \ Merge pull request #30 from qunyanm/type-parameter-bug-fixGravatar RustanLeino2016-02-12
| | |\ \
| * | | | Merge branch 'master' of https://github.com/boogie-org/boogieGravatar Rustan Leino2016-02-12
| |\| | |
| * | | | (Honestly, I don't know what I'm doing. I'm trying to revert these changes, b...Gravatar Rustan Leino2016-02-12
| | * | | added an exampleGravatar Shaz Qadeer2016-02-09
| | * | | another fixGravatar Shaz Qadeer2016-01-26
| | * | | improved some of the annotationsGravatar Shaz Qadeer2016-01-21
| | * | | some fixesGravatar Shaz Qadeer2016-01-19
| | | * | Bug fix in determining whether a type parameter is boundedGravatar qunyanm2016-01-19
| | |/ /
| | * | updated the example to implement the allocation of thread identifiers;Gravatar Shaz Qadeer2016-01-17
| | * | fixed a small problem in the precondition for FreeLinearGravatar Shaz Qadeer2016-01-10
| | * | added Free codeGravatar Shaz Qadeer2016-01-08
| | | * Added several test cases and some basic documentation for fp usageGravatar Checkmate502016-01-04
| | * | Minor changeGravatar Valentin Wüstholz2015-12-29
| | * | Fix issue with ids for assume-statements.Gravatar Valentin Wüstholz2015-12-28
| | * | Improve precision of abstract interpreter for modulo operations.Gravatar Valentin Wüstholz2015-12-28
| | * | Enable optimization for more prover queries.Gravatar Valentin Wüstholz2015-12-27
| | * | Merge branch 'master' of https://github.com/boogie-org/boogieGravatar qunyanm2015-12-15
| | |\ \
| | | * | Remove unused file.Gravatar Valentin Wüstholz2015-12-03
| | | * | Remove unused directory.Gravatar Valentin Wüstholz2015-12-03
| | | * | Remove workaround for older versions of Z3.Gravatar Valentin Wüstholz2015-12-02
| | | * | TravisCI build icon should only show build status for master branch, notGravatar Dan Liew2015-12-02
| | | * | Merge pull request #24 from boogie-org/dafny-bug-fixGravatar Dan Liew2015-12-02
| | | |\ \
| | | | * | Use the EndCurly token when creating the ReturnCmd for unifiedExitGravatar qunyanm2015-12-02
| | | |/ /
| | | * | Merge pull request #27 from boogie-org/update_recommended_Z3_versionGravatar Valentin Wüstholz2015-12-01
| | | |\ \
| | | | * | Update test output for Z3 4.4.1.Gravatar Valentin Wüstholz2015-12-01
| | | | * | Teach TravisCI to use Z3 4.4.1 from repositories that I'm currentlyGravatar Dan Liew2015-12-01
| | | |/ /
| | | | * Special fp types (such as infinity and NaN are now translated by boogieGravatar Checkmate502015-11-29
| | * | | Merge remote-tracking branch 'refs/remotes/origin/dafny-bug-fix'Gravatar qunyanm2015-11-25
| | |\ \ \
| | * \ \ \ Merge remote-tracking branch 'refs/remotes/origin/dafny-bug-fix'Gravatar qunyanm2015-11-25
| | |\ \ \ \ | | | |_|/ / | | |/| | |
| | | | * | Use the EndCurly token when creating the ReturnCmd for unifiedExitGravatar qunyanm2015-11-25
| | | |/ /
| | * | | Teach the TravisCI build to use the ``travis_retry`` command whenGravatar Dan Liew2015-11-21
| | * | | Add simplified may-unverified analysis and instrumentation.Gravatar Valentin Wüstholz2015-11-20
| | * | | Fix issue with partially-verified assertions.Gravatar Valentin Wüstholz2015-11-19
| | * | | Update test output after Nikolaj's enhancement in Z3.Gravatar Valentin Wüstholz2015-11-19
| | * | | Add a test.Gravatar Valentin Wüstholz2015-11-19
| | * | | Minor changesGravatar Valentin Wüstholz2015-11-19
| | * | | Improve experimental support for optimization (requires Z3 changeset 5948013b...Gravatar Valentin Wüstholz2015-11-18
| | * | | Add experimental support for optimization (requires Z3 build after changeset ...Gravatar Valentin Wüstholz2015-11-18
| | * | | Fix test output.Gravatar Valentin Wüstholz2015-11-17
| | * | | Fix issue #25.Gravatar Valentin Wüstholz2015-11-17
| | | * | Use EndCurly token for the ReturnCmd when creating unifiedExitGravatar qunyanm2015-11-16