Error handling 

Unlike the C++ API, which reports errors by throwing exceptions, the C API cannot propagate exceptions across the language boundary. Instead of terminating the process when an error occurs, cvc5 C API functions record the error in thread-local state and return a default value (e.g., NULL , false , or 0 ).

After invoking a C API function, the caller can check whether it succeeded via cvc5_has_error() and retrieve the associated message via cvc5_get_error_message() . The error state is reset at the start of the next C API call that can raise an error, so it reflects the outcome of the most recent such call. The query functions cvc5_has_error() and cvc5_get_error_message() never modify the error state themselves; it can also be cleared explicitly via cvc5_reset_error() . For example:

Cvc5TermManager* tm = cvc5_term_manager_new();
Cvc5* cvc5 = cvc5_new(tm);
// Trigger an error by passing an invalid (NULL) argument.
cvc5_assert_formula(cvc5, NULL);
if (cvc5_has_error())
{
  fprintf(stderr, "cvc5 error: %s\n", cvc5_get_error_message());
}
cvc5_delete(cvc5);
cvc5_term_manager_delete(tm);

bool cvc5_has_error ( void ) 

Determine if an error occurred during the most recent cvc5 C API call on the current thread.

Rather than terminating the process, cvc5 C API functions record errors in thread-local state and return a default value (e.g., NULL , false , or 0 ) on failure. After invoking a C API function, the caller can use this function to check whether the call succeeded, and cvc5_get_error_message() to retrieve the associated error message.

The error state is reset at the beginning of each (non-query) C API call, thus it always reflects the outcome of the most recent such call. It can also be reset manually via cvc5_reset_error() .

Note

This function does not itself modify the error state.

Returns :

True if the most recent C API call on this thread resulted in an error.

const char * cvc5_get_error_message ( void ) 

Retrieve the error message associated with the most recent error on the current thread.

Note

This function does not itself modify the error state. The returned pointer is owned by cvc5 and is only valid until the next C API call on this thread.

Returns :

The message of the most recent error, or the empty string if no error has occurred (i.e., if cvc5_has_error() returns false).

void cvc5_reset_error ( void ) 

Reset the thread-local error state.

After calling this function, cvc5_has_error() returns false and cvc5_get_error_message() returns the empty string, until the next error occurs.