From b63317eee7d877c68b76b253ee2fe511a08f452e Mon Sep 17 00:00:00 2001 From: Sankalp Gambhir Date: Tue, 24 Sep 2024 08:50:30 +0200 Subject: [PATCH] Only return a model if the config requests it --- src/main/scala/inox/solvers/invariant/InvariantSolver.scala | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/src/main/scala/inox/solvers/invariant/InvariantSolver.scala b/src/main/scala/inox/solvers/invariant/InvariantSolver.scala index 6edb5db74..5674d9937 100644 --- a/src/main/scala/inox/solvers/invariant/InvariantSolver.scala +++ b/src/main/scala/inox/solvers/invariant/InvariantSolver.scala @@ -848,7 +848,9 @@ abstract class AbstractInvariantSolver(override val program: Program, // the Horn model config.cast(SolverResponses.Unsat) - case SolverResponses.Check(r) => config.cast(if r then SolverResponses.Unsat else SolverResponses.SatWithModel(emptyProgramModel)) + case SolverResponses.Check(r) => + lazy val satRes = if config.withModel then SolverResponses.SatWithModel(emptyProgramModel) else SolverResponses.Sat + config.cast(if r then SolverResponses.Unsat else satRes) case _ => config.cast(SolverResponses.Unknown) // unknown or unreachable