Incorrect extraction on loop with copy

[ayhon]

MWE:

fn bar(a: &mut bool) { }
fn foo(s: &mut bool) {
    let mut a = *s;
    while 0 < 0 {
        bar(&mut a);
    }
    *s = a;
}

This code is extracted to

-- THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS
-- [foo]
import Aeneas
open Aeneas.Std Result Error
set_option linter.dupNamespace false
set_option linter.hashCommand false
set_option linter.unusedVariables false

namespace foo

/- [foo::bar]:
   Source: 'src/foo.rs', lines 1:0-1:24 -/
def bar (a : Bool) : Result Bool :=
  ok a

/- [foo::foo]: loop 0:
   Source: 'src/foo.rs', lines 4:4-6:5 -/
def foo_loop (s : Bool) : Result Unit :=
  if 0#i32 < 0#i32
  then do
       let a ← bar s
       foo_loop a
  else ok ()
partial_fixpoint

/- [foo::foo]:
   Source: 'src/foo.rs', lines 2:0-8:1 -/
def foo (s : Bool) : Result Bool :=
  do
  foo_loop s
  ok s

end foo

In the extracted code, foo_loop is a no-op, while it should be returning Bool since it takes a mutable reference to s (regardless of whether foo_loop performs any changes to s or not).