Produce __VERIFIER_nondet_* harnesses for determistic replay

[sim642]

No description provided.

[rmonat]

Would it also allow you to try out multiple seeds within the 15 minutes limit?

[sim642]

sv-sanitizers already can execute the program multiple times (until one finds a violation). And each one initializes randomness differently:

sv-sanitizers/sv-comp.c

Lines 8 to 12 in 54c2e1e

	// can't srand at the beginning of main, so GCC constructor
	__attribute__((constructor)) static void __sv_sanitizers_srand() {
	// getpid to have different seeds for processes created during the same second
	srand(time(NULL) ^ getpid());
	}

It's just that once a violation is found, the seed and the corresponding values returned by all nondets cannot be inspected to deterministically replay the violation (some SV-COMP tools can do it and witness2test also builds on this idea I think).