further fixes related to using uninterpreted function for error traces

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

3 files changed, 5 insertions, 20 deletions

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>