summaryrefslogtreecommitdiff
path: root/Source/Provers
Commit message (Expand)AuthorAge
* fixed bad mergeGravatar Ken McMillan2013-06-15
* Merge fixes for dualityGravatar Ken McMillan2013-06-14
|\
| * Fixes for duality under corralGravatar Ken McMillan2013-06-14
* | Fixed an issue in the prover interface.Gravatar wuestholz2013-06-07
* | Changed the prover interface to report traces for time outs and out of memory.Gravatar wuestholz2013-05-30
* | Minor change to prevent prover errors during trace extractionGravatar wuestholz2013-05-29
|/
* Adding background model to fixedpoint counterexamples and small code contract...Gravatar Ken McMillan2013-05-29
* Getting fixed point backend to work with Corral.Gravatar Ken McMillan2013-05-29
* Working on fixedpoint backendGravatar Ken McMillan2013-05-20
* Adding fixedpoint engine backendGravatar Ken McMillan2013-05-07
* added support for linear sets without useArrayTheory (but there is some incom...Gravatar Unknown2013-03-07
* fixed datatype bug reported by ChrisGravatar Unknown2013-03-05
* Parse integers returned by Z3 into BigNumGravatar akashlal2013-01-29
* Use the new ProverInterface's Evaluate method in stratified inlinigGravatar Unknown2013-01-03
* bug fixGravatar Unknown2012-12-28
* extended Evaluate to handle more typesGravatar Unknown2012-12-28
* Added expression evaluation APIGravatar Unknown2012-12-27
* Bug fix for ExplainHoudini. Made it robust under timeouts.Gravatar Unknown2012-12-20
* Incorporated contribution 3667, which fixes bug in /z3exe flag (http://boogie...Gravatar Rustan Leino2012-11-20
* Fix for parsing error in MAXSAT computation in ProverInterface::CheckAssumpti...Gravatar Unknown2012-10-08
* bunch of refactoringsGravatar Unknown2012-10-03
* Boogie: added type 'real' with overloaded arithmetic operations plus real div...Gravatar boehmes2012-09-27
* Removed AIFramework from Boogie -- use native trivial or native interval-base...Gravatar boehmes2012-09-27
* Removed abandoned Isabelle prover backendGravatar boehmes2012-09-27
* Implement support for alternative SMT solvers -- CVC3 and CVC4Gravatar Peter Collingbourne2012-09-06
* Made error trace generation (without labels) more general for stratifiedGravatar Unknown2012-07-04
* Trying to merge with recent changes, failing.Gravatar Ken McMillan2012-06-05
|\
| * Some changes to support expanded use of z3api.Gravatar Ken McMillan2012-06-05
* | moved class Macro to AbsyGravatar qadeer2012-06-04
* | Z3: do not assert that the ProgramFiles environment variable is setGravatar Peter Collingbourne2012-05-02
* | Get Boogie and GPUVerify to compile and run with MonoGravatar Peter Collingbourne2012-05-02
* | clean up in stratified inliningGravatar qadeer2012-04-29
* | eliminated class ErrorModelGravatar qadeer2012-04-28
* | removed proccopybounding codeGravatar qadeer2012-04-28
* | removed lazy inliningGravatar qadeer2012-04-28
* | 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