From d99531ab9121e39c2b1261e649e38b51765fcdb7 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Tam=C3=A1s=20T=C3=B3th?= Date: Fri, 29 Nov 2024 20:50:30 +0000 Subject: [PATCH] Strengthen pattern --- pyk/src/pyk/kore/rule.py | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/pyk/src/pyk/kore/rule.py b/pyk/src/pyk/kore/rule.py index e7349b06f0f..2d218a65050 100644 --- a/pyk/src/pyk/kore/rule.py +++ b/pyk/src/pyk/kore/rule.py @@ -5,7 +5,7 @@ from typing import TYPE_CHECKING, final from .prelude import inj -from .syntax import And, App, Axiom, Ceil, Equals, EVar, Implies, In, Not, Rewrites, SortVar, String, Top +from .syntax import DV, And, App, Axiom, Ceil, Equals, EVar, Implies, In, Not, Rewrites, SortApp, SortVar, String, Top if TYPE_CHECKING: from typing import Final @@ -232,7 +232,7 @@ def _extract_condition(pattern: Pattern) -> Pattern | None: match pattern: case Top(): return None - case Equals(left=cond): + case Equals(left=cond, right=DV(SortApp('SortBool'), String('true'))): return cond case _: raise ValueError(f'Cannot extract condition from pattern: {pattern.text}')