added a test case to make sure I understand Zvonimir's email about a SMACK macro being defined when smack is parsing C code