Doing bitvector work in cvc5 puts the solver in a broken state

[fosslinux]

When using the cvc5 solver with Silicon, performing bitvector operations by converting to and from integers somehow appears to put the solver in some kind of broken state, in which it gets stuck proving obviously true statements. It does not fail, but just keeps attempting to prove indefinitely. This does not occur with the Z3 solver.

This is the most minimal example I've managed to come up with.

domain BitVectorDomain64 interpretation (SMTLIB: "(_ BitVec 64)") {
  function bv_op(a: BitVectorDomain64, b: BitVectorDomain64): BitVectorDomain64// interpretation "bvand"
  function bv64_add(a: BitVectorDomain64, b: BitVectorDomain64): BitVectorDomain64
  function bv64_from_int(i: Int): BitVectorDomain64 interpretation "(_ int2bv 64)"
  function bv64_to_int(i: BitVectorDomain64): Int interpretation "ubv_to_int" // note this is the SMT instruction for cvc5; for older versions of Z3, this should be (_ bv2int 64)
}

method m()
function f(): Bool {true}

method fail(a: Int, b: Int)
  requires a == 1 || a == 2
  requires b == 1 || b == 2
{
  // any bitvector operation fails
  var c: Int := bv64_to_int(bv64_add(bv64_from_int(a), bv64_from_int(b)))
  if (c == 0) {
    m()
    assert f() // can be placed inside or outside the if
  }
}

Some notes:

• I suspect that this has something to do with the solver finding the bitvector reasoning difficult, and that somehow overloading the solver. I wouldn't expect the solver to be able to eliminate the c == 0 branch, and indeed, if you change a == 1 and b == 1 to a == 0 and b == 0, the same behaviour is observed. The preconditions on a and b must be non-trivial, in particular, something like requires a == 1 does not fail.
• The method call is somehow load-bearing.