summaryrefslogtreecommitdiff
path: root/Source/Provers
Commit message (Expand)AuthorAge
* Some fixes to ITPGravatar akashlal2014-10-04
* minor fixes to interpolating TPGravatar akashlal2014-10-03
* Added a flag to initialize the interpolating TPGravatar akashlal2014-09-29
* Merge.Gravatar Dan Liew2014-09-24
|\
* | Remove dead method argumentGravatar Dan Liew2014-09-24
* | Let the SMT lib convert models to Z3-like modelsGravatar Dan Liew2014-09-24
| * (Subhajit) Added an interface for InterpolatingTheoremProverGravatar akashlal2014-09-24
| * Simple VC generation for SIGravatar akashlal2014-09-24
|/
* Patch by Jeroen Ketema.Gravatar Dan Liew2014-09-19
* Fix nasty bug introduced by commit 61a94f409975.Gravatar Dan Liew2014-07-15
* OnModel now carries the result of the prover callGravatar akashlal2014-06-28
* Small refactoringGravatar Ally Donaldson2014-06-06
* Merge duality changesGravatar Ken McMillan2014-05-26
|\
| * Conjecture printing for duality and child user time tracking.Gravatar Ken McMillan2014-05-26
* | Simplify Z3 executable discovery.Gravatar wuestholz2014-05-12
|/
* Added /printFixedPoint optionGravatar Ken McMillan2014-04-14
* Fixed bug in printing real literalsGravatar Rustan Leino2014-02-10
* Fix Boogie so it compiled with mono. Patch by Dan Liew.Gravatar Ally Donaldson2014-01-14
* fixed vc generation so that even when builtin array functions are used,Gravatar qadeer2013-12-28
* MergeGravatar Ally Donaldson2013-12-09
|\
* | Small change related to CVC4 support. Patch by Pantazis DeligiannisGravatar Ally Donaldson2013-12-09
| * The back pred files have been eliminated. The small backpred string is now d...Gravatar qadeer2013-12-08
|/
* 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