From 7130b71c376274cb57ff5bc047d4e876c73cac88 Mon Sep 17 00:00:00 2001 From: gauravpartha Date: Mon, 8 Nov 2021 21:58:51 +0100 Subject: [PATCH] fix issue 381 (existentials in function body) --- .../viper/carbon/modules/impls/DefaultFuncPredModule.scala | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/main/scala/viper/carbon/modules/impls/DefaultFuncPredModule.scala b/src/main/scala/viper/carbon/modules/impls/DefaultFuncPredModule.scala index 928d1131..441f84bc 100644 --- a/src/main/scala/viper/carbon/modules/impls/DefaultFuncPredModule.scala +++ b/src/main/scala/viper/carbon/modules/impls/DefaultFuncPredModule.scala @@ -335,7 +335,8 @@ with DefinednessComponent with ExhaleComponent with InhaleComponent { } else Some(FuncApp(Identifier(recf.name + limitedPostfix), recargs map (_.transform(transformer)), t)) - case fa@Forall(vs,ts,e,tvs) => Some(Forall(vs,ts,e.transform(transformer),tvs)) // avoid recursing into the triggers of nested foralls (which will typically get translated via another call to this anyway) + case Forall(vs,ts,e,tvs) => Some(Forall(vs,ts,e.transform(transformer),tvs)) // avoid recursing into the triggers of nested foralls (which will typically get translated via another call to this anyway) + case Exists(vs,ts,e) => Some(Exists(vs,ts,e.transform(transformer))) // avoid recursing into the triggers of nested exists (which will typically get translated via another call to this anyway) } val res = exp transform transformer res