summaryrefslogtreecommitdiff
path: root/Source/Provers
Commit message (Collapse)AuthorAge
* 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
| | | | | Add supported :prover commands Minor fixes
* Handle /useArrayTheoryGravatar MichalMoskal2011-02-18
|
* Intercept Z3 warnings and pass them onGravatar MichalMoskal2011-02-18
|
* Remove workaround for Z3 scanner problems (fixed now); fix one commentGravatar MichalMoskal2011-02-18
|
* Recognize () as identifier terminatorsGravatar MichalMoskal2011-02-18
|
* Handle bitvectorsGravatar MichalMoskal2011-02-18
|
* Use explicit mechanism for skipping to the next assertionGravatar MichalMoskal2011-02-17
|
* Disable MBQI and AUTO_CONFIGGravatar MichalMoskal2011-02-17
|
* Kill the solver process when ctrl-c is pressedGravatar MichalMoskal2011-02-17
|
* Provide /p: as the short form of /proverOpt:.Gravatar MichalMoskal2011-02-17
| | | | | Add /p:O:<name>=<value> and /p:C:<solver-argument> prover options in SMT. Add default Z3 options when using Z3.
* Read prover responses; handle labelsGravatar MichalMoskal2011-02-17
|
* Make it possible to run Z3 on pipe; use generic PROVER_LOG optionsGravatar MichalMoskal2011-02-17
|
* Kill {:prover "..."} attribute support; no one ever used this stuffGravatar MichalMoskal2011-02-17
|
* Don't use Simplify's LogProverInterfaceGravatar MichalMoskal2011-02-17
|
* Indentation.Gravatar MichalMoskal2011-02-17
|
* Start implementation of pipe communication in SMTLIB backendGravatar MichalMoskal2011-02-17
|
* Fix printing of type-proxiesGravatar MichalMoskal2011-02-16
|
* Bugfixes in select-of-store axiomsGravatar MichalMoskal2011-02-16
|
* Skip "(assert true)" in output; skip "Linearing..." messages when they are fastGravatar MichalMoskal2011-02-16
|
* Fix let scopingGravatar MichalMoskal2011-02-15
|
* Workaround bug in Z3 SMT parserGravatar MichalMoskal2011-02-15
|
* Use SMT2 top-level syntaxGravatar MichalMoskal2011-02-15
|
* Use the new UniformArguments property; formattingGravatar MichalMoskal2011-02-15
|
* Print terms in SMT2 syntax (drop term/formula distinction)Gravatar MichalMoskal2011-02-15
|
* Move name-quoting (already for SMT2 not SMT1) into a seprate classGravatar MichalMoskal2011-02-15
|
* Better support for timeoutGravatar akashlal2011-02-12
|
* Add USE_PREDICATES option to TPTP and SMT proversGravatar MichalMoskal2011-02-11
|
* Get rid of -smtOutput option. Add /proverOpt:OUTPUT=... to SMT and TPTP ↵Gravatar MichalMoskal2011-02-11
| | | | provers. Add handling of help message about /proverOpt.
* Boogie: Yet another refinement of how Z3 is found. Previously, it would ↵Gravatar rustanleino2011-02-09
| | | | only look in one of "c:\Program Files\Microsoft Research" and "c:\Program Files (x86)\Microsoft Research", even if both existed (which meant that it might have looked in the wrong one). Now, both are considered.
* implemented /UseUnsatCoreForInlining option for use in stratified inliningGravatar qadeer2011-02-06
|
* Look for z3.exe in the prover plugin directory first.Gravatar MichalMoskal2011-02-02
|
* Boogie: Made the algorithm for finding Z3 more robust.Gravatar wuestholz2011-01-21
|
* Make the SMTLIB backend work again, particularly with /typeEncoding:mGravatar MichalMoskal2011-01-19
|
* Fix a bug in distinct() encodingGravatar MichalMoskal2011-01-19
|
* The TPTP backend works for some very limited examplesGravatar MichalMoskal2011-01-18
|
* Copy SMTLib "prover" as a basis for TPTP "prover".Gravatar MichalMoskal2011-01-18
|
* Use a made-up name when Context.Lookup() cannot find a nameGravatar MichalMoskal2010-12-10
|
* Don't crash in Context.Lookup when the namer has never seen the name. This ↵Gravatar MichalMoskal2010-12-10
| | | | happens when the name is never used in the VC (e.g. it gets peep-hole optimized).
* z3api: Bug fix with timeout. Use CheckAssumptions.Gravatar akashlal2010-12-07
|
* Added version.cs as link to those projects that were missing itGravatar stobies2010-12-06
| | | | Select 4.0 client profile on all projects
* Factored out the ParserHelper class into a separate project and updated the ↵Gravatar wuestholz2010-12-02
| | | | | | files generated by Coco/R. This was done to support sharing of the Coco/R .frame files with Spec#.
* Eliminated dependencies on SpecSharp and CCI from Boogie.sln and Dafny.slnGravatar qadeer2010-12-01
|
* z3api: Print log in smtlib2 format. Use CheckAssumptions (currently broken)Gravatar akashlal2010-11-29
|
* Added CheckAssumptions api interfaceGravatar akashlal2010-11-28
|
* added a fix for a bug in the Evaluate function.Gravatar qadeer2010-11-27
|
* changed the procedure Check so that the conflict clause is blocked only when ↵Gravatar qadeer2010-11-27
| | | | more than one counterexample is needed.
* Ported all projects to .NET Framework 4.0 in both Boogie.sln and Dafny.sln. ↵Gravatar qadeer2010-11-27
| | | | Removed references to Microsoft.Contracts.dll everywhere since that is available in .NET Framework 4.0.
* Some changes to the prover interface to make way for z3-api.Gravatar akashlal2010-11-24
|
* Boogie: Look for Z3 versions up to 2.20.Gravatar wuestholz2010-11-23
|
generated by cgit v1.2.3 (git 2.39.1) at 2024-08-05 22:00:48 +0000