SMTChecker: Some (uncommon) valid values for selecting contracts are rejected as invalid

[blishko]

Model checker's CLI option to select contracts to be analyzed (--model-checker-contracts) rejects some valid values, for example if the path contains :.

[cameel]

Full context: #15880 (comment)

BTW, note that an empty source name is actually something that can happen. You can't do this on the CLI, but in Standard JSON source names can be arbitrary strings, including empty ones. There are some quirks around their behavior (#15747) and I think we'd be better off disallowing them, but for the time being they're technically valid.

And they can contain : and , even on the CLI (as long as the file system allows this). Only contract names are guaranteed to be identifiers.