counterexample_found.h File Reference

Counterexample Found. More...

#include "solver_types.h"
#include <unordered_set>

Include dependency graph for counterexample_found.h:

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

Go to the source code of this file.

Functions
std::optional< propertyt::tracet >	counterexample_found (const std::vector< framet > &, const workt &, const std::unordered_set< symbol_exprt, irep_hash > &address_taken, bool verbose, const namespacet &)
void	show_assignment (const bv_pointers_widet &)

Detailed Description

Counterexample Found.

Definition in file counterexample_found.h.

Function Documentation

counterexample_found()

std::optional<propertyt::tracet> counterexample_found	(	const std::vector< framet > &	frames,
		const workt &	work,
		const std::unordered_set< symbol_exprt, irep_hash > &	address_taken,
		bool	verbose,
		const namespacet &	ns
	)

Definition at line 173 of file counterexample_found.cpp.

show_assignment()

void show_assignment

(

const bv_pointers_widet &

solver

)

Definition at line 24 of file counterexample_found.cpp.