fix a few tests

viperproject · Jul 2, 2024 · 0b7faf0 · 0b7faf0
1 parent fc2f804
commit 0b7faf0
Showing 1 changed file with 2 additions and 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
@@ -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