id|input_file|expected_stdout|expected_stderr|expected_exit_code|runner_modes|command_count|command_kind|support_status|syntax_family|reject_stage|status_category|reason_unknown|diagnostic|z3_expected|z3_diff_reason|allow_unsupported|allow_unknown|normalization
z3_arch_bool_incremental|smt2/z3_arch_bool_incremental.smt2|smt2/z3_arch_bool_incremental.expected.out||0|parser-runner,file-shell,interactive-shell|8|incremental|supported-success|Bool|none|sat-after-pop|none|none|same|none|false|false|exact
z3_arch_assumptions_core|smt2/z3_arch_assumptions_core.smt2|smt2/z3_arch_assumptions_core.expected.out||0|parser-runner,file-shell,interactive-shell|5|assumptions-core|supported-success|Bool|none|unsat-assumptions|none|none|same|none|false|false|exact
z3_arch_let_bool|smt2/z3_arch_let_bool.smt2|smt2/z3_arch_let_bool.expected.out||0|parser-runner,file-shell,interactive-shell|4|let-bool|supported-success|Bool|none|let-bool-unsat|none|none|same|none|false|false|exact
z3_arch_let_euf|smt2/z3_arch_let_euf.smt2|smt2/z3_arch_let_euf.expected.out||0|parser-runner,file-shell,interactive-shell|7|let-euf|supported-success|EUF|none|let-euf-unsat|none|none|same|none|false|false|exact
z3_arch_define_fun_bool|smt2/z3_arch_define_fun_bool.smt2|smt2/z3_arch_define_fun_bool.expected.out||0|parser-runner,file-shell,interactive-shell|5|define-fun-bool|supported-success|Bool|none|define-fun-bool-macro|none|none|same|none|false|false|exact
z3_arch_model_eval|smt2/z3_arch_model_eval.smt2|smt2/z3_arch_model_eval.expected.out||0|parser-runner,file-shell,interactive-shell|7|model-eval|supported-success|Bool|none|sat-model-value-eval|none|none|same|none|false|false|exact
z3_arch_eval_completion|smt2/z3_arch_eval_completion.smt2|smt2/z3_arch_eval_completion.expected.out||0|parser-runner,file-shell,interactive-shell|6|eval-completion|supported-success|EUF|none|eval-completion-false-true|none|error:model-eval-failed|different|z0-eval-completion-default-fails-partial-uf|false|false|exact
z3_arch_eval_availability|smt2/z3_arch_eval_availability.smt2|smt2/z3_arch_eval_availability.expected.out||0|parser-runner,file-shell,interactive-shell|7|eval-availability|supported-success|Bool|none|eval-disabled-no-current-success|no-current-result|error:model-production-disabled|different|z0-eval-availability-text|false|false|exact
z3_arch_model_query_availability|smt2/z3_arch_model_query_availability.smt2|smt2/z3_arch_model_query_availability.expected.out||0|parser-runner,file-shell,interactive-shell|7|model-query-availability|supported-success|EUF|none|model-query-unavailable|no-current-result|error:model-value-eval-unavailable|different|z0-model-eval-unavailable-text|false|false|exact
z3_arch_model_query_stale|smt2/z3_arch_model_query_stale.smt2|smt2/z3_arch_model_query_stale.expected.out||0|parser-runner,file-shell,interactive-shell|11|model-query-stale|supported-success|Bool|none|model-query-stale|stale|error:model-value-eval-stale|different|z0-stale-query-text|false|false|exact
z3_arch_model_repeated_scoped|smt2/z3_arch_model_repeated_scoped.smt2|smt2/z3_arch_model_repeated_scoped.expected.out||0|parser-runner,file-shell,interactive-shell|12|model-repeated-scoped|supported-success|Bool|none|multiple-model-queries-scopes|none|none|same|none|false|false|exact
z3_arch_model_euf_constants|smt2/z3_arch_model_euf_constants.smt2|smt2/z3_arch_model_euf_constants.expected.out||0|parser-runner,file-shell,interactive-shell|8|model-euf-constants|supported-success|EUF|none|model-universe-constants|none|none|different|z0-model-universe-format|false|false|exact
z3_arch_model_partial_unary_uf|smt2/z3_arch_model_partial_unary_uf.smt2|smt2/z3_arch_model_partial_unary_uf.expected.out||0|parser-runner,file-shell,interactive-shell|9|model-partial-unary-uf|supported-success|EUF|none|model-partial-function|none|none|different|z0-uses-unspecified-default|false|false|exact
z3_arch_get_value_partial_uf_completion|smt2/z3_arch_get_value_partial_uf_completion.smt2|smt2/z3_arch_get_value_partial_uf_completion.expected.out||0|parser-runner,file-shell,interactive-shell|10|get-value-partial-uf-completion|supported-success|EUF|none|get-value-completion|none|none|different|z0-completes-undefined-uf-application|false|false|exact
z3_arch_proof_modes|smt2/z3_arch_proof_modes.smt2|smt2/z3_arch_proof_modes.expected.out||0|parser-runner,file-shell,interactive-shell|12|proof-modes|supported-success|Bool|none|proof-disabled-enabled|none|none|different|z0-uses-proof-skeleton-text|false|false|exact
z3_arch_proof_availability|smt2/z3_arch_proof_availability.smt2|smt2/z3_arch_proof_availability.expected.out||0|parser-runner,file-shell,interactive-shell|8|proof-availability|supported-success|Bool|none|proof-no-current-wrong-stale|no-current-result/wrong-result/stale|error:proof-unavailable|different|z0-proof-availability-text|false|false|exact
z3_arch_unsat_query_availability|smt2/z3_arch_unsat_query_availability.smt2|smt2/z3_arch_unsat_query_availability.expected.out||0|parser-runner,file-shell,interactive-shell|12|unsat-query-availability|supported-success|Bool|none|unsat-query-no-current-wrong-stale|no-current-result/wrong-result/stale|error:unsat-query-unavailable|different|z0-unsat-query-availability-text|false|false|exact
z3_arch_unknown_unsupported|smt2/z3_arch_unknown_unsupported.smt2|smt2/z3_arch_unknown_unsupported.expected.out||0|parser-runner,file-shell,interactive-shell|5|unsupported-fragment|explicit-unsupported|quantifier|parser|unsupported-fragment|unsupported-fragment|unsupported:quantifiers|different|phase-limited-quantifiers|true|false|exact
z3_arch_unsupported_array_sort|smt2/z3_arch_unsupported_array_sort.smt2|smt2/z3_arch_unsupported_array_sort.expected.out||0|parser-runner,file-shell,interactive-shell|1|unsupported-array-sort|explicit-unsupported|array|sort-check|unsupported-fragment|unsupported-fragment|unsupported:arrays|different|phase-limited-arrays|true|false|exact
z3_arch_unsupported_array_select_store|smt2/z3_arch_unsupported_array_select_store.smt2|smt2/z3_arch_unsupported_array_select_store.expected.out||0|parser-runner,file-shell,interactive-shell|1|unsupported-array-select-store|explicit-unsupported|array|parser|unsupported-fragment|unsupported-fragment|unsupported:arrays|different|z0-reserves-array-operators-before-uf-lookup|true|false|exact
z3_arch_unsupported_bv_sort|smt2/z3_arch_unsupported_bv_sort.smt2|smt2/z3_arch_unsupported_bv_sort.expected.out||0|parser-runner,file-shell,interactive-shell|1|unsupported-bv-sort|explicit-unsupported|bv|sort-check|unsupported-fragment|unsupported-fragment|unsupported:bit-vectors|different|phase-limited-bit-vectors|true|false|exact
z3_arch_unsupported_bv_literal|smt2/z3_arch_unsupported_bv_literal.smt2|smt2/z3_arch_unsupported_bv_literal.expected.out||0|parser-runner,file-shell,interactive-shell|1|unsupported-bv-literal|explicit-unsupported|bv|parser|unsupported-fragment|unsupported-fragment|unsupported:bit-vectors|different|phase-limited-bit-vectors|true|false|exact
z3_arch_unsupported_bv_indexed_op|smt2/z3_arch_unsupported_bv_indexed_op.smt2|smt2/z3_arch_unsupported_bv_indexed_op.expected.out||0|parser-runner,file-shell,interactive-shell|1|unsupported-bv-indexed-op|explicit-unsupported|bv|parser|unsupported-fragment|unsupported-fragment|unsupported:bit-vectors|different|phase-limited-bit-vectors|true|false|exact
z3_arch_unsupported_datatype_decl|smt2/z3_arch_unsupported_datatype_decl.smt2|smt2/z3_arch_unsupported_datatype_decl.expected.out||0|parser-runner,file-shell,interactive-shell|1|unsupported-datatype-decl|explicit-unsupported|datatype|parser|unsupported-fragment|unsupported-fragment|unsupported:datatypes|different|phase-limited-datatypes|true|false|exact
z3_arch_unsupported_datatype_constructor|smt2/z3_arch_unsupported_datatype_constructor.smt2|smt2/z3_arch_unsupported_datatype_constructor.expected.out||0|parser-runner,file-shell,interactive-shell|1|unsupported-datatype-constructor|explicit-unsupported|datatype|parser|unsupported-fragment|unsupported-fragment|unsupported:datatypes|different|phase-limited-datatypes|true|false|exact
z3_arch_unsupported_datatype_match|smt2/z3_arch_unsupported_datatype_match.smt2|smt2/z3_arch_unsupported_datatype_match.expected.out||0|parser-runner,file-shell,interactive-shell|1|unsupported-datatype-match|explicit-unsupported|datatype|parser|unsupported-fragment|unsupported-fragment|unsupported:datatypes|different|phase-limited-datatypes|true|false|exact
z3_arch_unsupported_string_sort|smt2/z3_arch_unsupported_string_sort.smt2|smt2/z3_arch_unsupported_string_sort.expected.out||0|parser-runner,file-shell,interactive-shell|1|unsupported-string-sort|explicit-unsupported|seq|sort-check|unsupported-fragment|unsupported-fragment|unsupported:strings|different|phase-limited-seq-strings|true|false|exact
z3_arch_unsupported_string_literal|smt2/z3_arch_unsupported_string_literal.smt2|smt2/z3_arch_unsupported_string_literal.expected.out||0|parser-runner,file-shell,interactive-shell|1|unsupported-string-literal|explicit-unsupported|seq|parser|unsupported-fragment|unsupported-fragment|unsupported:strings|different|phase-limited-seq-strings|true|false|exact
z3_arch_unsupported_seq_op|smt2/z3_arch_unsupported_seq_op.smt2|smt2/z3_arch_unsupported_seq_op.expected.out||0|parser-runner,file-shell,interactive-shell|1|unsupported-seq-op|explicit-unsupported|seq|parser|unsupported-fragment|unsupported-fragment|unsupported:strings|different|phase-limited-seq-strings|true|false|exact
z3_arch_unsupported_exists|smt2/z3_arch_unsupported_exists.smt2|smt2/z3_arch_unsupported_exists.expected.out||0|parser-runner,file-shell,interactive-shell|4|unsupported-exists|explicit-unsupported|quantifier|parser|unsupported-fragment|unsupported-fragment|unsupported:quantifiers|different|phase-limited-quantifiers|true|false|exact
z3_arch_unsupported_reserved_identifier|smt2/z3_arch_unsupported_reserved_identifier.smt2|smt2/z3_arch_unsupported_reserved_identifier.expected.out||0|parser-runner,file-shell,interactive-shell|1|unsupported-reserved-identifier|explicit-unsupported|reserved|parser|unsupported-fragment|unsupported-fragment|unsupported:reserved-identifier|different|reserved-identifier-not-uf|true|false|exact
z3_arch_unsupported_define_fun_nonnullary|smt2/z3_arch_unsupported_define_fun_nonnullary.smt2|smt2/z3_arch_unsupported_define_fun_nonnullary.expected.out||0|parser-runner,file-shell,interactive-shell|1|unsupported-define-fun-nonnullary|explicit-unsupported|command|parser|unsupported-command|unsupported-fragment|unsupported:define-fun|different|phase-limited-define-fun|true|false|exact
z3_arch_unsupported_parametric_sort|smt2/z3_arch_unsupported_parametric_sort.smt2|smt2/z3_arch_unsupported_parametric_sort.expected.out||0|parser-runner,file-shell,interactive-shell|1|unsupported-parametric-sort|explicit-unsupported|sort|cmd-context|unsupported-fragment|unsupported-fragment|unsupported:sort-arity|different|phase-limited-parametric-sorts|true|false|exact
z3_arch_global_decls_default|smt2/z3_arch_global_decls_default.smt2|smt2/z3_arch_global_decls_default.expected.out||0|parser-runner,file-shell,interactive-shell|5|global-decls-default|supported-error|Bool|parser|undeclared-symbol|none|type:undeclared-symbol|same|none|false|false|exact
z3_arch_global_decls_enabled|smt2/z3_arch_global_decls_enabled.smt2|smt2/z3_arch_global_decls_enabled.expected.out||0|parser-runner,file-shell,interactive-shell|7|global-decls-enabled|supported-success|Bool|none|sat-after-pop-global-decl|none|none|same|none|false|false|exact
z3_arch_global_declarations_alias|smt2/z3_arch_global_declarations_alias.smt2|smt2/z3_arch_global_declarations_alias.expected.out||0|parser-runner,file-shell,interactive-shell|7|global-declarations-alias|supported-success|Bool|none|sat-after-pop-global-decl|none|none|same|none|false|false|exact
z3_arch_global_decls_late_set|smt2/z3_arch_global_decls_late_set.smt2|smt2/z3_arch_global_decls_late_set.expected.out||0|parser-runner,file-shell,interactive-shell|5|global-decls-late-set|supported-error|Bool|cmd-context|late-option|none|solver:global-decls-active|different|z0-uses-stable-context-error|false|false|exact
z3_arch_global_declarations_alias_late_set|smt2/z3_arch_global_declarations_alias_late_set.smt2|smt2/z3_arch_global_declarations_alias_late_set.expected.out||0|parser-runner,file-shell,interactive-shell|5|global-declarations-alias-late-set|supported-error|Bool|cmd-context|late-option|none|solver:global-decls-active|different|z0-uses-stable-context-error|false|false|exact
z3_arch_global_decls_reset|smt2/z3_arch_global_decls_reset.smt2|smt2/z3_arch_global_decls_reset.expected.out||0|parser-runner,file-shell,interactive-shell|8|global-decls-reset|supported-success|Bool|none|reset-option-persistence|none|none|same|none|false|false|exact
z3_arch_pop_underflow|smt2/z3_arch_pop_underflow.smt2|smt2/z3_arch_pop_underflow.expected.out||0|parser-runner,file-shell,interactive-shell|1|pop-underflow|supported-error|command|cmd-context|invalid-pop|none|solver:invalid-pop|different|z0-uses-stable-invalid-pop-diagnostic|false|false|exact
z3_arch_pop_over_scope|smt2/z3_arch_pop_over_scope.smt2|smt2/z3_arch_pop_over_scope.expected.out||0|parser-runner,file-shell,interactive-shell|5|pop-over-scope|supported-error|command|cmd-context|invalid-pop|none|solver:invalid-pop|different|z0-uses-stable-invalid-pop-diagnostic|false|false|exact
z3_arch_builtin_option_storage|smt2/z3_arch_builtin_option_storage.smt2|smt2/z3_arch_builtin_option_storage.expected.out||0|parser-runner,file-shell,interactive-shell|19|builtin-option-storage|supported-success|options|none|option-roundtrip|none|none|different|z0-stores-error-behavior-and-runner-uses-core-modes|false|false|exact
z3_arch_builtin_options_reset|smt2/z3_arch_builtin_options_reset.smt2|smt2/z3_arch_builtin_options_reset.expected.out||0|parser-runner,file-shell,interactive-shell|23|builtin-options-reset|supported-success|options|none|reset-option-persistence|none|none|same|none|false|false|exact
z3_arch_auto_config_option|smt2/z3_arch_auto_config_option.smt2|smt2/z3_arch_auto_config_option.expected.out||0|parser-runner,file-shell,interactive-shell|5|auto-config-option|supported-success|options|none|auto-config-roundtrip-reset|none|none|same|none|false|false|exact
z3_arch_reproducible_resource_limit_option|smt2/z3_arch_reproducible_resource_limit_option.smt2|smt2/z3_arch_reproducible_resource_limit_option.expected.out||0|parser-runner,file-shell,interactive-shell|5|reproducible-resource-limit-option|supported-success|options|none|reproducible-resource-limit-roundtrip-reset|none|none|same|none|false|false|exact
z3_arch_builtin_option_invalid_value|smt2/z3_arch_builtin_option_invalid_value.smt2|smt2/z3_arch_builtin_option_invalid_value.expected.out||1|parser-runner,file-shell,interactive-shell|4|builtin-option-invalid-value|supported-error|options|cmd-context|invalid-option-value|none|parse:option-invalid-verbosity|different|z0-uses-stable-option-validation-diagnostic|false|false|exact
z3_arch_builtin_option_invalid_bool_enum|smt2/z3_arch_builtin_option_invalid_bool_enum.smt2|smt2/z3_arch_builtin_option_invalid_bool_enum.expected.out||1|parser-runner,file-shell,interactive-shell|7|builtin-option-invalid-bool-enum|supported-error|options|cmd-context|invalid-option-value|none|parse:option-invalid-bool-enum|different|z0-uses-stable-option-validation-diagnostic|false|false|exact
z3_arch_regular_output_channel_stderr|smt2/z3_arch_regular_output_channel_stderr.smt2|smt2/z3_arch_regular_output_channel_stderr.expected.out|smt2/z3_arch_regular_output_channel_stderr.expected.err|0|file-shell,interactive-shell|3|regular-output-channel-stderr|supported-success|options|none|regular-output-channel-routing|none|none|same|none|false|false|exact
z3_arch_diagnostic_output_channel_stderr|smt2/z3_arch_diagnostic_output_channel_stderr.smt2|smt2/z3_arch_diagnostic_output_channel_stderr.expected.out|smt2/z3_arch_diagnostic_output_channel_stderr.expected.err|1|file-shell,interactive-shell|4|diagnostic-output-channel-stderr|supported-error|options|runner|diagnostic-output-channel-routing|none|parse:push-count|same|none|false|false|exact
z3_arch_unsupported_set_option|smt2/z3_arch_unsupported_set_option.smt2|smt2/z3_arch_unsupported_set_option.expected.out||0|parser-runner,file-shell,interactive-shell|1|unsupported-set-option|explicit-unsupported|options|cmd-context|unsupported-option|unsupported-fragment|unsupported:option|different|phase-limited-module-options|true|false|exact
z3_arch_unsupported_get_option|smt2/z3_arch_unsupported_get_option.smt2|smt2/z3_arch_unsupported_get_option.expected.out||0|parser-runner,file-shell,interactive-shell|1|unsupported-get-option|explicit-unsupported|options|cmd-context|unsupported-option|unsupported-fragment|unsupported:option|different|phase-limited-module-options|true|false|exact
z3_arch_set_info_print_success|smt2/z3_arch_set_info_print_success.smt2|smt2/z3_arch_set_info_print_success.expected.out||0|parser-runner,file-shell,interactive-shell|4|set-info-print-success|supported-success|info|none|metadata-print-success|none|none|same|none|false|false|exact
z3_arch_unsupported_get_info|smt2/z3_arch_unsupported_get_info.smt2|smt2/z3_arch_unsupported_get_info.expected.out||0|parser-runner,file-shell,interactive-shell|1|unsupported-get-info|explicit-unsupported|info|cmd-context|unsupported-info-key|unsupported-fragment|unsupported:info|different|phase-limited-info-key|true|false|exact
z3_arch_info_statistics_rlimit|smt2/z3_arch_info_statistics_rlimit.smt2|smt2/z3_arch_info_statistics_rlimit.expected.out||0|parser-runner,file-shell,interactive-shell|6|get-info-statistics-rlimit|supported-success|info|none|rlimit-statistics|none|none|different|z0-statistics-key-subset-exact|false|false|exact
z3_arch_info_statistics_no_check|smt2/z3_arch_info_statistics_no_check.smt2|smt2/z3_arch_info_statistics_no_check.expected.out||0|parser-runner,file-shell,interactive-shell|4|get-info-statistics-no-check|supported-success|info|none|rlimit-statistics-no-check|none|none|different|z0-statistics-empty-no-check-exact|false|false|exact
z3_arch_info_reason_unknown_default|smt2/z3_arch_info_reason_unknown_default.smt2|smt2/z3_arch_info_reason_unknown_default.expected.out||0|parser-runner,file-shell,interactive-shell|6|get-info-reason-unknown-default|supported-success|info|none|reason-unknown-default-stale|no-current-result|none|different|z0-reports-stale-after-context-mutation|false|false|exact
z3_arch_info_reason_unknown_unsat|smt2/z3_arch_info_reason_unknown_unsat.smt2|smt2/z3_arch_info_reason_unknown_unsat.expected.out||0|parser-runner,file-shell,interactive-shell|5|get-info-reason-unknown-unsat|supported-success|info|none|reason-unknown-unsat-cleared|no-current-result|none|same|none|false|false|exact
z3_arch_reset_clears_reason_unknown|smt2/z3_arch_reset_clears_reason_unknown.smt2|smt2/z3_arch_reset_clears_reason_unknown.expected.out||0|parser-runner,file-shell,interactive-shell|6|get-info-reason-unknown-reset|supported-success|info|none|reason-unknown-reset-cleared|no-current-result|none|same|none|false|false|exact
z3_arch_custom_statistics_incomplete|smt2/z3_arch_custom_statistics_incomplete.smt2|smt2/z3_arch_custom_statistics_incomplete.expected.out||0|parser-runner|1|custom-factory-statistics|supported-success|custom-factory|solver|statistics-incomplete-missing-owner|incomplete-theory(stats)|statistics-missing-owner:backend.custom|different|z0-custom-factory-statistics|false|false|exact
z3_arch_custom_statistics_schema|smt2/z3_arch_custom_statistics_schema.smt2|smt2/z3_arch_custom_statistics_schema.expected.out||0|parser-runner|1|custom-factory-statistics|supported-success|custom-factory|solver|statistics-schema|incomplete-theory(stats)|statistics-missing-owner:backend.custom|different|z0-custom-factory-statistics-schema|false|false|statistics-schema
z3_arch_custom_unknown_with_model|smt2/z3_arch_custom_unknown_with_model.smt2|smt2/z3_arch_custom_unknown_with_model.expected.out||0|parser-runner|7|custom-factory-unknown-with-model|supported-unknown|custom-factory|solver|unknown-with-model|maybe|none|different|z0-custom-factory-with-model|false|true|exact
z3_arch_custom_unknown_no_model|smt2/z3_arch_custom_unknown_no_model.smt2|smt2/z3_arch_custom_unknown_no_model.expected.out||0|parser-runner|6|custom-factory-unknown-no-model|supported-unknown|custom-factory|solver|unknown-no-model|maybe|error:model-eval-unavailable|different|z0-custom-factory-no-model|false|true|exact
z3_arch_custom_timeout_reason|smt2/z3_arch_custom_timeout_reason.smt2|smt2/z3_arch_custom_timeout_reason.expected.out||0|parser-runner|2|custom-factory-reason|supported-unknown|custom-factory|solver|unknown-timeout|timeout|none|different|z0-custom-factory-reason|false|true|exact
z3_arch_custom_memout_reason|smt2/z3_arch_custom_memout_reason.smt2|smt2/z3_arch_custom_memout_reason.expected.out||0|parser-runner|2|custom-factory-reason|supported-unknown|custom-factory|solver|unknown-memout|memout|none|different|z0-custom-factory-reason|false|true|exact
z3_arch_custom_max_conflicts_reason|smt2/z3_arch_custom_max_conflicts_reason.smt2|smt2/z3_arch_custom_max_conflicts_reason.expected.out||0|parser-runner|2|custom-factory-reason|supported-unknown|custom-factory|solver|unknown-max-conflicts|max-conflicts|none|different|z0-custom-factory-reason|false|true|exact
z3_arch_custom_resource_limit_reason|smt2/z3_arch_custom_resource_limit_reason.smt2|smt2/z3_arch_custom_resource_limit_reason.expected.out||0|parser-runner|2|custom-factory-reason|supported-unknown|custom-factory|solver|unknown-resource-limit|resource-limit-exceeded|none|different|z0-custom-factory-reason|false|true|exact
z3_arch_custom_canceled_reason|smt2/z3_arch_custom_canceled_reason.smt2|smt2/z3_arch_custom_canceled_reason.expected.out||0|parser-runner|2|custom-factory-reason|supported-unknown|custom-factory|solver|unknown-canceled|canceled(api)|none|different|z0-custom-factory-reason|false|true|exact
z3_arch_custom_unsupported_fragment_reason|smt2/z3_arch_custom_unsupported_fragment_reason.smt2|smt2/z3_arch_custom_unsupported_fragment_reason.expected.out||0|parser-runner|2|custom-factory-reason|supported-unknown|custom-factory|solver|unknown-unsupported-fragment|unsupported-fragment(array)|none|different|z0-custom-factory-reason|true|true|exact
z3_arch_custom_invalid_core_reason|smt2/z3_arch_custom_invalid_core_reason.smt2|smt2/z3_arch_custom_invalid_core_reason.expected.out||0|parser-runner|2|custom-factory-reason|supported-unknown|custom-factory|solver|unknown-invalid-core|invalid-core|none|different|z0-custom-factory-reason|false|true|exact
z3_arch_custom_invalid_proof_reason|smt2/z3_arch_custom_invalid_proof_reason.smt2|smt2/z3_arch_custom_invalid_proof_reason.expected.out||0|parser-runner|2|custom-factory-reason|supported-unknown|custom-factory|solver|unknown-invalid-proof|invalid-proof|none|different|z0-custom-factory-reason|false|true|exact
z3_arch_custom_invalid_model_reason|smt2/z3_arch_custom_invalid_model_reason.smt2|smt2/z3_arch_custom_invalid_model_reason.expected.out||0|parser-runner|2|custom-factory-reason|supported-unknown|custom-factory|solver|unknown-invalid-model|invalid-model|none|different|z0-custom-factory-reason|false|true|exact
z3_arch_custom_incomplete_theory_reason|smt2/z3_arch_custom_incomplete_theory_reason.smt2|smt2/z3_arch_custom_incomplete_theory_reason.expected.out||0|parser-runner|2|custom-factory-reason|supported-unknown|custom-factory|solver|unknown-incomplete-theory|incomplete-theory(fake)|none|different|z0-custom-factory-reason|false|true|exact
z3_arch_custom_incomplete_quantifiers_reason|smt2/z3_arch_custom_incomplete_quantifiers_reason.smt2|smt2/z3_arch_custom_incomplete_quantifiers_reason.expected.out||0|parser-runner|2|custom-factory-reason|supported-unknown|custom-factory|solver|unknown-incomplete-quantifiers|incomplete-quantifiers|none|different|z0-custom-factory-reason|false|true|exact
z3_arch_custom_incomplete_lambdas_reason|smt2/z3_arch_custom_incomplete_lambdas_reason.smt2|smt2/z3_arch_custom_incomplete_lambdas_reason.expected.out||0|parser-runner|2|custom-factory-reason|supported-unknown|custom-factory|solver|unknown-incomplete-lambdas|incomplete-lambdas|none|different|z0-custom-factory-reason|false|true|exact
z3_arch_produce_flags_disabled|smt2/z3_arch_produce_flags_disabled.smt2|smt2/z3_arch_produce_flags_disabled.expected.out||0|parser-runner,file-shell,interactive-shell|9|produce-flags-disabled|supported-success|options|none|disabled-query|none|none|different|z0-emits-local-disabled-query-text|false|false|exact
z3_arch_produce_models_late_enable|smt2/z3_arch_produce_models_late_enable.smt2|smt2/z3_arch_produce_models_late_enable.expected.out||0|parser-runner,file-shell,interactive-shell|5|produce-models-late-enable|supported-success|options|none|late-dynamic-option|none|none|same|none|false|false|exact
z3_arch_produce_proofs_late_set|smt2/z3_arch_produce_proofs_late_set.smt2|smt2/z3_arch_produce_proofs_late_set.expected.out||0|parser-runner,file-shell,interactive-shell|3|produce-proofs-late-set|supported-error|options|cmd-context|late-option|none|solver:late-option-produce-proofs|different|z0-uses-stable-late-option-diagnostic|false|false|exact
z3_arch_produce_unsat_cores_late_set|smt2/z3_arch_produce_unsat_cores_late_set.smt2|smt2/z3_arch_produce_unsat_cores_late_set.expected.out||0|parser-runner,file-shell,interactive-shell|3|produce-unsat-cores-late-set|supported-error|options|cmd-context|late-option|none|solver:late-option-produce-unsat-cores|different|z0-uses-stable-late-option-diagnostic|false|false|exact
z3_arch_produce_unsat_assumptions_late_set|smt2/z3_arch_produce_unsat_assumptions_late_set.smt2|smt2/z3_arch_produce_unsat_assumptions_late_set.expected.out||0|parser-runner,file-shell,interactive-shell|3|produce-unsat-assumptions-late-set|supported-error|options|cmd-context|late-option|none|solver:late-option-produce-unsat-assumptions|different|z0-uses-stable-late-option-diagnostic|false|false|exact
z3_arch_reset_assertions_reopens_produce_flags|smt2/z3_arch_reset_assertions_reopens_produce_flags.smt2|smt2/z3_arch_reset_assertions_reopens_produce_flags.expected.out||0|parser-runner,file-shell,interactive-shell|12|reset-assertions-produce-flags|supported-success|options|none|reset-assertions-option-reopen|none|none|different|z0-uses-proof-skeleton-text|false|false|exact
z3_arch_reset_assertions_scope_replay|smt2/z3_arch_reset_assertions_scope_replay.smt2|smt2/z3_arch_reset_assertions_scope_replay.expected.out||0|parser-runner,file-shell,interactive-shell|8|reset-assertions-scope-replay|supported-success|Bool|none|reset-assertions-scope-depth-replay|none|none|same|none|false|false|exact
z3_arch_reset_reopens_produce_flags|smt2/z3_arch_reset_reopens_produce_flags.smt2|smt2/z3_arch_reset_reopens_produce_flags.expected.out||0|parser-runner,file-shell,interactive-shell|13|reset-produce-flags|supported-success|options|none|reset-option-reopen|none|none|different|z0-uses-proof-skeleton-text|false|false|exact
z3_arch_reset_clears_macro_env|smt2/z3_arch_reset_clears_macro_env.smt2|smt2/z3_arch_reset_clears_macro_env.expected.out||0|parser-runner,file-shell,interactive-shell|8|reset-clears-macro-env|supported-error|Bool|parser|reset-clears-declarations-macros|none|type:undeclared-symbol|same|none|false|false|exact
z3_arch_set_logic_ordering|smt2/z3_arch_set_logic_ordering.smt2|smt2/z3_arch_set_logic_ordering.expected.out||0|parser-runner,file-shell,interactive-shell|11|set-logic-ordering|supported-error|setup|cmd-context|late-logic-after-assertion|none|solver:set-logic-after-assertions|same|none|false|false|exact
z3_arch_set_logic_duplicate|smt2/z3_arch_set_logic_duplicate.smt2|smt2/z3_arch_set_logic_duplicate.expected.out||0|parser-runner,file-shell,interactive-shell|2|set-logic-duplicate|supported-error|setup|cmd-context|duplicate-logic|none|solver:logic-already-set|same|none|false|false|exact
z3_arch_unsupported_logic_recovery|smt2/z3_arch_unsupported_logic_recovery.smt2|smt2/z3_arch_unsupported_logic_recovery.expected.out||0|parser-runner,file-shell,interactive-shell|5|unsupported-logic-recovery|explicit-unsupported|setup|cmd-context|unsupported-logic-state-unchanged|unsupported-logic|unsupported:logic|different|phase-limited-logic|true|false|exact
z3_arch_set_logic_option_ordering|smt2/z3_arch_set_logic_option_ordering.smt2|smt2/z3_arch_set_logic_option_ordering.expected.out||0|parser-runner,file-shell,interactive-shell|11|set-logic-option-ordering|supported-success|options|none|setup-preassert-dynamic-options|none|none|different|z0-uses-print-success-for-command-side-effects|false|false|exact
z3_arch_exit_stops_runner|smt2/z3_arch_exit_stops_runner.smt2|smt2/z3_arch_exit_stops_runner.expected.out||0|parser-runner,file-shell,interactive-shell|3|exit-stops-runner|supported-success|command|none|exit-stops-runner|none|none|same|none|false|false|exact
z3_arch_error_recovery_unsupported_command|smt2/z3_arch_error_recovery_unsupported_command.smt2|smt2/z3_arch_error_recovery_unsupported_command.expected.out||0|parser-runner,file-shell,interactive-shell|3|error-recovery-unsupported-command|supported-error|command|parser|unsupported-command|unsupported-fragment|unsupported:unsupported-command|different|z0-prints-unsupported-diagnostic-in-regular-transcript|true|false|exact
z3_arch_error_recovery_parse_continued|smt2/z3_arch_error_recovery_parse_continued.smt2|smt2/z3_arch_error_recovery_parse_continued.expected.out||1|parser-runner,file-shell,interactive-shell|3|error-recovery-parse-continued|supported-error|command|parser|parse-error-continued|none|parse:push-count|different|z0-shell-reports-command-parse-error-exit|false|false|exact
z3_arch_error_recovery_immediate_exit|smt2/z3_arch_error_recovery_immediate_exit.smt2|smt2/z3_arch_error_recovery_immediate_exit.expected.out||1|parser-runner,file-shell,interactive-shell|4|error-recovery-immediate-exit|supported-error|options|runner|parse-error-immediate-exit|none|parse:push-count|same|none|false|false|exact
