further fixes related to using uninterpreted function for error traces

removed Provers.Simplify, Provers.Z3, Provers.TPTP from the solution

12 files changed, 43 insertions, 167 deletions

diff --git a/Source/Boogie.sln b/Source/Boogie.sln
index 53130382..955dfb46 100644
--- a/Source/Boogie.sln
+++ b/Source/Boogie.sln
@@ -9,12 +9,8 @@ Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "Isabelle", "Provers\Isabell
 EndProject

 Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "AbsInt", "AbsInt\AbsInt.csproj", "{0EFA3E43-690B-48DC-A72C-384A3EA7F31F}"

 EndProject

-Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "Z3", "Provers\Z3\Z3.csproj", "{BB49B90B-BE21-4BE8-85BA-359FDB55F4DF}"

-EndProject

 Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "SMTLib", "Provers\SMTLib\SMTLib.csproj", "{9B163AA3-36BC-4AFB-88AB-79BC9E97E401}"

 EndProject

-Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "Simplify", "Provers\Simplify\Simplify.csproj", "{FEE9F01B-9722-4A76-A24B-72A4016DFA8E}"

-EndProject

 Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "VCGeneration", "VCGeneration\VCGeneration.csproj", "{E1F10180-C7B9-4147-B51F-FA1B701966DC}"

 EndProject

 Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "VCExpr", "VCExpr\VCExpr.csproj", "{56FFDBCA-7D14-43B8-A6CA-22A20E417EE1}"

@@ -37,8 +33,6 @@ Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "Model", "Model\Model.csproj
 EndProject

 Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "ParserHelper", "ParserHelper\ParserHelper.csproj", "{FCD3AC7F-9DFD-46C8-AB1E-09F0B0F16DC5}"

 EndProject

-Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "TPTP", "Provers\TPTP\TPTP.csproj", "{A598ED5A-93AD-4125-A555-3921A2F936FA}"

-EndProject

 Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "Houdini", "Houdini\Houdini.csproj", "{CF41E903-78EB-43BA-A355-E5FEB5ECECD4}"

 EndProject

 Global

@@ -136,31 +130,6 @@ Global
 		{0EFA3E43-690B-48DC-A72C-384A3EA7F31F}.z3apidebug|Mixed Platforms.ActiveCfg = Debug|Any CPU

 		{0EFA3E43-690B-48DC-A72C-384A3EA7F31F}.z3apidebug|Mixed Platforms.Build.0 = Debug|Any CPU

 		{0EFA3E43-690B-48DC-A72C-384A3EA7F31F}.z3apidebug|x86.ActiveCfg = z3apidebug|Any CPU

-		{BB49B90B-BE21-4BE8-85BA-359FDB55F4DF}.Checked|.NET.ActiveCfg = Checked|Any CPU

-		{BB49B90B-BE21-4BE8-85BA-359FDB55F4DF}.Checked|Any CPU.ActiveCfg = Checked|Any CPU

-		{BB49B90B-BE21-4BE8-85BA-359FDB55F4DF}.Checked|Any CPU.Build.0 = Checked|Any CPU

-		{BB49B90B-BE21-4BE8-85BA-359FDB55F4DF}.Checked|Mixed Platforms.ActiveCfg = Checked|Any CPU

-		{BB49B90B-BE21-4BE8-85BA-359FDB55F4DF}.Checked|Mixed Platforms.Build.0 = Checked|Any CPU

-		{BB49B90B-BE21-4BE8-85BA-359FDB55F4DF}.Checked|x86.ActiveCfg = Checked|Any CPU

-		{BB49B90B-BE21-4BE8-85BA-359FDB55F4DF}.Debug|.NET.ActiveCfg = Debug|Any CPU

-		{BB49B90B-BE21-4BE8-85BA-359FDB55F4DF}.Debug|.NET.Build.0 = Debug|Any CPU

-		{BB49B90B-BE21-4BE8-85BA-359FDB55F4DF}.Debug|Any CPU.ActiveCfg = Debug|Any CPU

-		{BB49B90B-BE21-4BE8-85BA-359FDB55F4DF}.Debug|Any CPU.Build.0 = Debug|Any CPU

-		{BB49B90B-BE21-4BE8-85BA-359FDB55F4DF}.Debug|Mixed Platforms.ActiveCfg = Debug|Any CPU

-		{BB49B90B-BE21-4BE8-85BA-359FDB55F4DF}.Debug|Mixed Platforms.Build.0 = Debug|Any CPU

-		{BB49B90B-BE21-4BE8-85BA-359FDB55F4DF}.Debug|x86.ActiveCfg = Debug|Any CPU

-		{BB49B90B-BE21-4BE8-85BA-359FDB55F4DF}.Release|.NET.ActiveCfg = Release|Any CPU

