summaryrefslogtreecommitdiff
path: root/Source/VCGeneration/Wlp.cs
Commit message (Expand)AuthorAge
* 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
* Minor changeGravatar Valentin Wüstholz2015-12-29
* Add experimental support for optimization (requires Z3 build after changeset ...Gravatar Valentin Wüstholz2015-11-18
* Add support for identifying unnecessary assumes.Gravatar Valentin Wüstholz2015-11-16
* Normalise line endings using a .gitattributes file. UnfortunatelyGravatar Dan Liew2015-06-28
* Add some experimental support for diagnosing timeouts.Gravatar Valentin Wüstholz2015-05-18
* Minor change to the encoding of partially verified assertions as VCGravatar wuestholz2015-01-30
* Worked on the verification result caching (use native support for partially v...Gravatar wuestholz2015-01-16
* Added a test and a todo.Gravatar wuestholz2015-01-02
* Worked on more native support for partially-verified assertions.Gravatar wuestholz2014-12-28
* Cleanup: removed unused codeGravatar akashlal2014-09-29
* Bug fix in stratified inlining (triggered by {:inline} functions)Gravatar akashlal2013-10-21
* fixed the problem with codexprsGravatar qadeer2013-09-07
* When a codeexpr is used at the top-level in an assume statement, we use the a...Gravatar qadeer2013-09-04
* More refactoring towards replacing PureCollections.Sequence with ListGravatar Ally Donaldson2013-07-22
* Refactored labsl2absy so that it is a Dictionary<int, Absy> instead of a plai...Gravatar Ally Donaldson2013-07-22
* Removed old comments about "BASEMOVE" and other constructor calls, where the ...Gravatar Unknown2013-01-07
* various cleanup regarding /doNotUseLabelsGravatar qadeer2012-02-28
* bug fixes related to using ControlFlowFunction instead of labelsGravatar qadeer2012-02-23
* using model instead of labelsGravatar Unknown2012-02-23
* Boogie: output number of proof obligations (asserts) along with timing inform...Gravatar Rustan Leino2012-01-09
* Added lazy summary computation to stratified inlining (not finished yet)Gravatar akashlal2011-11-20
* LetVC can get null label2absy from lazy inlining. So, I weakened the precond...Gravatar qadeer2011-05-03
* modified letvc generation so that the use of control flow function and labels...Gravatar qadeer2011-04-15
* added reachability information to the VC and used that to support arbitrary a...Gravatar Unknown2011-04-14
* Boogie:Gravatar rustanleino2010-09-23
* Boogie: Added boolean code expressions (sans well-formedness checks on the in...Gravatar rustanleino2010-08-10
* Boogie: VCGeneration port part 1/3: Replacing old source files with ported ve...Gravatar tabarbe2010-07-28
* Boogie\VCGeneration: Renaming sources in preparation for my addition of the p...Gravatar tabarbe2010-07-28
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-16 06:10:50 +0000