Enhance replace java nondet to deal with non-trivial goto

[JohnDumbell]

This is focused mostly around check_and_replace_target in replace_java_nondet.cpp.

The code attempts to find all instructions that's been generated between a org.cprover.CProver.nondetX() call and its assignment (or use) and then skips everything and replaces the call with just a NONDET statement of the specified type. This works in most basic situations, but if the goto code has any sort of complication which moves the final value between variables, like this:

temp0 = CProver.nonDetInt()
temp1 = Integer.unbox(temp0)
return_variable = temp1

Then it can't work out what to replace and aborts. There are a set of examples and tests in #2263 which highlight how this can be caused. Simplest way is when the return value of the Java CProver.nondetX gets boxed/unboxed before being assigned or returned.

(Probably needs something a little more robust than just fixing the examples in the tests.)