summaryrefslogtreecommitdiff
path: root/Source/Provers
Commit message (Expand)AuthorAge
* Added option of turning off model generation in SI. Can be very expensive som...Gravatar akashlal2011-11-26
* Boogie (and Dafny, with effects also on SscBoogie): I refactored CommandLine...Gravatar Rustan Leino2011-11-15
* 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
* MergeGravatar Michal Moskal2011-10-27
|\
* | Restart prover after out-of-memory error; honour -restartProver optionGravatar Michal Moskal2011-10-27
| * Boogie: internal clean-up, removed BvHandling type, everything now behaves as...Gravatar Rustan Leino2011-10-27
| * Boogie: Eliminated the /bv option. Only native bitvectors are supported now. ...Gravatar Rustan Leino2011-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
* fixed bug in vcgen for bitvectorsGravatar qadeer2011-07-09
* Don't send (check-sat) after error limit is reachedGravatar Michal Moskal2011-07-05
* MergeGravatar Michal Moskal2011-07-05
|\
| * Boogie: New cli option -z3exe:"path-to-z3.exe" allowing specifying path to th...Gravatar Unknown2011-07-05
* | Update the RECENT_Z3 #define to include SORT_AND_ORGravatar Michal Moskal2011-06-30
* | 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
|/
* Avoid restarting the theorem prover for stratified inlining because itGravatar Unknown2011-06-25
* further refactoringGravatar qadeer2011-06-24
* fixes to z3apiGravatar qadeer2011-06-24
* clean up in z3apiGravatar qadeer2011-06-22
* various fixes to port to latest version of Microsoft.Z3.dllGravatar qadeer2011-06-22
* 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
* Fixed a tricky bug in z3apiGravatar akashlal2011-03-18
* 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
* Renamed NonNullElements to NonNullDictionaryAndValues because the keys to dic...Gravatar mikebarnett2011-03-10
* Added a new solution configuration, Checked, that builds the Checked configur...Gravatar mikebarnett2011-03-07
generated by cgit v1.2.3 (git 2.39.1) at 2024-09-09 11:47:21 +0000