diff options
| author |  qadeer <qadeer@microsoft.com> | 2012-06-07 23:04:57 -0700 |
|---|---|---|
| committer | qadeer <qadeer@microsoft.com> | 2012-06-07 23:04:57 -0700 |
| commit | 9592ad585b9f2314b5983248e6fa7e12f6c8bbea (patch) | |
| tree | 6c603c49e2539f4d711710e126508831538c8024 /Source/VCGeneration/StratifiedVC.cs | |
| parent | 86075eb4e16ec383d9227cd11cf0d3ecdf95c8f8 (diff) | |
final (hopefully) fix to new SI
Diffstat (limited to 'Source/VCGeneration/StratifiedVC.cs')
| -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]));
}
|