SMT-Based Satisfiability of First-Order LTL with Event Freezing Functions and Metric Operators