在Z3中没有直接的方法来遍历表达式的已经存在的Z3_ast，这在API中似乎很清楚。然而，有没有一种间接的方法，例如，拆分一个连词，用一个词代替Z3_ast中的一个词，例如由Z3_parse_smtlib2_string获得的，或者作为Z3_get_interpolant获得的插入词(这些是从Z3输出的，所以能够检查它们是有意义的(。
遍历是可能的，在C API中，其函数为Z3_get_app_num_args和Z3_get_app_arg。然而，只有当AST是一个函数应用程序(一个应用程序，必要时通过Z3_to_app强制转换(，其他AST类型可能没有可遍历的参数(例如，变量和数字，请参见Z3_AST_kind(时，这才有效。