-		{BB49B90B-BE21-4BE8-85BA-359FDB55F4DF}.Release|Any CPU.ActiveCfg = Release|Any CPU

-		{BB49B90B-BE21-4BE8-85BA-359FDB55F4DF}.Release|Any CPU.Build.0 = Release|Any CPU

-		{BB49B90B-BE21-4BE8-85BA-359FDB55F4DF}.Release|Mixed Platforms.ActiveCfg = Release|Any CPU

-		{BB49B90B-BE21-4BE8-85BA-359FDB55F4DF}.Release|Mixed Platforms.Build.0 = Release|Any CPU

-		{BB49B90B-BE21-4BE8-85BA-359FDB55F4DF}.Release|x86.ActiveCfg = Release|Any CPU

-		{BB49B90B-BE21-4BE8-85BA-359FDB55F4DF}.z3apidebug|.NET.ActiveCfg = z3apidebug|Any CPU

-		{BB49B90B-BE21-4BE8-85BA-359FDB55F4DF}.z3apidebug|Any CPU.ActiveCfg = z3apidebug|Any CPU

-		{BB49B90B-BE21-4BE8-85BA-359FDB55F4DF}.z3apidebug|Any CPU.Build.0 = z3apidebug|Any CPU

-		{BB49B90B-BE21-4BE8-85BA-359FDB55F4DF}.z3apidebug|Mixed Platforms.ActiveCfg = Debug|Any CPU

-		{BB49B90B-BE21-4BE8-85BA-359FDB55F4DF}.z3apidebug|Mixed Platforms.Build.0 = Debug|Any CPU

-		{BB49B90B-BE21-4BE8-85BA-359FDB55F4DF}.z3apidebug|x86.ActiveCfg = z3apidebug|Any CPU

 		{9B163AA3-36BC-4AFB-88AB-79BC9E97E401}.Checked|.NET.ActiveCfg = Checked|Any CPU

 		{9B163AA3-36BC-4AFB-88AB-79BC9E97E401}.Checked|Any CPU.ActiveCfg = Checked|Any CPU

 		{9B163AA3-36BC-4AFB-88AB-79BC9E97E401}.Checked|Any CPU.Build.0 = Checked|Any CPU

@@ -186,31 +155,6 @@ Global
 		{9B163AA3-36BC-4AFB-88AB-79BC9E97E401}.z3apidebug|Mixed Platforms.ActiveCfg = Debug|Any CPU

 		{9B163AA3-36BC-4AFB-88AB-79BC9E97E401}.z3apidebug|Mixed Platforms.Build.0 = Debug|Any CPU

 		{9B163AA3-36BC-4AFB-88AB-79BC9E97E401}.z3apidebug|x86.ActiveCfg = z3apidebug|Any CPU

-		{FEE9F01B-9722-4A76-A24B-72A4016DFA8E}.Checked|.NET.ActiveCfg = Checked|Any CPU

-		{FEE9F01B-9722-4A76-A24B-72A4016DFA8E}.Checked|Any CPU.ActiveCfg = Checked|Any CPU

-		{FEE9F01B-9722-4A76-A24B-72A4016DFA8E}.Checked|Any CPU.Build.0 = Checked|Any CPU

-		{FEE9F01B-9722-4A76-A24B-72A4016DFA8E}.Checked|Mixed Platforms.ActiveCfg = Checked|Any CPU

-		{FEE9F01B-9722-4A76-A24B-72A4016DFA8E}.Checked|Mixed Platforms.Build.0 = Checked|Any CPU

-		{FEE9F01B-9722-4A76-A24B-72A4016DFA8E}.Checked|x86.ActiveCfg = Checked|Any CPU

-		{FEE9F01B-9722-4A76-A24B-72A4016DFA8E}.Debug|.NET.ActiveCfg = Debug|Any CPU

-		{FEE9F01B-9722-4A76-A24B-72A4016DFA8E}.Debug|.NET.Build.0 = Debug|Any CPU

-		{FEE9F01B-9722-4A76-A24B-72A4016DFA8E}.Debug|Any CPU.ActiveCfg = Debug|Any CPU

-		{FEE9F01B-9722-4A76-A24B-72A4016DFA8E}.Debug|Any CPU.Build.0 = Debug|Any CPU

-		{FEE9F01B-9722-4A76-A24B-72A4016DFA8E}.Debug|Mixed Platforms.ActiveCfg = Debug|Any CPU

-		{FEE9F01B-9722-4A76-A24B-72A4016DFA8E}.Debug|Mixed Platforms.Build.0 = Debug|Any CPU

-		{FEE9F01B-9722-4A76-A24B-72A4016DFA8E}.Debug|x86.ActiveCfg = Debug|Any CPU

-		{FEE9F01B-9722-4A76-A24B-72A4016DFA8E}.Release|.NET.ActiveCfg = Release|Any CPU

