Added comments to VC generation.
ACL2 generation from VC.  Starting running testcaeses.