summaryrefslogtreecommitdiff
path: root/Source/Core
Commit message (Expand)AuthorAge
* Add simplified may-unverified analysis and instrumentation.Gravatar Valentin Wüstholz2015-11-20
* Fix issue with partially-verified assertions.Gravatar Valentin Wüstholz2015-11-19
* Add experimental support for optimization (requires Z3 build after changeset ...Gravatar Valentin Wüstholz2015-11-18
* Add support for identifying unnecessary assumes.Gravatar Valentin Wüstholz2015-11-16
* Document the new behaviour of the ``-proc:`` command line optionGravatar Dan Liew2015-10-31
* Added wild card matching for /proc flagGravatar Shaobo2015-10-31
* fix for deterministicExtractLoops for nested loopsGravatar Shuvendu Lahiri2015-10-27
* Bug fix for deterministExtractLoops for Shaobo's exampleGravatar Shuvendu Lahiri2015-10-26
* updateGravatar Shaz Qadeer2015-09-28
* Merge branch 'master' of https://github.com/boogie-org/boogieGravatar Rustan Leino2015-08-28
|\
* | Added /verifySnapshots:3, which prints recycled errors messages with the sour...Gravatar Rustan Leino2015-08-28
| * fix for /deterministicExtractLoops sed in SymDiffGravatar Shuvendu Lahiri2015-07-19
| * Update URL to boogie-partners to its new location on GitHub.Gravatar Dan Liew2015-06-28
| * Fix issue #16 reported by @crazyktGravatar Dan Liew2015-06-28
| * Normalise line endings using a .gitattributes file. UnfortunatelyGravatar Dan Liew2015-06-28
| * Remove dead file.Gravatar Dan Liew2015-06-28
| * fixed bug reported by ChrisGravatar qadeer2015-06-15
| * adding z3name optionGravatar Ken McMillan2015-06-15
| * Minor changesGravatar Valentin Wüstholz2015-06-12
| * Fix issue with computation of statement checksums for lambda expressions.Gravatar Valentin Wüstholz2015-06-12
| * Fix issue in checksum computation for lambda expressions.Gravatar Valentin Wüstholz2015-06-12
| * various changes for duality from dead codeplex repoGravatar U-REDMOND\kenmcmil2015-06-09
|/
* Improve support for diagnosing timeouts.Gravatar Valentin Wüstholz2015-06-08
* Fix minor issue.Gravatar Valentin Wüstholz2015-06-05
* Improve support for diagnosing timeouts.Gravatar Valentin Wüstholz2015-06-05
* Add some experimental support for diagnosing timeouts.Gravatar Valentin Wüstholz2015-05-18
* Minor refactoringGravatar Valentin Wüstholz2015-05-17
* Make caching of verification results more fine-grained for changes that affec...Gravatar Valentin Wüstholz2015-05-17
* Add support for 'verified_under' attributes on procedure calls and invariants.Gravatar Valentin Wüstholz2015-04-29
* VC gen for security propertiesGravatar akashlal2015-04-05
* Eliminated calls to deprecated method.Gravatar wuestholz2015-02-18
* Added a setter for CommandLineOptions.ProverOptions and fixed several contracts.Gravatar wuestholz2015-02-18
* Protect Bitvector field of BvExtractExpr when it is immutable.Gravatar Dan Liew2015-02-12
* Protect E0 and E1 in BvConcatExpr if Expr is immutable.Gravatar Dan Liew2015-02-12
* Fix what looked like a serious design issue when Type checkingGravatar Dan Liew2015-02-12
* When an Expr immutable, never change Type reference if it has been set,Gravatar Dan Liew2015-02-12
* Protect the Args field of NAryExpr when it is immutable.Gravatar Dan Liew2015-02-12
* Fix performance issue in ComputeHashCode() methods of Expr classes.Gravatar Dan Liew2015-02-02
* Fix typechecking immutable Expr when we haveGravatar Dan Liew2015-01-31
* Made it produce slightly different passive commands for assignments to assump...Gravatar wuestholz2015-01-30
* Protect the body of ForAllExpr, ExistsExpr and LambdaExpr when theyGravatar Dan Liew2015-01-29
* Fix ForAllExpr, ExistsExpr and LambdaExpr constructors so it is possibleGravatar Dan Liew2015-01-29
* Protect the NAryExpr.Fun field when the NAryExpr is immutable.Gravatar Dan Liew2015-01-29
* Protect the Expr field of OldExpr if it is immutable. Add unit testGravatar Dan Liew2015-01-29
* Protect the Type field of an Expr if is Immutable. Note if the ExprGravatar Dan Liew2015-01-29
* Protect the Name and Decl fields of IdentifierExpr when it isGravatar Dan Liew2015-01-29
* Prevent a BvConst being changed once constructed. The motivationGravatar Dan Liew2015-01-29
* Add the ability to declare Expr to be immutable at construction time.Gravatar Dan Liew2015-01-29
* Fixed minor issue.Gravatar wuestholz2015-01-26
* Worked on the verification result caching (statement checksums).Gravatar wuestholz2015-01-26