From fc196de27a54c5d1f83afda43bcedc4bfa18010f Mon Sep 17 00:00:00 2001 From: Unknown Date: Wed, 2 May 2012 14:30:26 +0530 Subject: Slightly better management of outermost Push-Pop and FlushAxioms --- Source/VCGeneration/StratifiedVC.cs | 11 ++++++++--- 1 file changed, 8 insertions(+), 3 deletions(-) (limited to 'Source/VCGeneration/StratifiedVC.cs') 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; -- cgit v1.2.3