#include "check_debug.h"
int a, b, c;
int frob(void) {
	if (a && b != 1)
		return;

	__smatch_value("a");
	if (b == 0 && c) {
		__smatch_value("a");
	}
	__smatch_value("a");
}
/*
 * check-name: Smatch implied #7
 * check-command: smatch -I.. sm_implied7.c
 *
 * check-output-start
sm_implied7.c:7 frob() a = s32min-s32max
sm_implied7.c:9 frob() a = 0
sm_implied7.c:11 frob() a = s32min-s32max
 * check-output-end
 */