12 #ifndef CPROVER_SYMEX_PATH_SEARCH_H 13 #define CPROVER_SYMEX_PATH_SEARCH_H 124 bool execute(queuet::iterator state);
148 #endif // CPROVER_SYMEX_PATH_SEARCH_H
std::size_t number_of_infeasible_paths
property_mapt property_map
std::map< irep_idt, property_entryt > property_mapt
std::size_t number_of_locs
void set_branch_bound(int limit)
path_searcht(const namespacet &_ns)
virtual resultt operator()(const goto_functionst &goto_functions)
source_locationt source_location
std::size_t number_of_dropped_states
std::size_t number_of_paths
void initialize_property_map(const goto_functionst &goto_functions)
std::size_t number_of_feasible_paths
bool drop_state(const statet &state)
decide whether to drop a state
source_locationt last_source_location
bool is_not_reached() const
std::size_t number_of_steps
void set_time_limit(int limit)
void set_depth_limit(int limit)
bool is_feasible(statet &state)
std::list< statet > queuet
void set_unwind_limit(int limit)
std::size_t number_of_VCCs_after_simplification
std::size_t number_of_failed_properties
Safety Checker Interface.
State of path-based symbolic simulator.
void do_show_vcc(statet &state)
void set_context_bound(int limit)
absolute_timet start_time
enum path_searcht::search_heuristict search_heuristic
bool execute(queuet::iterator state)
void check_assertion(statet &state)
expanding_vectort< loc_datat > loc_data
std::size_t number_of_VCCs