Makes sense. Advanced ACL analyzers translate them into first order logic and then use something like Z3 to find the packets that satisfy them but they rarely support the time based ACLs. But those are not used much in practice.