summaryrefslogtreecommitdiff
path: root/Source/VCExpr
Commit message (Expand)AuthorAge
* Add support for weights on soft assumes.Gravatar Valentin Wüstholz2016-03-07
* Improve support for optimization and identifying unnecessary assumes.Gravatar Valentin Wüstholz2016-03-03
* Bug fix in determining whether a type parameter is boundedGravatar qunyanm2016-01-19
* Minor changesGravatar Valentin Wüstholz2015-11-19
* Add experimental support for optimization (requires Z3 build after changeset ...Gravatar Valentin Wüstholz2015-11-18
* Normalise line endings using a .gitattributes file. UnfortunatelyGravatar Dan Liew2015-06-28
* Add some experimental support for diagnosing timeouts.Gravatar Valentin Wüstholz2015-05-18
* Added a setter for CommandLineOptions.ProverOptions and fixed several contracts.Gravatar wuestholz2015-02-18
* Minor change to the encoding of partially verified assertions as VCGravatar wuestholz2015-01-30
* Change the return type of StandardVisitor.VisitLiteralExpr() fromGravatar Dan Liew2015-01-25
* Change the return type of StandardVisitor.VisitExistsExpr() fromGravatar Dan Liew2015-01-25
* Change the return type of StandardVisitor.VisitForAllExpr() fromGravatar Dan Liew2015-01-25
* Change the return type of StandardVisitor.VisitBvExtractExpr() fromGravatar Dan Liew2015-01-25
* Change the return type of StandardVisitor.VisitBvConcatExpr() fromGravatar Dan Liew2015-01-25
* Made invariant of class 'Trigger' robust byGravatar 0biha2015-01-01
* more work on reducing call stack consumptionGravatar qadeer2014-12-18
* patched two occurrences of StackOverflowException on benchmarks from IronCladGravatar qadeer2014-12-16
* Fix nasty bug introduced by commit 61a94f409975.Gravatar Dan Liew2014-07-15
* (Fixed and) strengthened contracts of ReadOnlyVisitor. The postconditions of...Gravatar Rustan Leino2014-02-24
* Fix Boogie so it compiled with mono. Patch by Dan Liew.Gravatar Ally Donaldson2014-01-14
* added syntax for par call and ParCallCmdGravatar qadeer2013-12-16
* added the QED build configurationGravatar qadeer2013-12-02
* fixed bugGravatar qadeer2013-09-09
* fixed the problem with codexprsGravatar qadeer2013-09-07
* When a codeexpr is used at the top-level in an assume statement, we use the a...Gravatar qadeer2013-09-04
* Avoid another potential data race.Gravatar wuestholz2013-07-23
* Resolved some issues with data races.Gravatar wuestholz2013-07-23
* Did some refactoring.Gravatar wuestholz2013-07-23
* Minor fixGravatar wuestholz2013-07-23
* Did some refactoring.Gravatar wuestholz2013-07-23
* Use 'All' and 'Any' instead of 'Contract.ForAll' and 'Contract.Exists' in cod...Gravatar wuestholz2013-07-22
* All ...Seq classes now goneGravatar Ally Donaldson2013-07-22
* ExprSeq: farewellGravatar Ally Donaldson2013-07-22
* RESeq: farewellGravatar Ally Donaldson2013-07-22
* BlockSeq: farewellGravatar Ally Donaldson2013-07-22
* CmdSeq: farewellGravatar Ally Donaldson2013-07-22
* Started to remove ...Seq classesGravatar Ally Donaldson2013-07-22
* More refactoringGravatar Ally Donaldson2013-07-22
* More refactoringGravatar Ally Donaldson2013-07-22
* More refactoring towards replacing PureCollections.Sequence with ListGravatar Ally Donaldson2013-07-22
* MergeGravatar Ally Donaldson2013-07-22
|\
* | Refactoring of TypeVariableSeqGravatar Ally Donaldson2013-07-22
* | Changed Has method of PureSequence to Contains to make refactoring easier.Gravatar Ally Donaldson2013-07-22
| * mergeGravatar Pantazis Deligiannis2013-07-22
| |\ | |/ |/|
* | Refactoring of VariableSeq and TypeSeqGravatar Ally Donaldson2013-07-22
* | Requires/EnsuresSeq replaced by List<Requires/Ensures>Gravatar Ally Donaldson2013-07-22
| * MergeGravatar Pantazis Deligiannis2013-07-15
|/|
* | Worked on the parallelization.Gravatar wuestholz2013-07-11
* | Worked on the parallelization.Gravatar wuestholz2013-07-10
* | Worked on the parallelization.Gravatar wuestholz2013-07-08