Reference-typed `RefCell` access and reference constants prevent verification of a simple division-by-zero case

[lynae99]

Prusti rejects a simple program that should be analyzable as a straightforward division-by-zero case when the dividend is obtained from RefCell<&u64> and the argument is initialized with a reference constant. Instead of verifying the arithmetic behavior, Prusti reports unsupported-feature errors for both the reference-typed field access and the reference constant.
Reproduction

fn test(x: std::cell::RefCell<&u64>, y: u64) -> u64 {
    let x = **x.borrow();
    x / y
}

fn main() {
    test(std::cell::RefCell::from(&(1)), 0);
}

Actual Behavior
Prusti reports the following errors:

1. error: [Prusti: unsupported feature] access to reference-typed fields is not supported
2. error: [Prusti: unsupported feature] unsupported constant type &'?5 u64

Expected Behavior
Prusti should ideally support this pattern, or lower it into an equivalent supported form, so that verification can proceed to the semantically relevant arithmetic check.
In this example, the important verification outcome is that x / y may divide by zero when y == 0. The use of RefCell<&u64> and &(1) should not by themselves block analysis.
Notes
This example combines two currently unsupported features:

• accessing a reference value stored inside RefCell
• passing a reference to a literal constant such as &(1)

Because of these unsupported-feature errors, Prusti cannot reach the underlying arithmetic verification scenario.