Non-deterministic left hand side in assignment with Java byte code about cbmc HOT 4 CLOSED

^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

nondetassign1$A.f() /* java::nondetassign1$A.f:()Lnondetassign1$A; */
        // 4 file nondetassign1.java line 16
        NONDET(bool) = (bool)1;
        // 5 file nondetassign1.java line 17
        nondetassign1$A.f:()Lnondetassign1$A;#return_value = (struct nondetassign1$A *)this;
        // 6 no location
        END_FUNCTION

^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

nondetassign1$A.g() /* java::nondetassign1$A.g:()V */
        // 10 no location
        struct java.lang.AssertionError *new_tmp0;
        // 11 file nondetassign1.java line 21
        local1i = (int)NONDET(bool);
        // 12 file nondetassign1.java line 22
        local2i = (int)NONDET(bool);
        // 13 file nondetassign1.java line 23
        IF $assertionsDisabled != FALSE THEN GOTO 1
        // 14 file nondetassign1.java line 23
        IF local1i == local2i THEN GOTO 1
        // 15 file nondetassign1.java line 23
        new_tmp0 = MALLOC(struct java.lang.AssertionError, 4);
        // 16 file nondetassign1.java line 23
        *new_tmp0 = { .@class_identifier="java::java.lang.AssertionError" };
        // 17 file nondetassign1.java line 23
        new_tmp0 . java.lang.AssertionError.<init>:()V();
        // 18 file nondetassign1.java line 23
        ASSERT false // assertion at file nondetassign1.java line 23
        // 19 file nondetassign1.java line 23
        THROW: throw(new_tmp0)
        // 20 file nondetassign1.java line 24
        // Labels: pc29
     1: dead new_tmp0;
        // 21 no location
        END_FUNCTION