From 2265e1459760a5af121fa7eb01d5847c45ccfd78 Mon Sep 17 00:00:00 2001 From: marcoeilers Date: Wed, 8 Jan 2025 15:33:38 +0100 Subject: [PATCH] Fixing incorrect shortcut. If the check returns false, that does not actually meann that the arguments are not equal, so the else was incorrect. --- src/main/scala/rules/MoreCompleteExhaleSupporter.scala | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/src/main/scala/rules/MoreCompleteExhaleSupporter.scala b/src/main/scala/rules/MoreCompleteExhaleSupporter.scala index c7292f53..9f94d8a2 100644 --- a/src/main/scala/rules/MoreCompleteExhaleSupporter.scala +++ b/src/main/scala/rules/MoreCompleteExhaleSupporter.scala @@ -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) } }