anchor.diff:    (* All the distinguished combinators that correspond to allocation, either on
      * the stack, on the heap (GC'd or manually-managed). *)
     | MLE_App ({ expr = MLE_TApp({ expr = MLE_Name p }, _) } , [ e1; e2 ])
  -    when (string_of_mlpath p = "FStar.Buffer.create" || string_of_mlpath p = "LowStar.Buffer.alloca" ||
  -          string_of_mlpath p = "LowStar.Monotonic.Buffer.malloca") ->
  +    when (string_of_mlpath p = "FStar.Buffer.create" || string_of_mlpath p = "LowStar.Monotonic.Buffer.malloca") ->
         EBufCreate (Stack, translate_expr env e1, translate_expr env e2)
   
     | MLE_App ({ expr = MLE_TApp({ expr = MLE_Name p }, _) } , [ init ])
  
positive.code:   | MLTY_Named ([arg; _; _], p) when
      Syntax.string_of_mlpath p = "LowStar.Monotonic.Buffer.mbuffer" -> TBuf (translate_type env arg)
    | MLTY_Named ([arg], p) when
      Syntax.string_of_mlpath p = "LowStar.Buffer.buffer" ||
      Syntax.string_of_mlpath p = "FStar.Buffer.buffer" ||
      Syntax.string_of_mlpath p = "FStar.HyperStack.reference" ||
      Syntax.string_of_mlpath p = "FStar.HyperStack.stackref" ||
      Syntax.string_of_mlpath p = "FStar.HyperStack.ref" ||
  
negative.code:       EBufFree (translate_expr env e2)
  
    (* Generic buffer operations. *)
    | MLE_App ({ expr = MLE_TApp({ expr = MLE_Name p }, _) }, [ e1; e2; _e3 ]) when (string_of_mlpath p = "FStar.Buffer.sub") ->
        EBufSub (translate_expr env e1, translate_expr env e2)
  
    | MLE_App ({ expr = MLE_TApp({ expr = MLE_Name p }, _) }, [ e1; e2; _e3 ]) when string_of_mlpath p = "LowStar.Monotonic.Buffer.msub" ->
        EBufSub (translate_expr env e1, translate_expr env e2)
  
    | MLE_App ({ expr = MLE_TApp({ expr = MLE_Name p }, _) }, [ e1; e2 ]) when (string_of_mlpath p = "FStar.Buffer.join") ->
        (translate_expr env e1)
  
    | MLE_App ({ expr = MLE_TApp({ expr = MLE_Name p }, _) }, [ e1; e2 ]) when (string_of_mlpath p = "FStar.Buffer.offset") ->
        EBufSub (translate_expr env e1, translate_expr env e2)
  
    | MLE_App ({ expr = MLE_TApp({ expr = MLE_Name p }, _) }, [ e1; e2 ]) when string_of_mlpath p = "LowStar.Monotonic.Buffer.moffset" ->
        EBufSub (translate_expr env e1, translate_expr env e2)
  
    | MLE_App ({ expr = MLE_TApp({ expr = MLE_Name p }, _) }, [ e1; e2; e3 ])
  