let mk_tuple_update c t i new_val =
  begin
    let ty = Z3.get_sort c t in
    let (mk_tuple_decl,fields)=Z3.get_tuple_sort c ty in
    if i>=Array.length fields then exitf "invalid tuple update, index is too big";
    let f j = 
      if i = j then (* use new_val at position i: *) new_val
      else (* use field j of t: *) (mk_unary_app c (fields.(j)) t)
    in let new_fields = Array.init (Array.length fields) f in
    Z3.mk_app c (Z3.get_tuple_sort_mk_decl c ty) new_fields;
  end