summaryrefslogtreecommitdiff
path: root/Source/Provers
Commit message (Expand)AuthorAge
* mergeGravatar Pantazis Deligiannis2013-07-19
|\
* | refactoring and fixes in the SMTLIB2 parserGravatar Pantazis Deligiannis2013-07-19
| * Revamp of staged Houdini, and completion of parallel support.Gravatar allydonaldson2013-07-18
* | fix: can now setup CVC4 logic properly, default is ALL_SUPPORTED, other logic...Gravatar Pantazis Deligiannis2013-07-15
* | fix for SetTimeOut in ProverInterface to work only under Z3 parserGravatar Pantazis Deligiannis2013-07-15
* | small fixGravatar Pantazis Deligiannis2013-07-15
* | MergeGravatar Pantazis Deligiannis2013-07-15
|\ \ | |/ |/|
| * temp fix until CVC4 bug is fixed (using QF_ALL_SUPPORTED instead of ALL_SUPPO...Gravatar Pantazis Deligiannis2013-07-15
| * code cleanup and refactoringGravatar Pantazis Deligiannis2013-07-11
| * code cleanup & refactoringGravatar Pantazis Deligiannis2013-07-11
* | Worked on the parallelization.Gravatar wuestholz2013-07-10
| * the cvc4 parser can now parse nested array expressionsGravatar Pantazis Deligiannis2013-07-10
| * fixed a bug where a formula was being send to CVC4 although it shouldn't norm...Gravatar Pantazis Deligiannis2013-07-10
| * added specific command line options to enable the SMTLIB2 output model parser...Gravatar Pantazis Deligiannis2013-07-09
| * some clean upGravatar Pantazis Deligiannis2013-07-09
* | Worked on the parallelization.Gravatar wuestholz2013-07-08
| * allows (reset) to be send only to the Z3 proverGravatar Pantazis Deligiannis2013-07-09
* | Worked on the parallelization.Gravatar wuestholz2013-07-08
| * mergeGravatar Pantazis Deligiannis2013-07-06
| |\ | |/ |/|
* | Worked on the parallelization.Gravatar wuestholz2013-07-05
* | Worked on the parallelization.Gravatar wuestholz2013-07-02
* | Worked on the parallelization.Gravatar wuestholz2013-07-01
* | 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 the CVC4 SMTLIB array parsing to work under the latest CVC4 model repre...Gravatar pantazis2013-06-13
| | * merged more CVC4 and Z3 SMTLIB2 parsing methods ... results into a more compa...Gravatar pantazis2013-06-13
| | * Z3 new parser takes now a new option for pp-bv-literalsGravatar pantazis2013-06-12
| | * naive SMTLIB2 ParserGravatar pantazis2013-06-12
| | * CVC4 ParserGravatar pantazis2013-06-12
| | * cvc4 command line option & cvc4.cs in ProversGravatar pantazis2013-06-12
| |/ |/|
* | 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