summaryrefslogtreecommitdiff
path: root/Source
Commit message (Expand)AuthorAge
...
* 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
* Minor change to the encoding of partially verified assertions as VCGravatar wuestholz2015-01-30
* Backed out changeset ed4196d6fe50Gravatar Dan Liew2015-01-29
* Make NUnit.Runners a require NuGet package again. This is anGravatar Dan Liew2015-01-29
* Tweak the unit test documentation on Visual studio.Gravatar Dan Liew2015-01-29
* Try to fix the "out-of-the-box" build of Boogie under Visual Studio. It turnsGravatar Dan Liew2015-01-29
* Improve documentation on testing.Gravatar Dan Liew2015-01-29
* Made the trace output for the caching more detailed.Gravatar wuestholz2015-01-29
* Add unit tests to check that ComputeHashCode() and GetHashCode() agreeGravatar Dan Liew2015-01-29
* Add unit tests to check that ComputeHashCode() and GetHashCode() agreeGravatar Dan Liew2015-01-29
* 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
* Add some unit tests to check the enforcement of Expr immutability.Gravatar 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
* Handle timeout in refinement loopGravatar akashlal2015-01-28
* Fixed minor issue.Gravatar wuestholz2015-01-26
* Worked on the verification result caching (statement checksums).Gravatar wuestholz2015-01-26
* Minor changeGravatar wuestholz2015-01-26
* Minor changeGravatar wuestholz2015-01-26
* Worked on the verification result caching (trace output).Gravatar wuestholz2015-01-26
* 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
* Worked on the verification result caching (use weights for extracted functions).Gravatar wuestholz2015-01-24
* Worked on the verification result caching (use native support for partially v...Gravatar wuestholz2015-01-16
* Fixes to StagedHoudiniGravatar Ally Donaldson2015-01-23
* MergeGravatar Ally Donaldson2015-01-22
|\
* | Fixes to StagedHoudiniGravatar Ally Donaldson2015-01-22
| * MergeGravatar qadeer2015-01-16
| |\ | |/ |/|
| * removed "layer" attribute from the desugared programGravatar qadeer2015-01-16
* | Worked on StagedHoudiniGravatar Ally Donaldson2015-01-16
* | Fix related to limitations in CVC4 model parsingGravatar Ally Donaldson2015-01-14
* | MergeGravatar Ally Donaldson2015-01-13
|\ \
| * \ Merging changes from wuestholz/BoogieInvariantFixesIIIIGravatar wuestholz2015-01-13
| |\ \
| * \ \ Merging changes from 0biha/BoogieInvariantFixesIIIaGravatar wuestholz2015-01-13
| |\ \ \ | | |_|/ | |/| |
* | | | Removed unnecessary stage-related attributes from candidate annotations.Gravatar Ally Donaldson2015-01-10
| | | * Made 2 invariants of class 'VariableCollector' robust by:Gravatar wuestholz2015-01-09