| build_full_trace() const override | java_single_path_symex_checkert | virtual |
| build_shortest_trace() const override | java_single_path_symex_checkert | virtual |
| build_trace(const irep_idt &property_id) const override | java_single_path_symex_checkert | virtual |
| equation_output(const symex_bmct &symex, const symex_target_equationt &equation) | single_path_symex_only_checkert | protected |
| final_update_properties(propertiest &properties, std::unordered_set< irep_idt > &updated_properties) | single_path_symex_only_checkert | protectedvirtual |
| get_namespace() const override | single_path_symex_checkert | virtual |
| goto_model | single_path_symex_only_checkert | protected |
| guard_manager | single_path_symex_only_checkert | protected |
| has_finished_exploration(const propertiest &) | single_path_symex_only_checkert | protectedvirtual |
| incremental_goto_checkert()=delete | incremental_goto_checkert | |
| incremental_goto_checkert(const incremental_goto_checkert &)=delete | incremental_goto_checkert | |
| incremental_goto_checkert(const optionst &, ui_message_handlert &) | incremental_goto_checkert | protected |
| initialize_worklist() | single_path_symex_only_checkert | protectedvirtual |
| is_ready_to_decide(const symex_bmct &, const path_storaget::patht &) override | single_path_symex_checkert | protectedvirtual |
| java_single_path_symex_checkert(const optionst &options, ui_message_handlert &ui_message_handler, abstract_goto_modelt &goto_model) | java_single_path_symex_checkert | inline |
| log | incremental_goto_checkert | protected |
| ns | single_path_symex_only_checkert | protected |
| operator()(propertiest &) override | single_path_symex_checkert | virtual |
| options | incremental_goto_checkert | protected |
| output_error_witness(const goto_tracet &) override | single_path_symex_checkert | virtual |
| output_proof() override | single_path_symex_checkert | virtual |
| prepare_property_decider(propertiest &properties, symex_target_equationt &equation, goto_symex_property_decidert &property_decider) | single_path_symex_checkert | protectedvirtual |
| property_decider | single_path_symex_checkert | protected |
| report() | incremental_goto_checkert | inlinevirtual |
| resume_path(path_storaget::patht &path) | single_path_symex_only_checkert | protectedvirtual |
| run_property_decider(incremental_goto_checkert::resultt &result, propertiest &properties, goto_symex_property_decidert &property_decider, std::chrono::duration< double > solver_runtime) | single_path_symex_checkert | protectedvirtual |
| setup_symex(symex_bmct &symex) override | java_single_path_symex_checkert | inlinevirtual |
| single_path_symex_checkert(const optionst &options, ui_message_handlert &ui_message_handler, abstract_goto_modelt &goto_model) | single_path_symex_checkert | |
| single_path_symex_only_checkert(const optionst &options, ui_message_handlert &ui_message_handler, abstract_goto_modelt &goto_model) | single_path_symex_only_checkert | |
| symex_initialized | single_path_symex_checkert | protected |
| symex_runtime | single_path_symex_only_checkert | protected |
| symex_symbol_table | single_path_symex_only_checkert | protected |
| ui_message_handler | incremental_goto_checkert | protected |
| unwindset | single_path_symex_only_checkert | protected |
| update_properties(propertiest &properties, std::unordered_set< irep_idt > &updated_properties, const symex_target_equationt &equation) | single_path_symex_only_checkert | protectedvirtual |
| worklist | single_path_symex_only_checkert | protected |
| ~goto_trace_providert()=default | goto_trace_providert | virtual |
| ~incremental_goto_checkert()=default | incremental_goto_checkert | virtual |
| ~single_path_symex_checkert()=default | single_path_symex_checkert | virtual |
| ~single_path_symex_only_checkert()=default | single_path_symex_only_checkert | virtual |
| ~witness_providert()=default | witness_providert | virtual |