// this program fails on an assertion in
// testgen.c.out: /home/arvidj/dev/e-acsl/share/e-acsl/memory_model/e_acsl_bittree.c:341: __get_exact: Assertion `0' failed.
// when compiled with -e-acsl-full-mmodel
int main(void) {
	int a = 10, *p;
	p = &a;
	/*@assert \valid(p); */
	return 0;
}