anchor.diff:        repl_stdin = open_stdin ();
         repl_names = commit_name_tracking None initial_names name_events } in
   
  -  if FStar.Options.record_hints() || FStar.Options.use_hints() then
  -    FStar.SMTEncoding.Solver.with_hints_db (List.hd (Options.file_list ())) (fun () -> go init_st)
  -  else
  -    go init_st
  +  let exit_code =
  +    if FStar.Options.record_hints() || FStar.Options.use_hints() then
  +      FStar.SMTEncoding.Solver.with_hints_db (List.hd (Options.file_list ())) (fun () -> go init_st)
  +    else
  +      go init_st in
  +  exit exit_code
   
   let interactive_mode (filename:string): unit =
     FStar.Util.set_printer interactive_printer;
  
positive.code:           { qid = q.qid; qq = MissingCurrentModule }
          | _ -> q
  
  let rec go st : unit =
    let query = validate_query st (read_interactive_query st.repl_stdin) in
    let (status, response), state_opt = run_query st query.qq in
    write_response query.qid status response;
    match state_opt with
    | Inl st' -> go st'
    | Inr exitcode -> exit exitcode
  
  let interactive_error_handler = // No printing here — collect everything for future use
    let issues : ref<list<issue>> = Util.mk_ref [] in
  
negative.code: let read_interactive_query stream : query =
    try
      match Util.read_line stream with
      | None -> raise (ExitREPL 0)
      | Some line ->
        match Util.json_of_string line with
        | None -> { qid = "?"; qq = ProtocolViolation "Json parsing failed." }
  