Fix naming in variables for non-deterministic values

Author: Matthias Güdemann

jbmc/src/java_bytecode/java_entry_point.cpp

@@ -399,7 +399,7 @@ exprt::operandst java_build_arguments(
 
       init_code.add(
         generate_nondet_switch(
-          id2string(function.base_name) + "_" + std::to_string(param_number),
+          id2string(function.name) + "_" + std::to_string(param_number),
           cases,
           java_int_type(),
           function.location,

jbmc/src/java_bytecode/nondet.cpp

@@ -46,7 +46,7 @@ symbol_exprt generate_nondet_int(
   // Declare a symbol for the non deterministic integer.
   const symbol_exprt &nondet_symbol = get_fresh_aux_symbol(
                                         int_type,
-                                        name_prefix + "::nondet_int",
+                                        name_prefix,
                                         "nondet_int",
                                         source_location,
                                         ID_java,