QordTrans theorem hangs when using cvc5

[danmatichuk]

In tests/regression/rational_properties.cry the following theorem:

property QordTrans (x : Rational) (y : Rational) (z : Rational) =
  x < y ==> y < z ==> x < z

Is expected to return "Unknown" when using cvc4, and then successfully proven with z3.

If the solver is changed to cvc5 the solver instead just hangs indefinitely. Attached is the relevant smt interaction.

Note: If manually invoked, passing --rlimit=190000 to cvc5 will successfully return unknown.

QordTrans.log

[RyanGlScott]

I like the idea of converting this test over to using CVC5 eventually (especially in light of #1806). It's unfortunate that cvc5 just hangs on this, and I'm not sure what ramifications there would be in changing the default rlimit setting.

One alternative would be to set a proverTimeout when proving these properties using cvc5 so that they time out instead of hanging forever. In order to do so, we would need to fix either #1807 or #1808 first, as they currently block proverTimeout support with respect to cvc5.