summaryrefslogtreecommitdiff
path: root/Source/Provers
Commit message (Expand)AuthorAge
...
* added the QED build configurationGravatar qadeer2013-12-02
* do monomorphic checkingGravatar qadeer2013-11-22
* Fixedpoint VC catch up with recent changesGravatar Ken McMillan2013-11-11
* Merge duality changes to mainlineGravatar Ken McMillan2013-11-09
|\
| * handling timeouts for fixedpoint enginesGravatar Ken McMillan2013-11-09
* | ProverInterface: model isn't available on timeoutGravatar akashlal2013-11-02
* | small refactoringGravatar Pantazis Deligiannis2013-10-02
* | changes to support a configured errorLimitGravatar Pantazis Deligiannis2013-09-30
* | MergeGravatar Pantazis Deligiannis2013-08-20
|\ \
* | | new option to disable checking for loop maintained invariants - this leads to...Gravatar Pantazis Deligiannis2013-08-15
| * | Reverted change to use MODEL_ON_FINAL_CHECK, which seems to cause Z3 unexpect...Gravatar Rustan Leino2013-08-02
| * | Turned on options in Z3 to try producing models for timeouts.Gravatar wuestholz2013-08-02
| * | Removed harmful "Assert(false)".Gravatar wuestholz2013-07-26
|/ /
* | Resolved some issues with data races.Gravatar wuestholz2013-07-23
* | More refactoringGravatar Ally Donaldson2013-07-22
* | small fix to pickup correctly the CVC4 executableGravatar Pantazis Deligiannis2013-07-22
* | fixGravatar Pantazis Deligiannis2013-07-22
* | refactoringGravatar Pantazis Deligiannis2013-07-22
* | refactoringGravatar Pantazis Deligiannis2013-07-22
* | 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
| |/ |/|