Add SMT pattern to find_event_triggered_at_timestamp (Klaas remark)

REPROSEC · Oct 14, 2024 · 2153663 · 2153663
1 parent 6cdd01c
commit 2153663
Show file tree

Hide file tree

Showing 2 changed files with 8 additions and 0 deletions.
diff --git a/src/core/DY.Core.Trace.Base.fst b/src/core/DY.Core.Trace.Base.fst
@@ -360,6 +360,10 @@ val find_event_triggered_at_timestamp_later:
     tr1 <$ tr2
   )
   (ensures find_event_triggered_at_timestamp tr1 prin tag content == find_event_triggered_at_timestamp tr2 prin tag content)
+  [SMTPat (find_event_triggered_at_timestamp tr1 prin tag content);
+   SMTPat (find_event_triggered_at_timestamp tr2 prin tag content);
+   SMTPat (tr1 <$ tr2)
+  ]
 let rec find_event_triggered_at_timestamp_later #label_t tr1 tr2 prin tag content =
   if length tr1 = length tr2 then ()
   else (

diff --git a/src/lib/event/DY.Lib.Event.Typed.fst b/src/lib/event/DY.Lib.Event.Typed.fst
@@ -235,6 +235,10 @@ val find_event_triggered_at_timestamp_later:
     tr1 <$ tr2
   )
   (ensures find_event_triggered_at_timestamp tr1 prin content == find_event_triggered_at_timestamp tr2 prin content)
+  [SMTPat (find_event_triggered_at_timestamp tr1 prin content);
+   SMTPat (find_event_triggered_at_timestamp tr2 prin content);
+   SMTPat (tr1 <$ tr2)
+  ]
 let find_event_triggered_at_timestamp_later #a #ev_a tr1 tr2 prin content =
   reveal_opaque (`%find_event_triggered_at_timestamp) (find_event_triggered_at_timestamp #a);
   DY.Core.find_event_triggered_at_timestamp_later tr1 tr2 prin ev_a.tag (serialize a content)