Revert "Set max-nondet-string-length to 10000 by default"

[majakusber]

Reverts #4643 which introduced a default value for max-nondet-string-length. Instead, the value will remain unbounded in CBMC by default and a default value will be defined in test-gen only.

[tautschnig]

+100 for distinguishing a verification tool (CBMC) from a test-input generator. Thank you @svorenova!

[majakusber]

@tautschnig Thank you for pointing it out 👍
Test-gen PR is ready here: https://github.com/diffblue/test-gen/pull/3425

[allredj]

✔️
Passed Diffblue compatibility checks (cbmc commit: c35c16a).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/112055707

[martin-cs]

I realise this patch caused a disproportionate amount of discussion on it's way in and it is not my intent to replicate that but, @svorenova -- why did you decide to revert this?

[majakusber]

Because from the discussion it seemed like this is not desired for CBMC (or if it is, what the default should be), but it would be useful for test-gen. So basically to not limit CBMC users unnecessarily.

[martin-cs]

Fair. Thanks.