Clean-up in gen_nondet_instruction_info

NathanJPhillips · Jul 17, 2018 · e4b8c44 · e4b8c44
1 parent 1f62596
commit e4b8c44
Showing 1 changed file with 3 additions and 4 deletions.
diff --git a/jbmc/src/java_bytecode/replace_java_nondet.cpp b/jbmc/src/java_bytecode/replace_java_nondet.cpp
@@ -93,10 +93,9 @@ get_nondet_instruction_info(const goto_programt::const_targett &instr)
     return nondet_instruction_infot();
   }
   const auto &code = instr->code;
-  if(code.get_statement() != ID_function_call)
-  {
-    return nondet_instruction_infot();
-  }
+  INVARIANT(
+    code.get_statement() == ID_function_call,
+    "function_call should have ID_function_call");
   const auto &function_call = to_code_function_call(code);
   return is_nondet_returning_object(function_call);
 }