Unsound behavior with QPs without condition

[marcoeilers]

@Felalolf found this examples that verifies but clearly shouldn't:

domain ShStruct2[T0, T1]  {

  function ShStructget1of2(x: ShStruct2[T0, T1]): T1 

  function ShStructget0of2(x: ShStruct2[T0, T1]): T0 

  function ShStructrev1of2(v1: T1): ShStruct2[T0, T1] 

  function ShStructrev0of2(v0: T0): ShStruct2[T0, T1] 

  axiom {
    (forall x: ShStruct2[T0, T1] ::
      { (ShStructget1of2(x): T1) }
      (ShStructrev1of2((ShStructget1of2(x): T1)): ShStruct2[T0, T1]) == x)
  }

  axiom {
    (forall x: ShStruct2[T0, T1] ::
      { (ShStructget0of2(x): T0) }
      (ShStructrev0of2((ShStructget0of2(x): T0)): ShStruct2[T0, T1]) == x)
  }
}

field Intint$$$$_E_$$$: Int

// decreases 
function witness_4e2a3fe_F(P0_PI0: Int): ShStruct2[Ref, Ref]

predicate SharedInv_4e2a3fe_F() {
  (forall i_V0: Int ::
    { (ShStructget0of2(witness_4e2a3fe_F(i_V0)): Ref) }
    true && (let fn$$0 == (witness_4e2a3fe_F(i_V0)) in true) ==>
    acc((ShStructget0of2(witness_4e2a3fe_F(i_V0)): Ref).Intint$$$$_E_$$$, 1 /
    2)) &&
  (forall i_V0: Int ::
    { (ShStructget1of2(witness_4e2a3fe_F(i_V0)): Ref) }
    true && (let fn$$0 == (witness_4e2a3fe_F(i_V0)) in true) ==>
    acc((ShStructget1of2(witness_4e2a3fe_F(i_V0)): Ref).Intint$$$$_E_$$$, 1 /
    2))
}

method processRequest_4e2a3fe_F(id_V0: Int)
  requires (let fn$$0 ==
      (witness_4e2a3fe_F(id_V0)) in
      acc((ShStructget0of2(fn$$0): Ref).Intint$$$$_E_$$$, 1 / 2) &&
      acc((ShStructget1of2(fn$$0): Ref).Intint$$$$_E_$$$, 1 / 2))
  requires acc(SharedInv_4e2a3fe_F(), write)
{

  // decl id_V0_CN0: int°°
  {
    var id_V0_CN0: Int

    // init id_V0_CN0
    inhale id_V0_CN0 == 0

    // id_V0_CN0 = id_V0
    id_V0_CN0 := id_V0

    // decl 

    // unfold acc(SharedInv_4e2a3fe_F())
    unfold acc(SharedInv_4e2a3fe_F(), write)

    // assert false
    assert false
    label returnLabel
  }
}