Incompleteness in witness computation for existential quantifiers

[wies]

See https://github.com/nyu-acsys/raven/blob/main/test/bugs/incomplete_witness_computation.rav#L36

Here is the relevant part of the debug output:

[Debug] WitnessComputation.elim_a1: expr = exists
        ghost $bind_xs&5: Stack.TList.T ::  exists x^6: Ref ::
         own(s^1, Stack.top, Stack.Frac$top.frac_chunk(x^6, 1.)) && Stack.list(x^6, $bind_xs&5)
[Debug] TrnslExhale.WitnessComputation.elim_a1: witnesses_local_vars_ident: 
[Debug] TrnslExhale.WitnessComputation.elim_a1: env_local_vars_ident: 
[Debug] TrnslExhale.WitnessComputation.elim_a1: env_local_var_decls: 
[Debug] Rewrites.HeapsExplicitTrnsl.WitnessComputation.elim_a1: witness_map: 
        []
[Warning] File "test/concurrent/treiber_stack/treiber_stack_atomics.rav", line 36, columns 4-18:
36 |     fold stack(s);
         ^^^^^^^^^^^^^^
Verification Error: No witnesses could be computed for: $bind_xs&5.