summaryrefslogtreecommitdiff
path: root/Source/VCGeneration
Commit message (Expand)AuthorAge
* bug fixGravatar qadeer2012-02-29
* verbose mode for stratified inlining.Gravatar Unknown2012-02-29
* Cleaned up code by getting rid of ApiProverInterface.Gravatar Unknown2012-02-29
* MergeGravatar qadeer2012-02-28
|\
* | fix to keep old behavior of OnModel in SIGravatar qadeer2012-02-28
| * Introduce ApiProverInterface.CheckOutcomeCore() for stratified inlining; simp...Gravatar Michal Moskal2012-02-28
|/
* fixed up SI to work with new error trace generationGravatar qadeer2012-02-28
* further fixesGravatar qadeer2012-02-28
* various cleanup regarding /doNotUseLabelsGravatar qadeer2012-02-28
* one more fixGravatar qadeer2012-02-27
* fixing stratified inlining to deal with new path infoGravatar qadeer2012-02-27
* various fixes related to new error tracesGravatar qadeer2012-02-27
* further fixes related to using uninterpreted function for error tracesGravatar qadeer2012-02-25
* bug fixes related to using ControlFlowFunction instead of labelsGravatar qadeer2012-02-23
* using model instead of labelsGravatar Unknown2012-02-23
* verbose modeGravatar akashlal2012-02-19
* Print procs that reached the recursion bound.Gravatar Unknown2012-02-07
* Use DateTime.UtcNow instead of DateTime.NowGravatar stobies2012-01-11
* Boogie: fixed proof-obligation countingGravatar Rustan Leino2012-01-09
* Boogie: output number of proof obligations (asserts) along with timing inform...Gravatar Rustan Leino2012-01-09
* fixed problems with datatypesGravatar qadeer2011-12-29
* Make set iteration order deterministicGravatar Michal Moskal2011-12-07
* Boogie: Fixed a crash due to old expressions in lambda expressions that were ...Gravatar wuestholz2011-12-02
* Remove invariant that was just wrongGravatar Michal Moskal2011-11-28
* Added option of turning off model generation in SI. Can be very expensive som...Gravatar akashlal2011-11-26
* minor bug fix in SIGravatar akashlal2011-11-24
* minor changes to summary computationGravatar akashlal2011-11-24
* fixes to summary computationGravatar Unknown2011-11-22
* Added lazy summary computation to stratified inlining (not finished yet)Gravatar akashlal2011-11-20
* Dafny: fixed bad Code ContractsGravatar Rustan Leino2011-11-16
* refactoring houdini so that it creates only a single instance of z3Gravatar qadeer2011-11-16
* Eliminated unused argument in the constructor for CheckerGravatar qadeer2011-11-16
* MergeGravatar akashlal2011-11-16
|\
| * Debugging output for stratified inlining. Emit attribute on Ensures whileGravatar Unknown2011-11-16
* | Boogie (and Dafny, with effects also on SscBoogie): I refactored CommandLine...Gravatar Rustan Leino2011-11-15
|/
* MergeGravatar qadeer2011-11-07
|\
* | change in model parsing with datatype valuesGravatar qadeer2011-11-07
* | Boogie: Get rid of {:inline} attributes on axiomsGravatar Michal Moskal2011-10-27
* | Boogie: Get rid of {:ignore} feature on axiomsGravatar Michal Moskal2011-10-27
* | Boogie: internal clean-up, removed BvHandling type, everything now behaves as...Gravatar Rustan Leino2011-10-27
* | Boogie: Eliminated the /bv option. Only native bitvectors are supported now. ...Gravatar Rustan Leino2011-10-27
| * various refactoringsGravatar qadeer2011-10-27
|/
* Added a push+pop+unsat-core interface to SMTLib (for stratified inlining only)Gravatar Unknown2011-10-19
* revised implementation of proc copy boundingGravatar qadeer2011-10-16
* Bug fix to stratified inlining error trace valuesGravatar Unknown2011-09-28
* Name the constant used in @MV_state function applications - otherwise we get ...Gravatar Michal Moskal2011-09-26
* fixed bug in data value generationGravatar qadeer2011-09-13
* Added some extra functionality to Model code for corralGravatar Unknown2011-09-13
* fixes to model value generation for stratified inliningGravatar qadeer2011-09-12
* further fixesGravatar qadeer2011-09-08