CURRENT_TIMESTAMP is truly random. One thing we can do is to over approximate. For example, let CURRENT_TIMESTAMP be a symbolic variable, which essentially can be any value. If we still can prove the equivalence, then the equivalence is sound. But there might be some false negative.

ROWNUM is interesting. You can actually declare ROWNUM as an extra attribute of the table and then assert it is a key (We will add support of key constraints very soon). Then many cases will be covered.