Added these lines to centaur/esim/stv/stv2c/stv2c.lisp, avoiding
certification by ACL2 (but still allowing it for ACL2(h)):

; Added 10/17/2013 by Matt K.: Making this hons-only, because the proof of
; RETURN-TYPE-OF-STV2C-OUTPUT-STUFF-AUX seems to bog down in ACL2 as opposed to
; ACL2(h), perhaps because worse-than needs to be memoized.
; cert_param: (hons-only)


git-svn-id: http://acl2-books.googlecode.com/svn/trunk@2152 303c5b2c-9740-0410-b014-fd8f9db7be32
release aignet aiger file reader/writer

git-svn-id: http://acl2-books.googlecode.com/svn/trunk@2153 303c5b2c-9740-0410-b014-fd8f9db7be32