From d64c8100bb116615cccbdd96f51356c6119c4bdb Mon Sep 17 00:00:00 2001 From: Lea Salome Brugger Date: Wed, 10 Jul 2024 14:30:57 +0200 Subject: [PATCH] Revert "Remove unnecessary parentheses" This reverts commit aee8e5378d1718e51c98a6a6c164e907241d59fc. --- .../translator/encodings/closures/ClosureSpecsEncoder.scala | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/main/scala/viper/gobra/translator/encodings/closures/ClosureSpecsEncoder.scala b/src/main/scala/viper/gobra/translator/encodings/closures/ClosureSpecsEncoder.scala index a1b665952..4a94e9d59 100644 --- a/src/main/scala/viper/gobra/translator/encodings/closures/ClosureSpecsEncoder.scala +++ b/src/main/scala/viper/gobra/translator/encodings/closures/ClosureSpecsEncoder.scala @@ -314,7 +314,7 @@ protected class ClosureSpecsEncoder { private var implementAssertionSpecOriginToStr: Map[Source.AbstractOrigin, String] = Map.empty private def doesNotImplementSpecErr(callNode: vpr.Node with vpr.Positioned, closureStr: String): ErrorTransformer = { - case e@vprerr.PreconditionInCallFalse(Source(info), reasons.AssertionFalse(Source(assInfo)), _) if e causedBy callNode && implementAssertionSpecOriginToStr.contains(assInfo.origin) => + case e@vprerr.PreconditionInCallFalse(Source(info), reasons.AssertionFalse(Source(assInfo)), _) if (e causedBy callNode) && implementAssertionSpecOriginToStr.contains(assInfo.origin) => PreconditionError(info).dueTo(SpecNotImplementedByClosure(info, closureStr, implementAssertionSpecOriginToStr(assInfo.origin))) case e@vprerr.PreconditionInAppFalse(Source(info), reasons.AssertionFalse(Source(assInfo)), _) if (e causedBy callNode) && implementAssertionSpecOriginToStr.contains(assInfo.origin) => PreconditionError(info).dueTo(SpecNotImplementedByClosure(info, closureStr, implementAssertionSpecOriginToStr(assInfo.origin)))