summaryrefslogtreecommitdiff
path: root/Source/Provers
Commit message (Expand)AuthorAge
* 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
* Fix some more contracts.Gravatar mikebarnett2011-03-07
* Fix contracts so runtime checking can be turned on.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
* Allow recent Z3 versions to be usedGravatar MichalMoskal2011-02-21
* Move model printing to ErrorModel classGravatar MichalMoskal2011-02-21
* 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
* Handle /useArrayTheoryGravatar MichalMoskal2011-02-18