fixed z3api so that it works on small examples now.

1 files changed, 12 insertions, 0 deletions

diff --git a/Source/Provers/Z3api/ProverLayer.cs b/Source/Provers/Z3api/ProverLayer.cs
index f3dfab69..7c41f25c 100644
--- a/Source/Provers/Z3api/ProverLayer.cs
+++ b/Source/Provers/Z3api/ProverLayer.cs
@@ -30,6 +30,12 @@ namespace Microsoft.Boogie.Z3
             this.z3ContextIsUsed = false;

         }

 

+        public override void Close()

+        {

+            base.Close();

+            ((Z3apiProverContext)Context).cm.z3.Dispose();

+            ((Z3apiProverContext)Context).cm.config.Config.Dispose();

+        }

         private bool z3ContextIsUsed;

 

         public void PushAxiom(VCExpr axiom)

@@ -39,6 +45,7 @@ namespace Microsoft.Boogie.Z3
             LineariserOptions linOptions = new Z3LineariserOptions(false, (Z3InstanceOptions)this.options, new List<VCExprVar>());

             cm.AddAxiom((VCExpr)axiom, linOptions);

         }

+

         private void PushConjecture(VCExpr conjecture)

         {

             Z3SafeContext cm = ((Z3apiProverContext)ctx).cm;

@@ -60,6 +67,11 @@ namespace Microsoft.Boogie.Z3
             outcome = cm.Check(out z3LabelModels);

         }

 

+        public override void PushVCExpression(VCExpr vc)

+        {

+            PushAxiom(vc);

+        }

+

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

         {

             LineariserOptions linOptions = new Z3LineariserOptions(false, (Z3InstanceOptions)this.options, new List<VCExprVar>());