From 0b7faf06e02ffdc7181ef53d02148314d55f6e48 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=A3o=20Pereira?= Date: Tue, 2 Jul 2024 14:18:59 +0200 Subject: [PATCH] fix a few tests --- .../info/implementation/typing/ghost/GhostExprTyping.scala | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/main/scala/viper/gobra/frontend/info/implementation/typing/ghost/GhostExprTyping.scala b/src/main/scala/viper/gobra/frontend/info/implementation/typing/ghost/GhostExprTyping.scala index b1d2327f4..2f2a04d60 100644 --- a/src/main/scala/viper/gobra/frontend/info/implementation/typing/ghost/GhostExprTyping.scala +++ b/src/main/scala/viper/gobra/frontend/info/implementation/typing/ghost/GhostExprTyping.scala @@ -45,8 +45,8 @@ trait GhostExprTyping extends BaseTyping { this: TypeInfoImpl => assignableTo.errors(exprType(cond), BooleanT)(expr) ++ // check that `thn` and `els` have a common type mergeableTypes.errors(exprType(thn), exprType(els))(expr) ++ - // check that all subexpressions are pure - isPureExpr(cond) ++ isPureExpr(thn) ++ isPureExpr(els) + // check that all subexpressions are pure. + isPureExpr(cond) ++ isWeaklyPureExpr(thn) ++ isWeaklyPureExpr(els) case n@PForall(vars, triggers, body) => // check whether all triggers are valid and consistent