Spurious statements when extracting to C
When extracted to C, file multiprecision/sqrtrem.mlw
produces spurious statements such as
res = wmpn_rshift(nr, nx, l, UINT64_C(1));
IGNORE2(sp,scratch);
res; // <- HERE
This comes from
let ghost r = wmpn_rshift_sep sp scratch l 1 in
This might be caused by an interaction between ghost results and function inlining.