Try 2

Author: Owen Jones

jbmc/src/java_bytecode/convert_java_nondet.cpp

@@ -90,9 +90,16 @@ static goto_programt::targett insert_nondet_init_code(
     code_declt decl(aux_symbol_expr);
     decl.add_source_location() = source_loc;
 
+    // Create goto instructions for declaring and deading aux_symbol
+    goto_programt aux_instructions;
+    code_blockt aux_block;
+    aux_block.move(decl);
+    goto_convert(
+      aux_block, symbol_table, aux_instructions, message_handler, mode);
+    CHECK_RETURN(aux_instructions.instructions.size() == 2);
+
     // Generate nondet init code
     code_blockt init_code;
-    init_code.add(decl);
 
     gen_nondet_init(
       aux_symbol_expr,
@@ -105,16 +112,27 @@ static goto_programt::targett insert_nondet_init_code(
       update_in_placet::NO_UPDATE_IN_PLACE);
 
     // Convert this code into goto instructions
-    goto_programt new_instructions;
+    goto_programt nondet_init_instructions;
     goto_convert(
-      init_code, symbol_table, new_instructions, message_handler, mode);
+      init_code, symbol_table, nondet_init_instructions, message_handler, mode);
 
-    // Insert the new instructions into the instruction list before target
-    goto_program.destructive_insert(target, new_instructions);
-    goto_program.update();
+    // First insert the declaration of aux_symbol at the front of
+    // nondet_init_instructions
+    goto_program.insert_before_swap(
+      nondet_init_instructions.instructions.begin(),
+      aux_instructions.instructions.front());
+
+    // Insert nondet_init_instructions into the instruction list before target
+    goto_program.destructive_insert(target, nondet_init_instructions);
 
-    // Replace op with aux symbol
+    // Replace op with aux symbol in target
     op = aux_symbol_expr;
+
+    // Finally insert the dead instruction for aux_symbol after target
+    goto_program.insert_after(target)->swap(
+      aux_instructions.instructions.back());
+
+    goto_program.update();
   }
 
   return next_instr;