summaryrefslogtreecommitdiff
path: root/Source
Commit message (Collapse)AuthorAge
...
* Handle as-array[...] model elementsGravatar MichalMoskal2011-02-23
|
* Fixes in /useArrayTheory handlingGravatar MichalMoskal2011-02-23
|
* Parse else-> clauses in the modelGravatar MichalMoskal2011-02-23
| | | | Disable MODEL_PARTIAL in SMTLib
* Throw exceptions when push/pop interface is used but not implementedGravatar MichalMoskal2011-02-23
| | | | Complete ErrorModel tables with the final bogus else clause
* Pass :skolemid to SMTLib proverGravatar MichalMoskal2011-02-23
|
* Implement Push/Pop interface.Gravatar MichalMoskal2011-02-23
| | | | Implement ProverContext.Lookup method.
* Allow recent Z3 versions to be usedGravatar MichalMoskal2011-02-21
|
* Move model printing to ErrorModel classGravatar MichalMoskal2011-02-21
| | | | Allow construction of ErrorModel instance from Model instance
* Per SMT standard push requires an argumentGravatar MichalMoskal2011-02-21
|
* Add some ExpertLevel functionsGravatar MichalMoskal2011-02-21
|
* Set Id of Elements.Gravatar MichalMoskal2011-02-21
| | | | Add some explanation at the beginning of the file.
* Dafny: Improved scheme for splitting expressions. Also, report each split ↵Gravatar rustanleino2011-02-19
| | | | in error messages.
* Print prover errors on stdout (same as prover warnings)Gravatar MichalMoskal2011-02-18
|
* Fix help for /mvGravatar MichalMoskal2011-02-18
|
* Allow use ErrorModel as a container for Model - make -mv work with SMTLib on Z3Gravatar MichalMoskal2011-02-18
|
* Accomodate for recent changes in Z3 V2 model formatGravatar 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
|
* Expose ToByteArray()Gravatar MichalMoskal2011-02-18
|
* Dafny:Gravatar rustanleino2011-02-17
| | | | | | | | | | | | | | | | | | * Big change: Add type and allocatedness information everywhere in the Boogie translation. This not only fixes some potential soundness problems (see Test/dafny1/TypeAntecedents.dfy), but it also gives more information about the program. On the downside, it also requires discharging more antecedents in order to use some axioms. Another downside is that overall performance has gone down (however, this may be just an indirect consequence of the change, as it was in one investigated case). * Increase the applicability of function axioms (extending the coarse-grain function/module height mechanism used as an antecedent of function axioms). (Internally, this uses the new canCall mechanism.) * Extend language with "allocated( Expr )" expressions, which for any type of expression "Expr" says that "Expr" is allocated and has the expected type. * More details error messages about ill-defined expressions (internally, by using CheckWellformedness instead of "assert IsTotal") * Add axioms about idempotence of set union and intersection * The compiler does not support (the experimental feature) coupling invariants, so generate error if the compiler ever gets one * In the implementation, combine common behavior of MatchCaseStmt and MatchCaseExpr into a superclass MatchCase * Fixed error in translation of while(*)
* Boogie: Fixed problem with binding power of .[.] versus type coercions in ↵Gravatar rustanleino2011-02-17
| | | | pretty printing
* 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
|
* Add IEnumerable.IterGravatar 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
|
* Stratified inlining: Added concrete values to error traces. Added an extra ↵Gravatar akashlal2011-02-17
| | | | flag "inferLeastForUnsat".
* 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
|
* Add VCExprNAry.UniformArguments property to return arguments of nested ↵Gravatar MichalMoskal2011-02-15
| | | | And/Or nodes.
* Add some extension methods to IEnumberable<T>Gravatar 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
|
* Fix with timeoutGravatar akashlal2011-02-12
|
* Better support for timeoutGravatar akashlal2011-02-12
|
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-08 15:32:29 +0000