#2598 is using cv5 in Lists.hs because z3 takes very long to reply some queries. We need to minimize the example and send a bug report to z3. https://github.com/ucsd-progsys/liquid-fixpoint/pull/815 discusses how this behavior was first noticed.