diff options
| author |  qadeer <unknown> | 2012-02-23 23:32:00 -0800 |
|---|---|---|
| committer | qadeer <unknown> | 2012-02-23 23:32:00 -0800 |
| commit | 44cc8ee3486a320aae809bc4755f4da8c4de4b79 (patch) | |
| tree | 8955f708bb69f407640ca7ccf85e5dbff98abcfb /Source/VCGeneration/Wlp.cs | |
| parent | 88a325c862048ab6d487fc8f5d6fcba3602960df (diff) | |
bug fixes related to using ControlFlowFunction instead of labels
Diffstat (limited to 'Source/VCGeneration/Wlp.cs')
| -rw-r--r-- | Source/VCGeneration/Wlp.cs | 4 |
1 files changed, 2 insertions, 2 deletions
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);
}
}
}
|