Boogie: Repaired a reentrancy error in Z3/Simplify.

3 files changed, 10 insertions, 9 deletions

diff --git a/Source/BoogieDriver/BoogieDriver.csproj b/Source/BoogieDriver/BoogieDriver.csproj
index 4c3efb52..c87c8fa4 100644
--- a/Source/BoogieDriver/BoogieDriver.csproj
+++ b/Source/BoogieDriver/BoogieDriver.csproj
@@ -87,10 +87,6 @@
     </Reference>

     <Reference Include="System.Data" />

     <Reference Include="System.Xml" />

-    <Reference Include="Z3, Version=0.0.0.0, Culture=neutral, processorArchitecture=MSIL">

-      <SpecificVersion>False</SpecificVersion>

-      <HintPath>..\Provers\Z3\bin\Debug\Z3.dll</HintPath>

-    </Reference>

   </ItemGroup>

   <ItemGroup>

     <Compile Include="BoogieDriver.cs" />

@@ -125,6 +121,10 @@
       <Project>{13C3A68C-462A-4CDA-A480-738046E37C5A}</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.sscproj">

       <Project>{CF42B700-10AA-4DA9-8992-48A800251C11}</Project>

       <Name>VCExpr</Name>

diff --git a/Source/Provers/Simplify/ProverInterface.ssc b/Source/Provers/Simplify/ProverInterface.ssc
index 2a50adee..dbd3ac19 100644
--- a/Source/Provers/Simplify/ProverInterface.ssc
+++ b/Source/Provers/Simplify/ProverInterface.ssc
@@ -154,7 +154,7 @@ namespace Microsoft.Boogie.Simplify
       return (AxiomVCExprTranslator!)ctx.exprTranslator;

     } }

 

-    protected abstract AxiomVCExprTranslator! SpawnVCExprTranslator();

+    protected abstract AxiomVCExprTranslator! SpawnVCExprTranslator(ProverOptions! p);

 

     // Return the number of axioms pushed to the theorem prover

     protected int FeedNewAxiomsDecls2Prover() throws UnexpectedProverOutputException; {

@@ -264,7 +264,7 @@ namespace Microsoft.Boogie.Simplify
       // if none exists so far, we have to create a new one

       // from scratch and feed the axioms to it

       if (ctx.exprTranslator == null) {

-        AxiomVCExprTranslator tl = SpawnVCExprTranslator();

+        AxiomVCExprTranslator tl = SpawnVCExprTranslator(options);

         ctx.exprTranslator = tl;

         tl.AddAxiom(tl.translate(ctx.Axioms, -1));

         // we clear the lists with new axioms and declarations;

@@ -541,7 +541,7 @@ namespace Microsoft.Boogie.Simplify
       return new SimplifyProverProcess(proverPath);

     }

 

-    protected override AxiomVCExprTranslator! SpawnVCExprTranslator() {

+    protected override AxiomVCExprTranslator! SpawnVCExprTranslator(ProverOptions! opts) {

       return new SimplifyVCExprTranslator(gen);

     }

   }

diff --git a/Source/Provers/Z3/ProverInterface.cs b/Source/Provers/Z3/ProverInterface.cs
index 824dabd4..994cb282 100644
--- a/Source/Provers/Z3/ProverInterface.cs
+++ b/Source/Provers/Z3/ProverInterface.cs
@@ -65,10 +65,11 @@ void ObjectInvariant()
       return new Z3ProverProcess(opts, inspector);

     }

 

-    protected override AxiomVCExprTranslator SpawnVCExprTranslator() {

+    protected override AxiomVCExprTranslator SpawnVCExprTranslator(ProverOptions opts) {

+      Contract.Requires(opts != null);

       Contract.Ensures(Contract.Result<AxiomVCExprTranslator>() != null);

 

-      return new Z3VCExprTranslator(gen, opts);

+      return new Z3VCExprTranslator(gen, (Z3InstanceOptions) opts);

     }

 

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