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.