From 867e7f53616a31d2204d19e9133783a5a5861a06 Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <ekneuss@gmail.com>
Date: Wed, 27 May 2015 18:38:21 +0200
Subject: [PATCH] Free the solver we get when checking if we are in
SMT-quantified
---
src/main/scala/leon/verification/AnalysisPhase.scala | 9 ++++++++-
1 file changed, 8 insertions(+), 1 deletion(-)
diff --git a/src/main/scala/leon/verification/AnalysisPhase.scala b/src/main/scala/leon/verification/AnalysisPhase.scala
index ce65a93bf..dbaa76433 100644
--- a/src/main/scala/leon/verification/AnalysisPhase.scala
+++ b/src/main/scala/leon/verification/AnalysisPhase.scala
@@ -33,12 +33,19 @@ object AnalysisPhase extends LeonPhase[Program,VerificationReport] {
baseSolverF
}
+ val isSMTQuantified = {
+ val solver = baseSolverF.getNewSolver
+ val res = solver.isInstanceOf[SMTLIBCVC4QuantifiedSolver]
+ solver.free
+ res
+ }
+
val vctx = VerificationContext(ctx, program, solverF, reporter)
reporter.debug("Generating Verification Conditions...")
try {
- val vcs = generateVCs(vctx, filterFuns, forceGrouped = baseSolverF.getNewSolver.isInstanceOf[SMTLIBCVC4QuantifiedSolver])
+ val vcs = generateVCs(vctx, filterFuns, forceGrouped = isSMTQuantified)
reporter.debug("Checking Verification Conditions...")
--
GitLab