; Error Line: 3
(declare a mpz)
(opaque a 1)