Enforce priority to be non-negative

runtimeverification · Jan 17, 2025 · 1ffb465 · 1ffb465
1 parent 901b3bf
commit 1ffb465
Showing 1 changed file with 2 additions and 0 deletions.
diff --git a/pyk/src/pyk/k2lean4/model.py b/pyk/src/pyk/k2lean4/model.py
@@ -136,6 +136,8 @@ def __init__(
         ident: str | DeclId | None = None,
         modifiers: Modifiers | None = None,
     ):
+        if priority and priority < 0:
+            raise ValueError('Priority must be non-negative')
         if not signature.ty:
             # TODO refine type to avoid this check
             raise ValueError('Missing type from signature')