12 #ifndef CPROVER_CBMC_COUNTEREXAMPLE_BEAUTIFICATION_H 13 #define CPROVER_CBMC_COUNTEREXAMPLE_BEAUTIFICATION_H 46 symex_target_equationt::SSA_stepst::const_iterator
failed;
49 #endif // CPROVER_CBMC_COUNTEREXAMPLE_BEAUTIFICATION_H Generate Equation using Symbolic Execution.
virtual ~counterexample_beautificationt()
void minimize(const exprt &expr, class prop_minimizet &prop_minimize)
Inheriting the interface of symex_targett this class represents the SSA form of the input program as ...
symex_target_equationt::SSA_stepst::const_iterator failed
Computes a satisfying assignment of minimal cost according to a const function using incremental SAT...
SAT-optimizer for minimizing expressions.
std::set< exprt > minimization_listt
symex_target_equationt::SSA_stepst::const_iterator get_failed_property(const prop_convt &prop_conv, const symex_target_equationt &equation)
Base class for all expressions.
void operator()(boolbvt &boolbv, const symex_target_equationt &equation)
void get_minimization_list(prop_convt &prop_conv, const symex_target_equationt &equation, minimization_listt &minimization_list)