let mk_sub = 
    let table = Hashtbl.create 17 in
    let _ =  Tools.add_at_reset (fun () -> Hashtbl.clear table) in
      fun n i j ->
        assert(0 <= i && i <= j && j < n);
        try
          Hashtbl.find table (n, i, j)
        with
            Not_found ->
              let hsh = genidx() in
              let op = (Bv(Sub(n, i, j)), hsh) in
                Hashtbl.add table (n, i, j) op; op