summaryrefslogtreecommitdiff
path: root/Source/VCExpr
Commit message (Expand)AuthorAge
* 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
| * mergeGravatar Pantazis Deligiannis2013-07-06
| |\ | |/ |/|
* | Fixes for duality under corralGravatar Ken McMillan2013-06-14
| * CVC4 ParserGravatar pantazis2013-06-12
|/
* removed call forall and * args to callsGravatar Unknown2013-02-23
* Removed old comments about "BASEMOVE" and other constructor calls, where the ...Gravatar Unknown2013-01-07
* Boogie: added type 'real' with overloaded arithmetic operations plus real div...Gravatar boehmes2012-09-27
* Removed AIFramework from Boogie -- use native trivial or native interval-base...Gravatar boehmes2012-09-27
* Boogie: Get rid of {:inline} attributes on axiomsGravatar Michal Moskal2011-10-27
* Boogie: Get rid of {:ignore} feature on axiomsGravatar Michal Moskal2011-10-27
* Boogie: internal clean-up, removed BvHandling type, everything now behaves as...Gravatar Rustan Leino2011-10-27
* Name the constant used in @MV_state function applications - otherwise we get ...Gravatar Michal Moskal2011-09-26
* Boogie: use (WEIGHT 0) with the select-of-store axiomsGravatar Rustan Leino2011-06-29
* Dafny: compile quantifiersGravatar rustanleino2011-03-26
* Re-enabled quantifier checking in the Checked configuration.Gravatar mikebarnett2011-03-16
* new algorithm for dead code detection (vc:doomed)Gravatar schaef2011-03-15
* 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
* Add VCExprNAry.UniformArguments property to return arguments of nested And/Or...Gravatar MichalMoskal2011-02-15