summaryrefslogtreecommitdiff
path: root/Source/Provers
Commit message (Expand)AuthorAge
* various changes for using unsat cores in HoudiniGravatar qadeer2012-04-17
* small fixGravatar qadeer2012-04-04
* added nonUniformUnfolding optionGravatar qadeer2012-04-03
* deleted the option UseUnsatCoreForInliningGravatar qadeer2012-04-02
* MergeGravatar 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
|/
* more type checking for datatypesGravatar qadeer2012-03-18
* bug fixGravatar qadeer2012-02-29
* MergeGravatar qadeer2012-02-29
|\
* | small changes to z3api to make it compile after the z3 project was ripped outGravatar qadeer2012-02-29
| * Cleaned up code by getting rid of ApiProverInterface.Gravatar Unknown2012-02-29
|/
* Simplification to previous checkinGravatar Michal Moskal2012-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
* 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
* MergeGravatar qadeer2012-02-23
|\
* | using model instead of labelsGravatar Unknown2012-02-23
| * added floating point keywords to reserved SMTwords listGravatar qadeer2012-02-20
|/
* minor fix in tracingGravatar qadeer2012-02-14
* minor bug in printing z3 path when running with /traceGravatar qadeer2012-02-09
* houdini will not request models nowGravatar qadeer2012-02-08
* 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
* made delegate a datatypeGravatar qadeer2011-12-30
* fixed problems with datatypesGravatar qadeer2011-12-29
* Added option of turning off model generation in SI. Can be very expensive som...Gravatar akashlal2011-11-26
* Boogie (and Dafny, with effects also on SscBoogie): I refactored CommandLine...Gravatar Rustan Leino2011-11-15
* Produce unsat cores only when enabled (in stratified inlining)Gravatar Unknown2011-11-11
* Fixed the generation of names for datatype functions to use the API forGravatar Mike Barnett2011-10-31
* Boogie: Updated the error message for old versions of Z3.Gravatar wuestholz2011-10-28
* Boogie: Get rid of {:ignore} feature on axiomsGravatar Michal Moskal2011-10-27
* Boogie: Present a nice error message when Z3 of lesser version than 3.2 is foundGravatar Michal Moskal2011-10-27
* MergeGravatar Michal Moskal2011-10-27
|\
* | Restart prover after out-of-memory error; honour -restartProver optionGravatar 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
|/
* Sync timeout messages with Z3 prover interfaceGravatar Michal Moskal2011-10-21
* Don't pass /T: option to Z3 - it kills Z3 prematurely when there are multiple...Gravatar Michal Moskal2011-10-21
* Improve logging when -proverOpt:VERBOSITY=1 or 2 is specifiedGravatar Michal Moskal2011-10-21
* Added a push+pop+unsat-core interface to SMTLib (for stratified inlining only)Gravatar Unknown2011-10-19
* added membership testsGravatar qadeer2011-10-05
* implementing datatypesGravatar qadeer2011-10-05
* check in support for generalized array theoryGravatar Unknown2011-09-06
* Fix printing of (Array ...) types with /useArrayTheoryGravatar Michal Moskal2011-09-06
* Support multi-dimensional arrays in SMTLib2 backend (using Z3 extension though)Gravatar Michal Moskal2011-09-06