From 030cc13d5cc3313f1dbb98701a43a52153e121b5 Mon Sep 17 00:00:00 2001 From: Marco Eilers Date: Sun, 10 Mar 2024 22:17:22 +0100 Subject: [PATCH] Discard empty triggers and partially evaluated ones --- src/main/scala/rules/Evaluator.scala | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/main/scala/rules/Evaluator.scala b/src/main/scala/rules/Evaluator.scala index 646798aaa..49b0d0395 100644 --- a/src/main/scala/rules/Evaluator.scala +++ b/src/main/scala/rules/Evaluator.scala @@ -1287,7 +1287,7 @@ object evaluator extends EvaluationRules { * incompletenesses because the corresponding quantifiers will not be triggered. */ - Q(s1, tTriggersSets map Trigger, v1)}) + Q(s1, tTriggersSets.filter(_.nonEmpty) map Trigger, v1)}) } /** Evaluates the given list of trigger sets `eTriggerSets` (expressions) and passes the result @@ -1404,7 +1404,7 @@ object evaluator extends EvaluationRules { for (e <- remainingTriggerExpressions) v.reporter.report(WarningsDuringVerification(Seq( VerifierWarning(s"Might not be able to use trigger $e, since it is not evaluated while evaluating the body of the quantifier", e.pos)))) - Q(s, cachedTriggerTerms, v) + Q(s, Seq(), v) } }