Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | Merging complete. Everything looks good *crosses fingers* | 2016-06-06 | |
| | |||
* | Removed old test infrastructure files except for | 2014-05-28 | |
| | | | | | | | | | ./AbsHoudini/ ./doomed/ ./z3api/ ./test17/ because their conversion to lit incomplete. | ||
* | Fix lit test suite when running Boogie under a path that contains | 2014-05-27 | |
| | | | | spaces. | ||
* | Enabled "Extract loops benchmarks" lit tests. | 2014-05-07 | |
| | |||
* | 1. Fix for free ensures in inlined procedures. Becomes a skip instead of an ↵ | 2012-06-01 | |
| | | | | | | | assume. 2. Fix for deterministic loop extraction, and a new regression. 3. All regressions (including Dafny) except houdini pass, it is most likely related to the free ensures change. | ||
* | Fixed the regression for deterministicExtractLoops. | 2012-05-25 | |
| | |||
* | Merge | 2012-05-25 | |
|\ | |||
* | | Adding an option for deterministicExtractLoops, that uses an alternate way ↵ | 2012-05-25 | |
| | | | | | | | | | | | | to extract loops into procedures. Unsound for concurrency. Added a test in extractLoops directory. | ||
| * | updated test | 2012-05-24 | |
|/ | |||
* | UseLabels=false when stratified inline is on | 2012-04-29 | |
| | |||
* | eliminated class ErrorModel | 2012-04-28 | |
| | |||
* | Boogie: Eliminated the /bv option. Only native bitvectors are supported now. ↵ | 2011-10-27 | |
| | | | | The :forceBvZ3Native, :forceBvInt, and :bvint attributes were also eliminated. | ||
* | Support for irreducible graphs (with extractLoops) | 2011-08-24 | |
| | |||
* | Added tests for extractloops | 2010-09-04 | |