Skip to content
Snippets Groups Projects
Commit 867e7f53 authored by Etienne Kneuss's avatar Etienne Kneuss
Browse files

Free the solver we get when checking if we are in SMT-quantified

parent 4150a2a9
Branches
Tags
No related merge requests found
......@@ -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...")
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment