Minor additions to z3api

1 files changed, 17 insertions, 0 deletions

diff --git a/Source/Provers/Z3api/ProverLayer.cs b/Source/Provers/Z3api/ProverLayer.cs
index 8d0c8aeb..6d26edd2 100644
--- a/Source/Provers/Z3api/ProverLayer.cs
+++ b/Source/Provers/Z3api/ProverLayer.cs
@@ -28,6 +28,7 @@ namespace Microsoft.Boogie.Z3
             this.options = opts;

             this.context = (Z3apiProverContext) ctxt;

             this.z3ContextIsUsed = false;

+            this.numAxiomsPushed = 0;

         }

 

         private Z3InstanceOptions options;

@@ -43,6 +44,8 @@ namespace Microsoft.Boogie.Z3
             get { return context.ExprGen; }

         }

 

+        private int numAxiomsPushed;

+

         public override void Close()

         {

             base.Close();

@@ -84,6 +87,7 @@ namespace Microsoft.Boogie.Z3
         public override void PushVCExpression(VCExpr vc)

         {

             PushAxiom(vc);

+            numAxiomsPushed++;

         }

 

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

@@ -135,6 +139,19 @@ namespace Microsoft.Boogie.Z3
             cm.Backtrack();

         }

 

+        // Number of axioms pushed since the last call to FlushAxioms

+        public override int NumAxiomsPushed()

+        {

+            return numAxiomsPushed;

+        }

+

+        public override int FlushAxiomsToTheoremProver()

+        {

+            var ret = numAxiomsPushed;

+            numAxiomsPushed = 0;

+            return ret;

+        }

+

         private List<string> RemovePrefixes(List<string> labels)

         {

             List<string> result = new List<string>();