TIMESTAMP = 1586295390
SHA256 (yices-2.6.2-src.tar.gz) = 1f205c056dd430f830c688fba6c87d8bd07bd8fa05f65936e12c27e71fa3576a
SIZE (yices-2.6.2-src.tar.gz) = 6014634