summaryrefslogtreecommitdiff
path: root/Source/Provers/SMTLib
Commit message (Expand)AuthorAge
...
* more type checking for datatypesGravatar qadeer2012-03-18
* 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
* MergeGravatar qadeer2012-02-23
|\
* | using model instead of labelsGravatar Unknown2012-02-23
| * added floating point keywords to reserved SMTwords listGravatar qadeer2012-02-20
|/
* minor fix in tracingGravatar qadeer2012-02-14
* minor bug in printing z3 path when running with /traceGravatar qadeer2012-02-09
* houdini will not request models nowGravatar qadeer2012-02-08
* Use DateTime.UtcNow instead of DateTime.NowGravatar stobies2012-01-11
* made delegate a datatypeGravatar qadeer2011-12-30
* fixed problems with datatypesGravatar qadeer2011-12-29
* Added option of turning off model generation in SI. Can be very expensive som...Gravatar akashlal2011-11-26
* 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