Goto Verifier for stopping at the first failing property and localizing the fault. More...

#include "bmc_util.h"
#include "fault_localization_provider.h"
#include "goto_verifier.h"

Include dependency graph for stop_on_fail_verifier_with_fault_localization.h:

This graph shows which files directly or indirectly include this file:

Classes
class	stop_on_fail_verifier_with_fault_localizationt< incremental_goto_checkerT >
	Stops when the first failing property is found and localizes the fault Requires an incremental goto checker that is a `goto_trace_providert` and `fault_localization_providert`. More...

Detailed Description

Goto Verifier for stopping at the first failing property and localizing the fault.

Classes