Support Verifier.nondetObject #53

Verifier.nondetObject(Class<T> type, ObjectFactory<T> factory) (added to sv-benchmarks 2025-10) is not supported. It is used by the 14 tasks in java/objects/ (28 verification runs: 14 expected true, 14 expected false).

Semantics: the returned object is nondeterministic; the reference implementation just calls factory.createObject(). Tasks use it e.g. as Any o = Verifier.nondetObject(Any.class, new Factories.AnyFactory()); and branch on o != null, the object's dynamic type, or its fields.

• Analyse what the objects tasks require (null vs. non-null, dynamic type, field values)
• Decide on an approach, e.g. symbolic null/type choice + instrumenting the factory so object contents are handled implicitly (see notes in targets/sv-comp/todo.md)
• Witnesses: check how a nondetObject result is expressed in YAML 2.3 (function_return constraint), or whether this needs clarification upstream
• Measure on java/objects/ (no new wrong verdicts)

Target: final resubmission (Nov 17).