diff options
| -rw-r--r-- | Source/VCGeneration/StratifiedVC.cs | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/Source/VCGeneration/StratifiedVC.cs b/Source/VCGeneration/StratifiedVC.cs index abe93783..e589bb44 100644 --- a/Source/VCGeneration/StratifiedVC.cs +++ b/Source/VCGeneration/StratifiedVC.cs @@ -139,8 +139,7 @@ namespace VC { Contract.Assert(interfaceExprs.Count == svc.interfaceExprVars.Count);
StratifiedInliningInfo info = svc.info;
VCExpressionGenerator gen = info.vcgen.prover.VCExprGen;
- // VCExpr ret = gen.Eq(reachExpr, svc.entryExprVar);
- VCExpr ret = VCExpressionGenerator.True;
+ VCExpr ret = svc.vcexpr;
for (int i = 0; i < interfaceExprs.Count; i++) {
ret = gen.And(ret, gen.Eq(interfaceExprs[i], svc.interfaceExprVars[i]));
}
|