diff options
| author |  qadeer <qadeer@microsoft.com> | 2012-02-29 11:41:52 -0800 |
|---|---|---|
| committer | qadeer <qadeer@microsoft.com> | 2012-02-29 11:41:52 -0800 |
| commit | 812e6dbb864807936e17cc83adbe357b987bb264 (patch) | |
| tree | bd04885dcb332259632037f04f1bbfacf9dfedbf /Source/VCGeneration | |
| parent | 9474036365c43cbbb420ec96b3fe60068c60058e (diff) | |
bug fix
Diffstat (limited to 'Source/VCGeneration')
| -rw-r--r-- | Source/VCGeneration/StratifiedVC.cs | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/Source/VCGeneration/StratifiedVC.cs b/Source/VCGeneration/StratifiedVC.cs index 59008af7..b9b0928c 100644 --- a/Source/VCGeneration/StratifiedVC.cs +++ b/Source/VCGeneration/StratifiedVC.cs @@ -1255,7 +1255,7 @@ namespace VC Hashtable/*TransferCmd->ReturnCmd*/ gotoCmdOrigins = PassifyImpl(impl, program, out mvInfo);
var exprGen = checker.TheoremProver.Context.ExprGen;
VCExpr controlFlowVariableExpr = CommandLineOptions.Clo.UseLabels ? null : exprGen.Integer(BigNum.ZERO);
- vcMain = GenerateVC(impl, null, out mainLabel2absy, checker);
+ vcMain = GenerateVC(impl, controlFlowVariableExpr, out mainLabel2absy, checker);
if (!CommandLineOptions.Clo.UseLabels) {
VCExpr controlFlowFunctionAppl = exprGen.ControlFlowFunctionApplication(exprGen.Integer(BigNum.ZERO), exprGen.Integer(BigNum.ZERO));
VCExpr eqExpr = exprGen.Eq(controlFlowFunctionAppl, exprGen.Integer(BigNum.FromInt(impl.Blocks[0].UniqueId)));
|