anchor.diff:        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") ->
  +    when (string_of_mlpath p = "FStar.Buffer.rcreate_mm" || string_of_mlpath p = "LowStar.Buffer.rcreate_mm") ->
         EBufCreate (ManuallyManaged, translate_expr env e1, translate_expr env e2)
   
     (* Only manually-managed references and buffers can be freed. *)
     | MLE_App ({ expr = MLE_TApp({ expr = MLE_Name p }, _) }, [ e2 ]) when (string_of_mlpath p = "FStar.HyperStack.ST.rfree") ->
         EBufFree (translate_expr env e2)
   
  -  | MLE_App ({ expr = MLE_TApp({ expr = MLE_Name p }, _) }, [ e2 ]) when (string_of_mlpath p = "FStar.Buffer.rfree") ->
  +  | MLE_App ({ expr = MLE_TApp({ expr = MLE_Name p }, _) }, [ e2 ]) when (string_of_mlpath p = "FStar.Buffer.rfree" || string_of_mlpath p = "LowStar.Buffer.rfree") ->
         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") ->
  +  | MLE_App ({ expr = MLE_TApp({ expr = MLE_Name p }, _) }, [ e1; e2; _e3 ]) when (string_of_mlpath p = "FStar.Buffer.sub" || string_of_mlpath p = "LowStar.Buffer.sub") ->
         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") ->
  +  | MLE_App ({ expr = MLE_TApp({ expr = MLE_Name p }, _) }, [ e1; e2 ]) when (string_of_mlpath p = "FStar.Buffer.offset" || string_of_mlpath p = "LowStar.Buffer.offset") ->
         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 = "FStar.Buffer.upd" || string_of_mlpath p = "FStar.Buffer.op_Array_Assignment" ->
  +    when string_of_mlpath p = "FStar.Buffer.upd" || string_of_mlpath p = "FStar.Buffer.op_Array_Assignment"
  +    || string_of_mlpath p = "LowStar.Buffer.upd" ->
         EBufWrite (translate_expr env e1, translate_expr env e2, translate_expr env e3)
     | MLE_App ({ expr = MLE_TApp({ expr = MLE_Name p }, _) }, [ e1; e2 ])
       when string_of_mlpath p = "FStar.HyperStack.ST.op_Colon_Equals" ->
  
positive.code:       EBufCreate (Eternal, 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") ->
        EBufCreate (Eternal, translate_expr env e1, translate_expr env e2)
  
    | MLE_App ({ expr = MLE_TApp({ expr = MLE_Name p }, _) } , [ _rid; init ])
  
negative.code:     ->
        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" ||
  