some set helpers and temporal operators

philzook58 · Jan 26, 2025 · 1cf7045 · 1cf7045
1 parent 5f4002d
commit 1cf7045
Showing 1 changed file with 1 addition and 0 deletions.
diff --git a/kdrag/theories/logic/temporal.py b/kdrag/theories/logic/temporal.py
@@ -20,6 +20,7 @@ def res(x, y):
             y1 = TLift(y1)
             if y1.sort() != S:
                 raise TypeError(f"{y} but expected sort {S}")
+        assert isinstance(y1, smt.DatatypeRef)
         t = smt.FreshInt("t")
         return S(smt.Lambda([t], op(x.val[t], y1.val[t])))