anchor.diff:                      (List.rev !fresh_scope)) in
       let theory = theory@[Push]@qry@[Pop] in
       let theory, used_unsat_core = filter_theory theory in
  -    let input, qhash, log_file_name = mk_input false theory in
  +    let input, qhash, log_file_name = mk_input true theory in
       if not (cache_hit log_file_name cache qhash cb) then
           enqueue ({job=z3_job log_file_name r true label_messages input qhash; callback=cb})
   
  
positive.code:         match remaining with
          | [] -> ()
          | _ ->
              FStar.Errors.log_issue
                       r
                       (Errors.Warning_UnexpectedZ3Output, (BU.format1 "Unexpected output from Z3: %s\n"
                                      (String.concat "\n" remaining))) in
      {smt_result = BU.must result_opt;
       smt_reason_unknown = reason_unknown;
       smt_unsat_core = unsat_core;
       smt_statistics = statistics;
       smt_labels = labels}
  
  let doZ3Exe (r:Range.range) (fresh:bool) (input:string) (label_messages:error_labels) : z3status * z3statistics =
    let parse (z3out:string) =
      let lines = String.split ['\n'] z3out |> List.map BU.trim_string in
      let smt_output = smt_output_sections r lines in
      let unsat_core =
          match smt_output.smt_unsat_core with
          | None -> None
  
negative.code:     let theory = theory @[Push]@qry@[Pop] in
      let theory, _used_unsat_core = filter_theory theory in
      let input, qhash, log_file_name = mk_input fresh theory in
      if not (fresh && cache_hit log_file_name cache qhash cb) then
          run_job ({job=z3_job log_file_name r fresh label_messages input qhash; callback=cb})
  
  let ask_n_cores
  