NOTE: PLEASE VERIFY INTEGRITY AFTER DOWNLOAD: - SHA-256: eb5dab87eb050ddb23b2041e6e2727ad41a01bb2eeca82dccf1f4517e0114cc8 IF HASHES DO NOT MATCH, PLEASE RE-DOWNLOAD AND VERIFY AGAIN. ----------------------------------------------------------------------------------------- This artifact collects the examples used in the paper and provides themas a test suite. Each example is a separate program that can be used in anumber of ways. The program’s text is used in the paper. No results aregenerated. Each program takes a single input that controls which path throughthe program is taken and gives a single output that records which brancheswere taken. This allows them to be used for back-to-back testing withcompilers, interpreters, source-to-source translation, or dynamic analysistools. If the input/output relation changes, then transformation is buggyand unable to handle that kind of loop. They also have assertions that hold true only for valid paths throughthe program, making them ideal for testing with static analysis tools. Ifan assertion fails, it indicates a bug in the static analysis tool.To demonstrate how these can be used, we provide a setup to testCBMC.