diff --git a/src/main/scala/leon/verification/AnalysisPhase.scala b/src/main/scala/leon/verification/AnalysisPhase.scala index ce65a93bfe16269bb91b382429cc9197343cdb60..dbaa76433c0fb2c6cafaa3cf0c3947feb4b5b7dd 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...")