Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | 1. Fix for free ensures in inlined procedures. Becomes a skip instead of an ↵ | Unknown | 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. | Unknown | 2012-05-25 |
| | |||
* | Merge | Unknown | 2012-05-25 |
|\ | |||
* | | Adding an option for deterministicExtractLoops, that uses an alternate way ↵ | Unknown | 2012-05-25 |
| | | | | | | | | | | | | to extract loops into procedures. Unsound for concurrency. Added a test in extractLoops directory. | ||
| * | updated test | qadeer | 2012-05-24 |
|/ | |||
* | UseLabels=false when stratified inline is on | qadeer | 2012-04-29 |
| | |||
* | eliminated class ErrorModel | qadeer | 2012-04-28 |
| | |||
* | Boogie: Eliminated the /bv option. Only native bitvectors are supported now. ↵ | Rustan Leino | 2011-10-27 |
| | | | | The :forceBvZ3Native, :forceBvInt, and :bvint attributes were also eliminated. | ||
* | Support for irreducible graphs (with extractLoops) | Unknown | 2011-08-24 |
| | |||
* | Added tests for extractloops | akashlal | 2010-09-04 |