Slightly better management of outermost Push-Pop and FlushAxioms

1 files changed, 8 insertions, 3 deletions

diff --git a/Source/VCGeneration/StratifiedVC.cs b/Source/VCGeneration/StratifiedVC.cs
index f3a7e27e..ad83b7fe 100644
--- a/Source/VCGeneration/StratifiedVC.cs
+++ b/Source/VCGeneration/StratifiedVC.cs
@@ -1282,6 +1282,9 @@ namespace VC
             // Record current time

             var startTime = DateTime.UtcNow;

 

+            // Flush any axioms that came with the program before we start SI on this implementation

+            prover.AssertAxioms();

+

             // Run live variable analysis

             if (CommandLineOptions.Clo.LiveVariableAnalysis == 2)

             {

@@ -1308,6 +1311,11 @@ namespace VC
             var coverageManager = new CoverageGraphManager(calls);

             coverageManager.addMain();

 

+

+            // We'll restore the original state of the theorem prover at the end

+            // of this procedure

+            prover.Push();

+

             // Put all of the necessary state into one object

             var vState = new VerificationState(vc, calls, prover, reporter, prover2, new EmptyErrorHandler());

             vState.vcSize += SizeComputingVisitor.ComputeSize(vc);

@@ -1315,9 +1323,6 @@ namespace VC
 

             if (useSummary) summaryComputation = new SummaryComputation(vState, computeUnderBound);

 

-            // We'll restore the original state of the theorem prover at the end

-            // of this procedure

-            vState.checker.prover.Push();

 

             Outcome ret = Outcome.ReachedBound;