-		{FEE9F01B-9722-4A76-A24B-72A4016DFA8E}.Release|Any CPU.ActiveCfg = Release|Any CPU

-		{FEE9F01B-9722-4A76-A24B-72A4016DFA8E}.Release|Any CPU.Build.0 = Release|Any CPU

-		{FEE9F01B-9722-4A76-A24B-72A4016DFA8E}.Release|Mixed Platforms.ActiveCfg = Release|Any CPU

-		{FEE9F01B-9722-4A76-A24B-72A4016DFA8E}.Release|Mixed Platforms.Build.0 = Release|Any CPU

-		{FEE9F01B-9722-4A76-A24B-72A4016DFA8E}.Release|x86.ActiveCfg = Release|Any CPU

-		{FEE9F01B-9722-4A76-A24B-72A4016DFA8E}.z3apidebug|.NET.ActiveCfg = z3apidebug|Any CPU

-		{FEE9F01B-9722-4A76-A24B-72A4016DFA8E}.z3apidebug|Any CPU.ActiveCfg = z3apidebug|Any CPU

-		{FEE9F01B-9722-4A76-A24B-72A4016DFA8E}.z3apidebug|Any CPU.Build.0 = z3apidebug|Any CPU

-		{FEE9F01B-9722-4A76-A24B-72A4016DFA8E}.z3apidebug|Mixed Platforms.ActiveCfg = Debug|Any CPU

-		{FEE9F01B-9722-4A76-A24B-72A4016DFA8E}.z3apidebug|Mixed Platforms.Build.0 = Debug|Any CPU

-		{FEE9F01B-9722-4A76-A24B-72A4016DFA8E}.z3apidebug|x86.ActiveCfg = z3apidebug|Any CPU

 		{E1F10180-C7B9-4147-B51F-FA1B701966DC}.Checked|.NET.ActiveCfg = Checked|Any CPU

 		{E1F10180-C7B9-4147-B51F-FA1B701966DC}.Checked|Any CPU.ActiveCfg = Checked|Any CPU

 		{E1F10180-C7B9-4147-B51F-FA1B701966DC}.Checked|Any CPU.Build.0 = Checked|Any CPU

@@ -473,30 +417,6 @@ Global
 		{FCD3AC7F-9DFD-46C8-AB1E-09F0B0F16DC5}.z3apidebug|Mixed Platforms.ActiveCfg = Release|Any CPU

 		{FCD3AC7F-9DFD-46C8-AB1E-09F0B0F16DC5}.z3apidebug|Mixed Platforms.Build.0 = Release|Any CPU

 		{FCD3AC7F-9DFD-46C8-AB1E-09F0B0F16DC5}.z3apidebug|x86.ActiveCfg = Release|Any CPU

-		{A598ED5A-93AD-4125-A555-3921A2F936FA}.Checked|.NET.ActiveCfg = Checked|Any CPU

-		{A598ED5A-93AD-4125-A555-3921A2F936FA}.Checked|Any CPU.ActiveCfg = Checked|Any CPU

-		{A598ED5A-93AD-4125-A555-3921A2F936FA}.Checked|Any CPU.Build.0 = Checked|Any CPU

-		{A598ED5A-93AD-4125-A555-3921A2F936FA}.Checked|Mixed Platforms.ActiveCfg = Checked|Any CPU

-		{A598ED5A-93AD-4125-A555-3921A2F936FA}.Checked|Mixed Platforms.Build.0 = Checked|Any CPU

-		{A598ED5A-93AD-4125-A555-3921A2F936FA}.Checked|x86.ActiveCfg = Checked|Any CPU

-		{A598ED5A-93AD-4125-A555-3921A2F936FA}.Debug|.NET.ActiveCfg = Debug|Any CPU

-		{A598ED5A-93AD-4125-A555-3921A2F936FA}.Debug|Any CPU.ActiveCfg = Debug|Any CPU

-		{A598ED5A-93AD-4125-A555-3921A2F936FA}.Debug|Any CPU.Build.0 = Debug|Any CPU

-		{A598ED5A-93AD-4125-A555-3921A2F936FA}.Debug|Mixed Platforms.ActiveCfg = Debug|Any CPU

-		{A598ED5A-93AD-4125-A555-3921A2F936FA}.Debug|Mixed Platforms.Build.0 = Debug|Any CPU

-		{A598ED5A-93AD-4125-A555-3921A2F936FA}.Debug|x86.ActiveCfg = Debug|Any CPU

-		{A598ED5A-93AD-4125-A555-3921A2F936FA}.Release|.NET.ActiveCfg = Release|Any CPU

-		{A598ED5A-93AD-4125-A555-3921A2F936FA}.Release|Any CPU.ActiveCfg = Release|Any CPU

