On 06/14/2017 07:02 PM, Dan Williams wrote:
> On Wed, Jun 14, 2017 at 9:53 AM, Vlastimil Babka <vbabka@suse.cz> wrote:
> 
> Can you share the test-thp.c so I can add this to my test collection?

Attached.

> I'm assuming cbmc is "Bounded Model Checker for C/C++"?

Yes. This blog from Paul inspired me:
http://paulmck.livejournal.com/38997.html

Works nicely, just if it finds a bug, the counterexamples are a bit of
PITA to decipher :)

Vlastimil