summaryrefslogtreecommitdiff
path: root/Source/Provers
Commit message (Collapse)AuthorAge
* more work on reducing call stack consumptionGravatar qadeer2014-12-18
|
* patched two occurrences of StackOverflowException on benchmarks from IronCladGravatar qadeer2014-12-16
|
* Merge some FixpointVC changes that got left behindGravatar Ken McMillan2014-12-08
|\
* | Patch by Jeroen KetemaGravatar Dan Liew2014-12-01
| | | | | | | | | | | | | | | | | | | | Fix some of the interfacing with Z3 4.3.2 in SMTLib. In particular: * It makes the useSmtOutputFormat usable * It fixes parsing of bit vectors that occur in the models returned by Z3 Similar stuff might be broken in the other interfaces to Z3, but it shouldn’t be more broken than it already was.
* | Patch by Jeroen KetemaGravatar Dan Liew2014-11-17
| | | | | | | | Fix interfacing with CVC4 1.5
* | re-enabling -useUnsatCoreForContractInferGravatar shuvendu2014-11-07
| | | | | | | | An example houdini\testUnsatCore.bpl to test out the unsatCore (Currently seems to be not working)
* | Minor change to make some regression tests work with Z3 4.3.2Gravatar wuestholz2014-11-05
| |
* | Logging for SMTLib proverGravatar akashlal2014-11-05
| |
| * Merge FixpointVC changes with mainlineGravatar Ken McMillan2014-10-08
|/|
| * Added "extra recursion bound" to FixedpointVC to support Corral.Gravatar Ken McMillan2014-10-08
| |
* | 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
| | | | | | | | | | | | Patch by Jeroen Ketema
* | | Let the SMT lib convert models to Z3-like modelsGravatar Dan Liew2014-09-24
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | The Model parser for SMT models is broken beyond repair and this by-passes this. The code could be moved to the model parser, but that's a refactoring for another day. Also, the existing version already had multiple reparses going on and this at least removes one of those. Patch by Jeroen Ketema.
| * | (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
|/ | | | | | Only set produce-unsat-cores in the case /explainHoudini is passed. This allows contract inference to be used with solvers that do no support unsat cores, as long as no explanation of the Houdini run is required.
* Fix nasty bug introduced by commit 61a94f409975.Gravatar Dan Liew2014-07-15
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | There were many calls in the code to ``` new TokenTextWriter("<buffer>", buffer, false) ``` Prior to 61a94f409975 this was a call to the following constructor ``` TokenTextWriter(string filename, TextWriter writer, bool setTokens) ``` After that commit these then became calls to ``` TokenTextWriter(string filename, TextWriter writer, bool pretty) ``` An example of where this would cause issues was if ToString() was called on an AbsyCmd then the its token would be modified because the setTokens parameter was effectively set to True when the original intention was for it to be set to false! To fix this I've * Removed the default parameter value for pretty and fixed all uses so that we pass false where it was implicitly being set before * Where the intention was to set setTokens to false this has been fixed so it is actually set to false! Unfortunately I couldn't find a way of observing this bug from the Boogie executable so I couldn't create a test case. I could only observe it when I was using Boogie's APIs.
* 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
| | | | the program can be verified without the use of /useArrayTheory
* 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 ↵Gravatar qadeer2013-12-08
|/ | | | directly included in ProverInterface.cs.
* 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 ↵Gravatar Pantazis Deligiannis2013-08-15
| | | | | | | | | | | | to an underapproximation that helps to speedup houdini refutation of candidates
| * | Reverted change to use MODEL_ON_FINAL_CHECK, which seems to cause Z3 ↵Gravatar Rustan Leino2013-08-02
| | | | | | | | | | | | unexpectedly to output model information
| * | 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
| |
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-04 22:09:14 +0000