-		{A598ED5A-93AD-4125-A555-3921A2F936FA}.Release|Any CPU.Build.0 = Release|Any CPU

-		{A598ED5A-93AD-4125-A555-3921A2F936FA}.Release|Mixed Platforms.ActiveCfg = Release|Any CPU

-		{A598ED5A-93AD-4125-A555-3921A2F936FA}.Release|Mixed Platforms.Build.0 = Release|Any CPU

-		{A598ED5A-93AD-4125-A555-3921A2F936FA}.Release|x86.ActiveCfg = Release|Any CPU

-		{A598ED5A-93AD-4125-A555-3921A2F936FA}.z3apidebug|.NET.ActiveCfg = Release|Any CPU

-		{A598ED5A-93AD-4125-A555-3921A2F936FA}.z3apidebug|Any CPU.ActiveCfg = Release|Any CPU

-		{A598ED5A-93AD-4125-A555-3921A2F936FA}.z3apidebug|Any CPU.Build.0 = Release|Any CPU

-		{A598ED5A-93AD-4125-A555-3921A2F936FA}.z3apidebug|Mixed Platforms.ActiveCfg = Release|Any CPU

-		{A598ED5A-93AD-4125-A555-3921A2F936FA}.z3apidebug|Mixed Platforms.Build.0 = Release|Any CPU

-		{A598ED5A-93AD-4125-A555-3921A2F936FA}.z3apidebug|x86.ActiveCfg = Release|Any CPU

 		{CF41E903-78EB-43BA-A355-E5FEB5ECECD4}.Checked|.NET.ActiveCfg = Release|Any CPU

 		{CF41E903-78EB-43BA-A355-E5FEB5ECECD4}.Checked|Any CPU.ActiveCfg = Release|Any CPU

 		{CF41E903-78EB-43BA-A355-E5FEB5ECECD4}.Checked|Any CPU.Build.0 = Release|Any CPU

@@ -527,10 +447,7 @@ Global
 	EndGlobalSection

 	GlobalSection(NestedProjects) = preSolution

 		{435D5BD0-6F62-49F8-BB24-33E2257519AD} = {B758C1E3-824A-439F-AA2F-0BA1143E8C8D}

-		{BB49B90B-BE21-4BE8-85BA-359FDB55F4DF} = {B758C1E3-824A-439F-AA2F-0BA1143E8C8D}

 		{9B163AA3-36BC-4AFB-88AB-79BC9E97E401} = {B758C1E3-824A-439F-AA2F-0BA1143E8C8D}

-		{FEE9F01B-9722-4A76-A24B-72A4016DFA8E} = {B758C1E3-824A-439F-AA2F-0BA1143E8C8D}

 		{966DD87B-A29D-4F3C-9406-F680A61DC0E0} = {B758C1E3-824A-439F-AA2F-0BA1143E8C8D}

-		{A598ED5A-93AD-4125-A555-3921A2F936FA} = {B758C1E3-824A-439F-AA2F-0BA1143E8C8D}

 	EndGlobalSection

 EndGlobal

