Previously, "include" used locale-dependent decoding of source files, while the rest of Cryptol uses UTF8. This change makes "include" consistent with the rest of Cryptol, and adds a test that checks for malformed UTF8.