LetVC can get null label2absy from lazy inlining. So, I weakened the precondition otherwise the checked build was failing

1 files changed, 0 insertions, 2 deletions

diff --git a/Source/VCGeneration/VC.cs b/Source/VCGeneration/VC.cs
index 8c8b17a0..11db59b0 100644
--- a/Source/VCGeneration/VC.cs
+++ b/Source/VCGeneration/VC.cs
@@ -3621,7 +3621,6 @@ namespace VC {
                         Hashtable/*<int, Absy!>*/ label2absy,

                         ProverContext proverCtxt) {

       Contract.Requires(startBlock != null);

-      Contract.Requires(label2absy != null);

       Contract.Requires(proverCtxt != null);

 

       Contract.Ensures(Contract.Result<VCExpr>() != null);

@@ -3640,7 +3639,6 @@ namespace VC {
                         ProverContext proverCtxt)

     {

       Contract.Requires(block != null);

-      Contract.Requires(label2absy != null);

       Contract.Requires(blockVariables!= null);

       Contract.Requires(cce.NonNullElements(bindings));

       Contract.Requires(proverCtxt != null);