summaryrefslogtreecommitdiff
path: root/Source/Provers/SMTLib/ProverInterface.cs
Commit message (Expand)AuthorAge
* eliminated class ErrorModelGravatar qadeer2012-04-28
* removed proccopybounding codeGravatar 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
|/
* Cleaned up code by getting rid of ApiProverInterface.Gravatar Unknown2012-02-29
* Simplification to previous checkinGravatar Michal Moskal2012-02-28
* Introduce ApiProverInterface.CheckOutcomeCore() for stratified inlining; simp...Gravatar Michal Moskal2012-02-28
* fixed up SI to work with new error trace generationGravatar qadeer2012-02-28
* various fixes related to new error tracesGravatar qadeer2012-02-27
* further fixes related to using uninterpreted function for error tracesGravatar qadeer2012-02-25
* bug fixes related to using ControlFlowFunction instead of labelsGravatar qadeer2012-02-23
* using model instead of labelsGravatar Unknown2012-02-23
* Use DateTime.UtcNow instead of DateTime.NowGravatar stobies2012-01-11
* made delegate a datatypeGravatar qadeer2011-12-30
* fixed problems with datatypesGravatar qadeer2011-12-29
* Produce unsat cores only when enabled (in stratified inlining)Gravatar Unknown2011-11-11
* Fixed the generation of names for datatype functions to use the API forGravatar Mike Barnett2011-10-31
* Boogie: Get rid of {:ignore} feature on axiomsGravatar Michal Moskal2011-10-27
* Restart prover after out-of-memory error; honour -restartProver optionGravatar Michal Moskal2011-10-27
* Sync timeout messages with Z3 prover interfaceGravatar Michal Moskal2011-10-21
* Added a push+pop+unsat-core interface to SMTLib (for stratified inlining only)Gravatar Unknown2011-10-19
* implementing datatypesGravatar qadeer2011-10-05
* Add PROVER_PATH prover option (to base options, but currently only used by SM...Gravatar Michal Moskal2011-08-29
* Don't send (check-sat) after error limit is reachedGravatar Michal Moskal2011-07-05
* SMTLib: Only use (set-logic ...) when requested; quote some more symbolsGravatar Michal Moskal2011-06-30
* Don't set logic to UFNIA when /useArrayTheoryGravatar Michal Moskal2011-05-09
* Use (get-model) Z3 command; quote skolem-idsGravatar Michal Moskal2011-04-28
* Fix parsing of (labels) Z3 response; complain about unrecognized responses thereGravatar Michal Moskal2011-04-28
* Use :reason-unknown not :last-failure for Z3 in SMT mode; disable SORT_AND_OR...Gravatar Michal Moskal2011-04-28
* Updates for the latest changes in Z3's SMT2 parserGravatar Michal Moskal2011-04-22
* Replaced all dictionaries that mapped to bool (i.e., were being used to imple...Gravatar mikebarnett2011-03-10
* Mimic Z3 logic for figuring out the blocking clause for the next counterexampleGravatar MichalMoskal2011-02-23
* Add MULTI_TRACES prover option (equivalent of /z3multipleErrors)Gravatar MichalMoskal2011-02-23
* Check for timeout/memoryoutGravatar MichalMoskal2011-02-23
* Dispose of the prover when Close() is called.Gravatar MichalMoskal2011-02-23
* Do typed->untyped translation for -mv variablesGravatar MichalMoskal2011-02-23
* Provide dummy implementation of FlushAxiomsToTheoremProver()Gravatar MichalMoskal2011-02-23
* Implement Push/Pop interface.Gravatar MichalMoskal2011-02-23
* Per SMT standard push requires an argumentGravatar MichalMoskal2011-02-21
* Print prover errors on stdout (same as prover warnings)Gravatar MichalMoskal2011-02-18
* Allow use ErrorModel as a container for Model - make -mv work with SMTLib on Z3Gravatar MichalMoskal2011-02-18
* Ask Z3 to generate models, in V2 format, when neededGravatar MichalMoskal2011-02-18
* Intercept Z3 warnings and pass them onGravatar MichalMoskal2011-02-18