summaryrefslogtreecommitdiff
path: root/Source/Provers/SMTLib
Commit message (Expand)AuthorAge
* 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: Updated the error message for old versions of Z3.Gravatar wuestholz2011-10-28
* Boogie: Get rid of {:ignore} feature on axiomsGravatar Michal Moskal2011-10-27
* Boogie: Present a nice error message when Z3 of lesser version than 3.2 is foundGravatar 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
* Don't pass /T: option to Z3 - it kills Z3 prematurely when there are multiple...Gravatar Michal Moskal2011-10-21
* Improve logging when -proverOpt:VERBOSITY=1 or 2 is specifiedGravatar Michal Moskal2011-10-21
* Added a push+pop+unsat-core interface to SMTLib (for stratified inlining only)Gravatar Unknown2011-10-19
* added membership testsGravatar qadeer2011-10-05
* implementing datatypesGravatar qadeer2011-10-05
* check in support for generalized array theoryGravatar Unknown2011-09-06
* Fix printing of (Array ...) types with /useArrayTheoryGravatar Michal Moskal2011-09-06
* Support multi-dimensional arrays in SMTLib2 backend (using Z3 extension though)Gravatar Michal Moskal2011-09-06
* further fixes; temporarily commented outGravatar qadeer2011-09-03
* adding support for accessing Z3's generalized array theoryGravatar qadeer2011-09-02
* Add PROVER_PATH prover option (to base options, but currently only used by SM...Gravatar Michal Moskal2011-08-29
* Use SMT2 syntax for sign_extendGravatar Michal Moskal2011-08-22
* deleted lazyinlining option 2 and 3Gravatar qadeer2011-08-17
* Don't send (check-sat) after error limit is reachedGravatar Michal Moskal2011-07-05
* Add /T: option to Z3 to kill it if it exceeds soft timeout by more than 1sGravatar Michal Moskal2011-06-30
* 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
* Test commitGravatar Michal Moskal2011-04-05
* Use new, SMT2 compliant, Z3 syntax for labelsGravatar MichalMoskal2011-04-02
* Re-enabled quantifier checking in the Checked configuration.Gravatar mikebarnett2011-03-16
* Turn off quantifier checking in the runtime checking.Gravatar mikebarnett2011-03-14
* Replaced all dictionaries that mapped to bool (i.e., were being used to imple...Gravatar mikebarnett2011-03-10
* Added a new solution configuration, Checked, that builds the Checked configur...Gravatar mikebarnett2011-03-07
* Mimic Z3 logic for figuring out the blocking clause for the next counterexampleGravatar MichalMoskal2011-02-23
* Don't ever put a label under a quantifier.Gravatar MichalMoskal2011-02-23
* Add MULTI_TRACES prover option (equivalent of /z3multipleErrors)Gravatar MichalMoskal2011-02-23
* Add hack for {:bvbuiltin "sign_extend 42"}, which requires slightly different...Gravatar MichalMoskal2011-02-23
* Check for timeout/memoryoutGravatar MichalMoskal2011-02-23
* Strip (= 0) and (!= 0) from patterns (we used to allow that with anyNeq thing...Gravatar MichalMoskal2011-02-23
* Don't try to declare bv typesGravatar MichalMoskal2011-02-23
* Dispose of the prover when Close() is called.Gravatar MichalMoskal2011-02-23
* Set SOFT_TIMEOUT Z3 option if desired (SMT2 doesn't have :time-limit option!)Gravatar MichalMoskal2011-02-23
* Pass solverargumentsGravatar MichalMoskal2011-02-23
* Do typed->untyped translation for -mv variablesGravatar MichalMoskal2011-02-23
* Provide dummy implementation of FlushAxiomsToTheoremProver()Gravatar MichalMoskal2011-02-23
* Fixes in /useArrayTheory handlingGravatar MichalMoskal2011-02-23
* Parse else-> clauses in the modelGravatar MichalMoskal2011-02-23
* Pass :skolemid to SMTLib proverGravatar MichalMoskal2011-02-23
* Implement Push/Pop interface.Gravatar MichalMoskal2011-02-23