// S : tags   sym c todo  $TAGS
// S : expect --result valid
// S : cc     -o test.bc  $CC_OPT $file
// S : verify --symbolic --solver $solver --sequential -o ignore:control $V_OPT test.bc

#include <stdbool.h>

extern int __VERIFIER_nondet_int(void);
extern bool __VERIFIER_nondet_bool(void);

void f( int d ) {}

void main()
{
    bool c = __VERIFIER_nondet_bool();
    if ( c )
        f( 1 );
    else
        f( 2 );
}