How will one make up a C program for the TASS model extractor?

== Input/Output ==

== Assumptions ==

== Assertion Language ==

 * forall/exists

== Loop invariants/co-invariants ==

== Library calls ==