// S : tags   error c sym min  $TAGS
// S : expect --result error --location-comment ERROR
// S : cc     -o test.bc  $CC_OPT $file
// S : verify --symbolic --solver $solver $V_OPT test.bc

#include <stdbool.h>
#include <assert.h>

bool __VERIFIER_nondet_bool();

int main()
{
    bool a = __VERIFIER_nondet_bool();
    bool b = !a;

    assert( a == b ); /* ERROR */
}