Remvoe accidental result-flipping in previous change

epfl-lara · Sep 17, 2024 · 7e1e98c · 7e1e98c
1 parent 96a02ab
commit 7e1e98c
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/src/main/scala/inox/solvers/invariant/InvariantSolver.scala b/src/main/scala/inox/solvers/invariant/InvariantSolver.scala
@@ -846,7 +846,7 @@ abstract class AbstractInvariantSolver(override val program: Program,
           reportInvariants(model)
           // discard underlying model. We cannot construct a program model (cex) from
           // the Horn model 
-          config.cast(SolverResponses.SatWithModel(emptyProgramModel))
+          config.cast(SolverResponses.Unsat)
 
         case SolverResponses.Check(r) => config.cast(if r then SolverResponses.Unsat else SolverResponses.SatWithModel(emptyProgramModel))