diff --git a/src/java_bytecode/java_object_factory.cpp b/src/java_bytecode/java_object_factory.cpp index 55dfc96931f..36fa819c979 100644 --- a/src/java_bytecode/java_object_factory.cpp +++ b/src/java_bytecode/java_object_factory.cpp @@ -464,19 +464,12 @@ void java_object_factoryt::gen_nondet_init( } else { - code_assignt assign; - assign.lhs()=expr; + exprt rhs=type.id()==ID_c_bool? + get_nondet_bool(type): + side_effect_expr_nondett(type); + code_assignt assign(expr, rhs); assign.add_source_location()=loc; - if(type.id()==ID_c_bool) - { - assign.rhs()=get_nondet_bool(type); - } - else - { - assign.rhs()=side_effect_expr_nondett(type); - } - init_code.copy_to_operands(assign); } }