Skip to content

Commit

Permalink
Fixing incorrect shortcut. If the check returns false, that does not …
Browse files Browse the repository at this point in the history
…actually meann that the arguments are not equal, so the else was incorrect.
  • Loading branch information
marcoeilers committed Jan 8, 2025
1 parent 438bb97 commit 2265e14
Showing 1 changed file with 2 additions and 3 deletions.
5 changes: 2 additions & 3 deletions src/main/scala/rules/MoreCompleteExhaleSupporter.scala
Original file line number Diff line number Diff line change
Expand Up @@ -165,10 +165,9 @@ object moreCompleteExhaleSupporter extends SymbolicExecutionRules {
// the counterexample might be wrong.
if (relevantChunks.size == 1 && !Verifier.config.counterexample.isDefined) {
val chunk = relevantChunks.head
if (v.decider.check(And(chunk.args.zip(args).map { case (t1, t2) => t1 === t2 }), Verifier.config.checkTimeout())) {
val argsEqual = And(chunk.args.zip(args).map { case (t1, t2) => t1 === t2 })
if (v.decider.check(argsEqual, Verifier.config.checkTimeout())) {
return Q(s, chunk.snap, chunk.perm, chunk.permExp, v)
} else {
return Q(s, chunk.snap, NoPerm, Option.when(withExp)(ast.NoPerm()()), v)
}
}

Expand Down

0 comments on commit 2265e14

Please sign in to comment.