counterexample_found.h

Go to the documentation of this file.

/*******************************************************************\
 
Module: Counterexample Found
 
Author: Daniel Kroening, dkr@amazon.com
 
\*******************************************************************/
 
 
#ifndef CPROVER_CPROVER_COUNTEREXAMPLE_FOUND_H
#define CPROVER_CPROVER_COUNTEREXAMPLE_FOUND_H
 
#include "solver_types.h"
 
#include <unordered_set>
 
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 &);
 
class bv_pointers_widet;
 
void show_assignment(const bv_pointers_widet &);
 
#endif // CPROVER_CPROVER_COUNTEREXAMPLE_FOUND_H