Bad code generation when dereferencing directly a rc_copy_alloc_id

The following example fails https://gitlab.mpi-sws.org/iris/refinedc/-/blob/master/examples/intptr.c#L68.

I tried fixing code generation with a hack, changing

let (e2, l2) = translate_expr lval None e2 in
let (e3, l3) = translate_expr lval None e3 in
(locate (CopyAID(e3, e2)), l2 @ l3)

into

let (e2, l2) = translate_expr false None e2 in
let (e3, l3) = translate_expr false None e3 in
let e = locate (CopyAID(e3, e2)) in
let e = if lval then locate (Deref(false, LPtr, e)) else e in
(e, l2 @ l3)

but with that the automation still gets stuck. In fact, there might also be a problem there, I'm not sure. You end up with a read rule with a term of the form !{LPtr} (CopyAID ...). Clearly, this is again a LValue versus RValue problem, but I can't find how to solve it. Any idea?