Baltoli
commented
7 years ago Is this in fact necessary? A short investigation seemed to indicate that external functions can't be asserted over (i.e. we can say call(printf) as much as we like and it'll get satisfied, and similarly for pthread_create)
We obviously can't recurse into the definition of an external call, but it's perfectly reasonable to want to assert about calls to them - if the function is a declaration, its instruction graph should just be entry / exit rather than not existing at all.