48 if(prop_conv_solver !=
nullptr)
56 const auto any_failures = std::any_of(
59 [](
const std::pair<irep_idt, property_infot> &property) {
60 return property.second.status == property_statust::FAIL;
62 std::string status = any_failures ?
"FAILURE" :
"INCONCLUSIVE";
64 {{
labelt({
"incremental",
"status"}),
66 message_hander.
statistics() << incremental_status;
72 resultt result(resultt::progresst::DONE);
74 std::chrono::duration<double> solver_runtime(0);
99 <<
"Passing problem to "
103 const auto solver_start = std::chrono::steady_clock::now();
110 equation.convert_without_assertions(
126 [&properties](
const irep_idt &property_id) {
140 const auto solver_stop = std::chrono::steady_clock::now();
142 std::chrono::duration<double>(solver_stop - solver_start);
143 log.status() <<
"Runtime decision procedure: " << solver_runtime.count()
148 ? resultt::progresst::FOUND_FAIL
149 : resultt::progresst::DONE;
152 if(result.
progress == resultt::progresst::FOUND_FAIL)
206 if(
options.get_bool_option(
"beautify"))
void update_status_of_unknown_properties(propertiest &properties, std::unordered_set< irep_idt > &updated_properties)
Sets the property status of UNKNOWN properties to PASS.
void update_properties_status_from_symex_target_equation(propertiest &properties, std::unordered_set< irep_idt > &updated_properties, const symex_target_equationt &equation)
Sets property status to PASS for properties whose conditions are constant true in the equation.
void update_status_of_not_checked_properties(propertiest &properties, std::unordered_set< irep_idt > &updated_properties)
Sets the property status of NOT_CHECKED properties to PASS.
ssa_step_predicatet ssa_step_matches_failing_property(const irep_idt &property_id)
Returns a function that checks whether an SSA step is an assertion with property_id.
void output_graphml(const goto_tracet &goto_trace, const namespacet &ns, const optionst &options)
outputs an error witness in graphml format
void postprocess_equation(symex_bmct &symex, symex_target_equationt &equation, const optionst &options, const namespacet &ns, ui_message_handlert &ui_message_handler)
Post process the equation.
void setup_symex(symex_bmct &symex, const namespacet &ns, const optionst &options, ui_message_handlert &ui_message_handler)
Bounded Model Checking Utilities.
void build_goto_trace(const symex_target_equationt &target, ssa_step_predicatet is_last_step_to_keep, const decision_proceduret &decision_procedure, const namespacet &ns, goto_tracet &goto_trace)
Build a trace by going through the steps of target and stopping after the step matching a given condi...
Abstract interface to eager or lazy GOTO models.
resultt
Result of running the decision procedure.
static get_goto_functiont get_goto_function(abstract_goto_modelt &goto_model)
Return a function to get/load a goto function from the given goto model Create a default delegate to ...
incremental_goto_checkert()=delete
ui_message_handlert & ui_message_handler
Class that provides messages with a built-in verbosity 'level'.
mstreamt & statistics() const
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
goto_tracet build_trace(const irep_idt &) const override
Builds and returns the trace for the FAILed property with the given property_id.
bool current_equation_converted
guard_managert guard_manager
void output_proof() override
goto_tracet build_shortest_trace() const override
Builds and returns the trace up to the first failed property.
symex_bmc_incremental_one_loopt symex
bool initial_equation_generated
resultt operator()(propertiest &) override
Check whether the given properties with status NOT_CHECKED, UNKNOWN or properties newly discovered by...
void output_error_witness(const goto_tracet &) override
single_loop_incremental_symex_checkert(const optionst &options, ui_message_handlert &ui_message_handler, abstract_goto_modelt &goto_model)
goto_symex_property_decidert property_decider
goto_tracet build_full_trace() const override
Builds and returns the complete trace.
symex_target_equationt equation
bool full_equation_generated
const namespacet & get_namespace() const override
Returns the namespace associated with the traces.
abstract_goto_modelt & goto_model
symbol_tablet symex_symbol_table
A way of representing nested key/value data.
Counterexample Beautification.
bool has_properties_to_check(const propertiest &properties)
Return true if there as a property with NOT_CHECKED or UNKNOWN status.
bool is_property_to_check(property_statust status)
Return true if the status is NOT_CHECKED or UNKNOWN.
std::size_t count_properties(const propertiest &properties, property_statust status)
Return the number of properties with given status.
@ UNKNOWN
The checker was unable to determine the status of the property.
std::map< irep_idt, property_infot > propertiest
A map of property IDs to property infos.
void output_incremental_status(const propertiest &properties, messaget &message_hander)
Goto Checker using multi-path symbolic execution with incremental unwinding of a specified loop.
void revert_slice(symex_target_equationt &equation)
Undo whatever has been done by slice
std::unordered_set< irep_idt > updated_properties
Changed properties since the last call to incremental_goto_checkert::operator()
static structured_data_entryt data_node(const jsont &data)