summaryrefslogtreecommitdiff
path: root/Source/VCGeneration/StratifiedVC.cs
Commit message (Expand)AuthorAge
* MergeGravatar qadeer2012-05-10
|\
* | some other cleanupsGravatar qadeer2012-05-10
| * Slightly better management of outermost Push-Pop and FlushAxiomsGravatar Unknown2012-05-02
|/
* z3 process is killed nowGravatar qadeer2012-05-01
* added counterexample generation based on labels back to stratified inliningGravatar qadeer2012-05-01
* log file fixGravatar qadeer2012-04-30
* clean up in stratified inliningGravatar qadeer2012-04-29
* eliminated class ErrorModelGravatar qadeer2012-04-28
* removed proccopybounding codeGravatar qadeer2012-04-28
* eliminated LazyInliningInfoGravatar qadeer2012-04-28
* removed lazy inliningGravatar qadeer2012-04-28
* Added test to stratified inlining.Gravatar Unknown2012-04-24
* various changes for using unsat cores in HoudiniGravatar qadeer2012-04-17
* Added functionality to "skip" procedures. Some cleanup.Gravatar akashlal2012-04-12
* added nonUniformUnfolding optionGravatar qadeer2012-04-03
* deleted the option UseUnsatCoreForInliningGravatar qadeer2012-04-02
* MergeGravatar qadeer2012-04-01
|\
* | commented out SuperAwesomeMethodGravatar qadeer2012-04-01
| * bug fix for previous refactoringGravatar Unknown2012-04-02
* | MergeGravatar qadeer2012-04-01
|\|
* | partial work on non-uniform loop unrollingGravatar qadeer2012-04-01
| * Refactored CheckAssumptions APIGravatar Unknown2012-04-02
|/
* 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
* bug fixes related to using ControlFlowFunction instead of labelsGravatar qadeer2012-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: output number of proof obligations (asserts) along with timing inform...Gravatar Rustan Leino2012-01-09
* 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
* Debugging output for stratified inlining. Emit attribute on Ensures whileGravatar Unknown2011-11-16
* 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
* fixed bug in data value generationGravatar qadeer2011-09-13