anchor.diff:    | MLE_App ({ expr = MLE_TApp({ expr = MLE_Name p }, _) } , [ e1; e2 ])
       when (string_of_mlpath p = "FStar.Buffer.create" ||
             string_of_mlpath p = "LowStar.Monotonic.Buffer.malloca" ||
  -          string_of_mlpath p = "LowStar.ImmutableBuffer.ialloca" ||
  -          string_of_mlpath p = "Steel.Array.alloc") ->
  +          string_of_mlpath p = "LowStar.ImmutableBuffer.ialloca") ->
         EBufCreate (Stack, translate_expr env e1, translate_expr env e2)
   
     | MLE_App ({ expr = MLE_TApp({ expr = MLE_Name p }, _) } , [ elen ])
  
positive.code:     *)
    | MLE_App ({ expr = MLE_TApp({ expr = MLE_Name p }, _) } , [ _rid; init ])
      when (string_of_mlpath p = "FStar.HyperStack.ST.ralloc") ||
           (string_of_mlpath p = "FStar.HyperStack.ST.ralloc_drgn")->
        EBufCreate (Eternal, translate_expr env init, EConstant (UInt32, "1"))
  
    | MLE_App ({ expr = MLE_TApp({ expr = MLE_Name p }, _) }, [ _e0; e1; e2 ])
  
negative.code:          (string_of_mlpath p = "FStar.HyperStack.ST.ralloc_drgn_mm") ->
        EBufCreate (ManuallyManaged, translate_expr env init, EConstant (UInt32, "1"))
  
    | MLE_App ({ expr = MLE_TApp({ expr = MLE_Name p }, _) } , [ init ])
      when (string_of_mlpath p = "Steel.Reference.alloc") ->
        EBufCreate (ManuallyManaged, translate_expr env init, EConstant (UInt32, "1"))
  
    | MLE_App ({ expr = MLE_TApp({ expr = MLE_Name p }, _) }, [ _e0; e1; e2 ])
      when (string_of_mlpath p = "FStar.Buffer.rcreate_mm" ||
            string_of_mlpath p = "LowStar.Monotonic.Buffer.mmalloc" ||
  