From 8b0392fe672ce820ba07af673fe9177babdee00b Mon Sep 17 00:00:00 2001
From: akashlal <unknown>
Date: Thu, 26 Aug 2010 14:49:43 +0000
Subject: Minor additions to z3api

---
 Source/Provers/Z3api/ProverLayer.cs | 17 +++++++++++++++++
 1 file changed, 17 insertions(+)

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>();
-- 
cgit v1.2.3