anchor.diff:                  debug (fun() -> BU.print "Translate fv: it's a Sig_let\n" []);
                   debug (fun () -> BU.print2 "Type of lbdef: %s - %s\n" (P.tag_of_term (SS.compress lb.lbtyp)) (P.term_to_string (SS.compress lb.lbtyp)));
                   debug (fun () -> BU.print2 "Body of lbdef: %s - %s\n" (P.tag_of_term (SS.compress lb.lbdef)) (P.term_to_string (SS.compress lb.lbdef)));
  -                // let t = SS.compress lb.lbdef in
  -                // let x = (S.new_bv None S.tun, None) in
  -                // let t' = S.mk (Tm_abs([x], t, None)) None t.pos in
  -                // iapp (translate env bs t') (List.map (fun u -> (translate_univ env bs u, None)) us)
  -                translate_letbinding env [] lb
  +
  +                // VD: Don't unfold primops
  +                if (List.mem (P.lid_to_string (fvar.fv_name.v)) primops) then
  +                    mkConstruct fvar [] []
  +                else
  +                    translate_letbinding env [] lb
                end
             | None -> failwith "Could not find mutually recursive definition")
         | Some { sigel = Sig_datacon(_, _, _, lid, _, []) } ->
  
positive.code:   BU.smap_fold m (fun k v u -> BU.print2 "%s -> %%s\n" k (P.sigelt_to_string_short v)) ()
  
  let primops = ["op_Minus"; "op_Addition"; "op_Subtraction"; "op_GreaterThan"; "equals";
                 "op_Negation"; "c_and"; "c_or"]
  
  type var = bv
  type sort = int
  
negative.code:          | _ ->  U.mk_app tm args
        in
        let fv_lid = P.lid_to_string (fv.fv_name.v) in
        if (List.mem fv_lid primops) then
            readback_primops env fv_lid args
        else
            (match us with
  