diff --git a/Source/BoogieDriver/BoogieDriver.cs b/Source/BoogieDriver/BoogieDriver.cs
index c2c09ded..9a30401d 100644
--- a/Source/BoogieDriver/BoogieDriver.cs
+++ b/Source/BoogieDriver/BoogieDriver.cs
@@ -443,11 +443,6 @@ namespace Microsoft.Boogie {
       Contract.Ensures(0 <= Contract.ValueAtReturn(out inconclusives) && 0 <= Contract.ValueAtReturn(out timeOuts));

 

       errorCount = verified = inconclusives = timeOuts = outOfMemories = 0;

-      CommandLineOptions.Clo.UseLabels =

-        CommandLineOptions.Clo.UseLabels ||

-        CommandLineOptions.Clo.SoundnessSmokeTest ||

-        !(CommandLineOptions.Clo.vcVariety == CommandLineOptions.VCVariety.Dag ||

-          CommandLineOptions.Clo.vcVariety == CommandLineOptions.VCVariety.DagIterative);

 

       // ---------- Infer invariants --------------------------------------------------------

 

@@ -509,13 +504,6 @@ namespace Microsoft.Boogie {
 

       #region Verify each implementation

 

-#if ROB_DEBUG

-      string now = DateTime.Now.ToString().Replace(' ','-').Replace('/','-').Replace(':','-');

-      System.IO.StreamWriter w = new System.IO.StreamWriter(@"\temp\batch_"+now+".bpl");

-      program.Emit(new TokenTextWriter(w));

-      w.Close();

-#endif

-

       ConditionGeneration vcgen = null;

       try {

         if (CommandLineOptions.Clo.vcVariety == CommandLineOptions.VCVariety.Doomed) {

diff --git a/Source/BoogieDriver/BoogieDriver.csproj b/Source/BoogieDriver/BoogieDriver.csproj
index 52714dc9..9b6e329b 100644
--- a/Source/BoogieDriver/BoogieDriver.csproj
+++ b/Source/BoogieDriver/BoogieDriver.csproj
@@ -184,22 +184,10 @@
       <Project>{435D5BD0-6F62-49F8-BB24-33E2257519AD}</Project>

       <Name>Isabelle</Name>

     </ProjectReference>

-    <ProjectReference Include="..\Provers\Simplify\Simplify.csproj">

-      <Project>{FEE9F01B-9722-4A76-A24B-72A4016DFA8E}</Project>

-      <Name>Simplify</Name>

-    </ProjectReference>

     <ProjectReference Include="..\Provers\SMTLib\SMTLib.csproj">

       <Project>{9B163AA3-36BC-4AFB-88AB-79BC9E97E401}</Project>

       <Name>SMTLib</Name>

     </ProjectReference>

-    <ProjectReference Include="..\Provers\TPTP\TPTP.csproj">

-      <Project>{A598ED5A-93AD-4125-A555-3921A2F936FA}</Project>

-      <Name>TPTP</Name>

-    </ProjectReference>

-    <ProjectReference Include="..\Provers\Z3\Z3.csproj">

-      <Project>{BB49B90B-BE21-4BE8-85BA-359FDB55F4DF}</Project>

-      <Name>Z3</Name>

-    </ProjectReference>

     <ProjectReference Include="..\VCGeneration\VCGeneration.csproj">

       <Project>{E1F10180-C7B9-4147-B51F-FA1B701966DC}</Project>

       <Name>VCGeneration</Name>

diff --git a/Source/Houdini/Checker.cs b/Source/Houdini/Checker.cs
index 3670c441..c12c6d8b 100644
--- a/Source/Houdini/Checker.cs
+++ b/Source/Houdini/Checker.cs
@@ -8,9 +8,7 @@ using System.Diagnostics.Contracts;
 using System.Collections.Generic;

 using Microsoft.Boogie;

 using Microsoft.Boogie.VCExprAST;

-using Microsoft.Boogie.Simplify;

-using Microsoft.Boogie.Z3;

-using Microsoft.Boogie.SMTLib;

+using Microsoft.Basetypes;

 using System.Collections;

 using System.IO;

 using System.Threading;

@@ -31,9 +29,6 @@ namespace Microsoft.Boogie.Houdini {
       descriptiveName = impl.Name;

       collector = new ConditionGeneration.CounterexampleCollector();

       collector.OnProgress("HdnVCGen", 0, 0, 0.0);

-      if (CommandLineOptions.Clo.SoundnessSmokeTest) {

-        throw new Exception("HoudiniVCGen does not support Soundness smoke test.");

-      }

 

       vcgen.ConvertCFG2DAG(impl, program);

       ModelViewInfo mvInfo;

@@ -64,10 +59,10 @@ namespace Microsoft.Boogie.Houdini {
         var ctx = checker.TheoremProver.Context;

         var bet = ctx.BoogieExprTranslator;

         VCExpr controlFlowVariableExpr = bet.LookupVariable(controlFlowVariable);

-        Contract.Assert(controlFlowVariableExpr != null);

-        VCExpr controlFlowFunctionAppl = ctx.ExprGen.ControlFlowFunctionApplication(controlFlowVariableExpr, ctx.ExprGen.Integer(Microsoft.Basetypes.BigNum.ZERO));

-        Contract.Assert(controlFlowFunctionAppl != null);

-        vc = ctx.ExprGen.Implies(ctx.ExprGen.Eq(controlFlowFunctionAppl, ctx.ExprGen.Integer(Microsoft.Basetypes.BigNum.FromInt(entryBlockId))), vc);

+        VCExpr eqExpr1 = ctx.ExprGen.Eq(controlFlowVariableExpr, ctx.ExprGen.Integer(BigNum.ZERO));

+        VCExpr controlFlowFunctionAppl = ctx.ExprGen.ControlFlowFunctionApplication(controlFlowVariableExpr, ctx.ExprGen.Integer(BigNum.ZERO));

+        VCExpr eqExpr2 = ctx.ExprGen.Eq(controlFlowFunctionAppl, ctx.ExprGen.Integer(BigNum.FromInt(entryBlockId)));

+        vc = ctx.ExprGen.Implies(eqExpr1, ctx.ExprGen.Implies(eqExpr2, vc));

       }

 

       DateTime now = DateTime.UtcNow;

diff --git a/Source/Houdini/Houdini.cs b/Source/Houdini/Houdini.cs
index 9735aec1..68a8efb6 100644
--- a/Source/Houdini/Houdini.cs
+++ b/Source/Houdini/Houdini.cs
@@ -8,9 +8,7 @@ using System.Diagnostics.Contracts;
 using System.Collections.Generic;

 using Microsoft.Boogie;

 using Microsoft.Boogie.VCExprAST;

-using Microsoft.Boogie.Simplify;

 using VC;

-using Microsoft.Boogie.Z3;

 using System.Collections;

 using System.IO;

 using Microsoft.AbstractInterpretationFramework;

diff --git a/Source/Houdini/Houdini.csproj b/Source/Houdini/Houdini.csproj
index c4d4cb8a..af1755a3 100644
--- a/Source/Houdini/Houdini.csproj
+++ b/Source/Houdini/Houdini.csproj
@@ -106,18 +106,10 @@
       <Project>{FCD3AC7F-9DFD-46C8-AB1E-09F0B0F16DC5}</Project>

       <Name>ParserHelper</Name>

     </ProjectReference>

-    <ProjectReference Include="..\Provers\Simplify\Simplify.csproj">

-      <Project>{FEE9F01B-9722-4A76-A24B-72A4016DFA8E}</Project>

-      <Name>Simplify</Name>

-    </ProjectReference>

     <ProjectReference Include="..\Provers\SMTLib\SMTLib.csproj">

       <Project>{9B163AA3-36BC-4AFB-88AB-79BC9E97E401}</Project>

       <Name>SMTLib</Name>

     </ProjectReference>

-    <ProjectReference Include="..\Provers\Z3\Z3.csproj">

-      <Project>{BB49B90B-BE21-4BE8-85BA-359FDB55F4DF}</Project>

-      <Name>Z3</Name>

-    </ProjectReference>

     <ProjectReference Include="..\VCExpr\VCExpr.csproj">

       <Project>{56FFDBCA-7D14-43B8-A6CA-22A20E417EE1}</Project>

       <Name>VCExpr</Name>

diff --git a/Source/Provers/SMTLib/Inspector.cs b/Source/Provers/SMTLib/Inspector.cs
index 4126c169..362502f3 100644
--- a/Source/Provers/SMTLib/Inspector.cs
+++ b/Source/Provers/SMTLib/Inspector.cs
@@ -11,7 +11,6 @@ using System.Collections.Generic;
 using System.Diagnostics.Contracts;

 //using util;

 using Microsoft.Boogie;

-using Microsoft.Boogie.Simplify;

 using Microsoft.Basetypes;

 using Microsoft.Boogie.VCExprAST;

 

diff --git a/Source/Provers/SMTLib/ProverInterface.cs b/Source/Provers/SMTLib/ProverInterface.cs
index 657603d0..4c0597f9 100644
--- a/Source/Provers/SMTLib/ProverInterface.cs
+++ b/Source/Provers/SMTLib/ProverInterface.cs
@@ -17,7 +17,6 @@ using Microsoft.Boogie;
 using Microsoft.Boogie.VCExprAST;

 using Microsoft.Boogie.Clustering;

 using Microsoft.Boogie.TypeErasure;

-using Microsoft.Boogie.Simplify;

 using System.Text;

 

 namespace Microsoft.Boogie.SMTLib

@@ -285,15 +284,6 @@ namespace Microsoft.Boogie.SMTLib
         Process.Close();

     }

 

-    string controlFlowVariable;

-

-    private VCExpr ArgumentZero(VCExpr vc) {

-      VCExprNAry naryExpr = vc as VCExprNAry;

-      if (naryExpr == null)

-        return null;

-      return naryExpr[0];

-    }

-

     public override void BeginCheck(string descriptiveName, VCExpr vc, ErrorHandler handler)

     {

       //Contract.Requires(descriptiveName != null);

@@ -307,9 +297,6 @@ namespace Microsoft.Boogie.SMTLib
         currentLogFile.Write(common.ToString());

       }

 

-      if (!CommandLineOptions.Clo.UseLabels)

-        controlFlowVariable = VCExpr2String(ArgumentZero(ArgumentZero(ArgumentZero(vc))),1);

-

       PrepareCommon();

       string vcString = "(assert (not\n" + VCExpr2String(vc, 1) + "\n))";

       FlushAxioms();

@@ -462,7 +449,7 @@ namespace Microsoft.Boogie.SMTLib
     }

 

     private string[] CalculatePath() {

-      SendThisVC("(get-value ((ControlFlow " + controlFlowVariable + " 0)))");

+      SendThisVC("(get-value ((ControlFlow 0 0)))");

       var path = new List<string>();

       while (true) {

         var resp = Process.GetProverResponse();

@@ -484,7 +471,7 @@ namespace Microsoft.Boogie.SMTLib
         else {

           path.Add("+" + v);

         }

-        SendThisVC("(get-value ((ControlFlow " + controlFlowVariable + " " + v + ")))");

+        SendThisVC("(get-value ((ControlFlow 0 " + v + ")))");

       }

       return path.ToArray();

     }

diff --git a/Source/Provers/SMTLib/SMTLib.csproj b/Source/Provers/SMTLib/SMTLib.csproj
index f4cdbb14..3dc042a6 100644
--- a/Source/Provers/SMTLib/SMTLib.csproj
+++ b/Source/Provers/SMTLib/SMTLib.csproj
@@ -191,10 +191,6 @@
       <Project>{E1F10180-C7B9-4147-B51F-FA1B701966DC}</Project>

       <Name>VCGeneration</Name>

     </ProjectReference>

-    <ProjectReference Include="..\Simplify\Simplify.csproj">

-      <Project>{FEE9F01B-9722-4A76-A24B-72A4016DFA8E}</Project>

-      <Name>Simplify</Name>

-    </ProjectReference>

   </ItemGroup>

   <ItemGroup>

     <Folder Include="Properties\" />

diff --git a/Source/Provers/TPTP/TPTP.csproj b/Source/Provers/TPTP/TPTP.csproj
index 564b33f3..882d8009 100644
--- a/Source/Provers/TPTP/TPTP.csproj
+++ b/Source/Provers/TPTP/TPTP.csproj
@@ -116,10 +116,6 @@
       <Project>{E1F10180-C7B9-4147-B51F-FA1B701966DC}</Project>

       <Name>VCGeneration</Name>

     </ProjectReference>

-    <ProjectReference Include="..\Simplify\Simplify.csproj">

-      <Project>{FEE9F01B-9722-4A76-A24B-72A4016DFA8E}</Project>

-      <Name>Simplify</Name>

-    </ProjectReference>

   </ItemGroup>

   <ItemGroup>

     <Folder Include="Properties\" />

diff --git a/Source/Provers/Z3api/Z3api.csproj b/Source/Provers/Z3api/Z3api.csproj
index 94184957..7c481438 100644
--- a/Source/Provers/Z3api/Z3api.csproj
+++ b/Source/Provers/Z3api/Z3api.csproj
@@ -162,14 +162,6 @@
       <Project>{E1F10180-C7B9-4147-B51F-FA1B701966DC}</Project>

       <Name>VCGeneration</Name>

     </ProjectReference>

-    <ProjectReference Include="..\Simplify\Simplify.csproj">

-      <Project>{FEE9F01B-9722-4A76-A24B-72A4016DFA8E}</Project>

-      <Name>Simplify</Name>

-    </ProjectReference>

-    <ProjectReference Include="..\Z3\Z3.csproj">

-      <Project>{BB49B90B-BE21-4BE8-85BA-359FDB55F4DF}</Project>

-      <Name>Z3</Name>

-    </ProjectReference>

   </ItemGroup>

   <ItemGroup>

     <Compile Include="..\..\version.cs">

diff --git a/Source/VCGeneration/VC.cs b/Source/VCGeneration/VC.cs
index 49fa7144..1c0aeee8 100644
--- a/Source/VCGeneration/VC.cs
+++ b/Source/VCGeneration/VC.cs
@@ -607,8 +607,30 @@ namespace VC {
         Hashtable label2Absy;

         Checker ch = parent.FindCheckerFor(impl, CommandLineOptions.Clo.SmokeTimeout);

         Contract.Assert(ch != null);

-        VCExpr vc = parent.GenerateVC(impl, null, out label2Absy, ch);

+

+        Variable controlFlowVariable = null;

+        if (!CommandLineOptions.Clo.UseLabels) {

+          foreach (Variable v in impl.LocVars) {

+            if (v.Name == "@cfc") {

+              controlFlowVariable = v;

+              break;

+            }

+          }

+        }

+

+        VCExpr vc = parent.GenerateVC(impl, controlFlowVariable, out label2Absy, ch);

         Contract.Assert(vc != null);

+        

+        if (!CommandLineOptions.Clo.UseLabels) {

+          var ctx = ch.TheoremProver.Context;

+          var bet = ctx.BoogieExprTranslator;

+          VCExpr controlFlowVariableExpr = bet.LookupVariable(controlFlowVariable);

+          VCExpr eqExpr1 = ctx.ExprGen.Eq(controlFlowVariableExpr, ctx.ExprGen.Integer(BigNum.ZERO));

+          VCExpr controlFlowFunctionAppl = ctx.ExprGen.ControlFlowFunctionApplication(controlFlowVariableExpr, ctx.ExprGen.Integer(BigNum.ZERO));

+          VCExpr eqExpr2 = ctx.ExprGen.Eq(controlFlowFunctionAppl, ctx.ExprGen.Integer(BigNum.FromInt(impl.Blocks[0].UniqueId)));

+          vc = ctx.ExprGen.Implies(eqExpr1, ctx.ExprGen.Implies(eqExpr2, vc));

+        }

+

         impl.Blocks = backup;

 

         if (CommandLineOptions.Clo.TraceVerify) {

@@ -1537,7 +1559,6 @@ namespace VC {
 		  ));

 

         LocalVariable controlFlowVariable = null;

-

         if (!CommandLineOptions.Clo.UseLabels) {

           controlFlowVariable = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, "@cfc", Microsoft.Boogie.Type.Int));

           impl.LocVars.Add(controlFlowVariable);

@@ -1548,10 +1569,10 @@ namespace VC {
 

         if (!CommandLineOptions.Clo.UseLabels) {

           VCExpr controlFlowVariableExpr = bet.LookupVariable(controlFlowVariable);

-          Contract.Assert(controlFlowVariableExpr != null);

+          VCExpr eqExpr1 = ctx.ExprGen.Eq(controlFlowVariableExpr, ctx.ExprGen.Integer(BigNum.ZERO));

           VCExpr controlFlowFunctionAppl = ctx.ExprGen.ControlFlowFunctionApplication(controlFlowVariableExpr, ctx.ExprGen.Integer(BigNum.ZERO));

-          Contract.Assert(controlFlowFunctionAppl != null);

-          vc = ctx.ExprGen.Implies(ctx.ExprGen.Eq(controlFlowFunctionAppl, ctx.ExprGen.Integer(BigNum.FromInt(impl.Blocks[0].UniqueId))), vc);

+          VCExpr eqExpr2 = ctx.ExprGen.Eq(controlFlowFunctionAppl, ctx.ExprGen.Integer(BigNum.FromInt(impl.Blocks[0].UniqueId)));

+          vc = ctx.ExprGen.Implies(eqExpr1, ctx.ExprGen.Implies(eqExpr2, vc));

         }

         

         if (CommandLineOptions.Clo.vcVariety == CommandLineOptions.VCVariety.Local) {

@@ -1667,7 +1688,7 @@ namespace VC {
           break;

         case CommandLineOptions.VCVariety.Dag:

           if (cce.NonNull(CommandLineOptions.Clo.TheProverFactory).SupportsDags) {

-            vc = DagVC(cce.NonNull(impl.Blocks[0]), label2absy, new Hashtable/*<Block, VCExpr!>*/(), ch.TheoremProver.Context, out assertionCount);

+            vc = DagVC(cce.NonNull(impl.Blocks[0]), controlFlowVariable, label2absy, new Hashtable/*<Block, VCExpr!>*/(), ch.TheoremProver.Context, out assertionCount);

           } else {

             vc = LetVC(cce.NonNull(impl.Blocks[0]), controlFlowVariable, label2absy, ch.TheoremProver.Context, out assertionCount);

           }

@@ -3593,6 +3614,7 @@ namespace VC {
     }

 

     static VCExpr DagVC(Block block,

+                         Variable controlFlowVariable,

                          Hashtable/*<int, Absy!>*/ label2absy,

                          Hashtable/*<Block, VCExpr!>*/ blockEquations,

                          ProverContext proverCtxt,

@@ -3623,8 +3645,14 @@ namespace VC {
         foreach (Block successor in cce.NonNull(gotocmd.labelTargets)) {

           Contract.Assert(successor != null);

           int ac;

-          VCExpr c = DagVC(successor, label2absy, blockEquations, proverCtxt, out ac);

+          VCExpr c = DagVC(successor, controlFlowVariable, label2absy, blockEquations, proverCtxt, out ac);

           assertionCount += ac;

+          if (controlFlowVariable != null) {

+            VCExprVar controlFlowVariableExpr = proverCtxt.BoogieExprTranslator.LookupVariable(controlFlowVariable);

+            VCExpr controlFlowFunctionAppl = gen.ControlFlowFunctionApplication(controlFlowVariableExpr, gen.Integer(BigNum.FromInt(block.UniqueId)));

+            VCExpr controlTransferExpr = gen.Eq(controlFlowFunctionAppl, gen.Integer(BigNum.FromInt(successor.UniqueId)));

+            c = gen.Implies(controlTransferExpr, c);

+          }  

           SuccCorrect = SuccCorrect == null ? c : gen.And(SuccCorrect, c);

         }

       }

@@ -3632,7 +3660,7 @@ namespace VC {
         SuccCorrect = VCExpressionGenerator.True;

       }

 

-      VCContext context = new VCContext(label2absy, proverCtxt);

+      VCContext context = new VCContext(label2absy, proverCtxt, controlFlowVariable);

       vc = Wlp.Block(block, SuccCorrect, context);

       assertionCount += context.AssertionCount;