anchor.diff:  let run_all () =
       BU.print1 "%s" (P.term_to_string znat);
       let l_int = run_all_interpreter_with_time () in
  -    let l_nbe = run_all_nbe_with_time () in
  +    let l_nbe = run_all_nbe_with_time () in ()
       compare_times l_int l_nbe
  
positive.code:     always i (term_eq (U.unascribe x) expected)
  
  let run_interpreter i r expected = run_either i r expected (N.normalize [Env.Beta; Env.UnfoldUntil delta_constant; Env.Primops])
  let run_nbe i r expected =
  run_either i r expected (FStar.TypeChecker.NBE.test_normalize [FStar.TypeChecker.NBE.UnfoldUntil delta_constant])
  let run_interpreter_with_time i r expected =
    let interp () = run_interpreter i r expected in
    (i, snd (FStar.Util.return_execution_time interp))
  
negative.code:   ; (25, (tc_nbe "copy [0;1]"), (tc_nbe "[0;1]"))
    ; (26, (tc_nbe "rev [0;1;2;3;4;5;6;7;8;9;10]"), (tc_nbe "[10;9;8;7;6;5;4;3;2;1;0]"))
    // Type defs not yet implemented for NBE
    // ; (271, (tc_nbe "(FStar.String.substring \"abcdef\" 1 2)"), (tc_nbe "\"bc\"")) //VD: Not sure why, but this test fails on the normalizer
    // ; (27, (tc_nbe "(rev (FStar.String.list_of_string \"abcd\"))"), (tc_nbe "['d'; 'c'; 'b'; 'a']"))// -- CH: works up to an unfolding too much (char -> char')
    ; (28, (tc_nbe "(fun x y z q -> z) T T F T"), (tc_nbe "F"))
    ; (29, (tc_nbe "[T; F]"), (tc_nbe "[T; F]"))
    ; (31, (tc_nbe "id_tb T"), (tc_nbe "T"))
  