Skip to content

Commit

Permalink
Only return a model if the config requests it
Browse files Browse the repository at this point in the history
  • Loading branch information
sankalpgambhir committed Sep 24, 2024
1 parent 9bf9546 commit b63317e
Showing 1 changed file with 3 additions and 1 deletion.
4 changes: 3 additions & 1 deletion src/main/scala/inox/solvers/invariant/InvariantSolver.scala
Original file line number Diff line number Diff line change
Expand Up @@ -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

Expand Down

0 comments on commit b63317e

Please sign in to comment.