#ifndef _cover_hpp_INCLUDED
#define _cover_hpp_INCLUDED

/*------------------------------------------------------------------------*/

// This header only provides the 'COVER' macro for testing.  It is unrelated
// to 'cover.cpp' which implements covered clause elimination (CCE), but we
// wanted to use the name base name in both cases.  More explanation on CCE
// is provided in 'cover.cpp'.

/*------------------------------------------------------------------------*/

// Coverage goal, used similar to 'assert' (but with flipped condition) and
// also included even if 'NDEBUG' is defined (in optimizing compilation).
//
// This should in essence not be used in production code.
//
// There seems to be no problem overloading the name 'COVER' of this macro
// with the constant 'COVER' of 'Internal::Mode' (surprisingly).

#define COVER(COND) \
do { \
  if (!(COND)) break; \
  fprintf (stderr, \
    "%scadical%s: %s:%d: %s: Coverage goal %s`%s'%s reached.\n", \
    terr.bold_code (), terr.normal_code (), \
    __FUNCTION__, __LINE__, __FILE__, \
    terr.green_code (), # COND, terr.normal_code ()); \
  fflush (stderr); \
  abort (); \
} while (0)

#endif