diff options
Diffstat (limited to 'Source/VCGeneration')
| -rw-r--r-- | Source/VCGeneration/StratifiedVC.cs | 4 | ||||
| -rw-r--r-- | Source/VCGeneration/Wlp.cs | 4 |
2 files changed, 6 insertions, 2 deletions
diff --git a/Source/VCGeneration/StratifiedVC.cs b/Source/VCGeneration/StratifiedVC.cs index d13811e0..e0d7b4a7 100644 --- a/Source/VCGeneration/StratifiedVC.cs +++ b/Source/VCGeneration/StratifiedVC.cs @@ -208,8 +208,12 @@ namespace VC Hashtable/*<int, Absy!>*/ label2absy;
VCExpressionGenerator gen = checker.VCExprGen;
Contract.Assert(gen != null);
+
+
VCExpr vcexpr = gen.Not(GenerateVC(impl, null, out label2absy, checker));
Contract.Assert(vcexpr != null);
+
+
info.label2absy = label2absy;
info.mvInfo = mvInfo;
diff --git a/Source/VCGeneration/Wlp.cs b/Source/VCGeneration/Wlp.cs index 6d4d8051..94892c29 100644 --- a/Source/VCGeneration/Wlp.cs +++ b/Source/VCGeneration/Wlp.cs @@ -136,9 +136,9 @@ namespace VC { Contract.Assert(controlFlowFunctionAppl != null);
VCExpr assertFailure = gen.Eq(controlFlowFunctionAppl, gen.Integer(BigNum.FromInt(-ac.UniqueId)));
if (ctxt.Label2absy == null) {
- return gen.AndSimp(gen.Implies(assertFailure, C), gen.Implies(C, N));
+ return gen.AndSimp(gen.Implies(assertFailure, C), N);
} else {
- return gen.AndSimp(gen.LabelNeg(cce.NonNull(id.ToString()), gen.Implies(assertFailure, C)), gen.Implies(C, N));
+ return gen.AndSimp(gen.LabelNeg(cce.NonNull(id.ToString()), gen.Implies(assertFailure, C)), N);
}
}
}
|