summaryrefslogtreecommitdiff
path: root/Source/Provers/Z3/Prover.ssc
Commit message (Expand)AuthorAge
* Boogie: Added stratified inlining. It is enabled using the flag /stratifiedIn...Gravatar akashlal2010-07-07
* Boogie:Gravatar rustanleino2010-06-22
* Added another option for lazy inlining based on macro expansion. This option...Gravatar qadeer2010-05-03
* 1. Fixed lazy inlining implementation so that inlined procedures use live var...Gravatar qadeer2010-04-30
* 1. Fixed an off-by-one error in parsing array partitions in Z3 modelsGravatar qadeer2010-04-19
* First cut of lazy inlining. The option can be turned on by the flag /lazyInl...Gravatar qadeer2010-04-17
* Revert the matching depth limit change from previous checkin: would break VCC.Gravatar MichalMoskal2009-12-10
* Z3 parameters to help it bail out of fruitless searches fasterGravatar mkawa2009-12-05
* Changed how Boogie looks for Z3: first look in the directory where Boogie is...Gravatar rustanleino2009-10-14
* Handle new Z3 'Memout' message.Gravatar stobies2009-09-30
* Added /z3multipleErrors flag for generation of multiple counterexamples per a...Gravatar mkawa2009-09-23
* Use callback mechanism to report prover warnings; do not just write them to s...Gravatar stobies2009-09-07
* Initial set of files.Gravatar mikebarnett2009-07-15
generated by cgit v1.2.3 (git 2.39.1) at 2025-01-24 01:02:43 +0000