From 812e6dbb864807936e17cc83adbe357b987bb264 Mon Sep 17 00:00:00 2001 From: qadeer Date: Wed, 29 Feb 2012 11:41:52 -0800 Subject: bug fix --- Source/Provers/Z3api/ProverLayer.cs | 2 +- Source/VCGeneration/StratifiedVC.cs | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/Source/Provers/Z3api/ProverLayer.cs b/Source/Provers/Z3api/ProverLayer.cs index bff7773c..3b7b8f43 100644 --- a/Source/Provers/Z3api/ProverLayer.cs +++ b/Source/Provers/Z3api/ProverLayer.cs @@ -158,7 +158,7 @@ REVERSE_IMPLIES= Encode P==>Q as Q||!P. } } - public class Z3apiProcessTheoremProver : ApiProverInterface + public class Z3apiProcessTheoremProver : ProverInterface { public Z3apiProcessTheoremProver(Z3InstanceOptions opts, DeclFreeProverContext ctxt) { 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))); -- cgit v1.2.3