Suppress loading methods with nondet signatures

Author: reuk

src/java_bytecode/java_bytecode_convert_method.cpp

@@ -31,6 +31,7 @@ Author: Daniel Kroening, [email protected]
 #include <algorithm>
 #include <functional>
 #include <unordered_set>
+#include <regex>
 
 class patternt
 {
@@ -2531,6 +2532,29 @@ void java_bytecode_convert_method(
   safe_pointer<std::vector<irep_idt> > needed_methods,
   safe_pointer<std::set<irep_idt> > needed_classes)
 {
+  static const std::unordered_set<std::string> methods_to_ignore
+  {
+    "nondetBoolean",
+    "nondetByte",
+    "nondetChar",
+    "nondetShort",
+    "nondetInt",
+    "nondetLong",
+    "nondetFloat",
+    "nondetDouble",
+    "nondetWithNull",
+    "nondetWithoutNull",
+  };
+
+  if(std::regex_match(
+       id2string(class_symbol.name),
+       std::regex(".*org\\.cprover\\.CProver.*")) &&
+     methods_to_ignore.find(id2string(method.name))!=methods_to_ignore.end())
+  {
+    // Ignore these methods, rely on default stubbing behaviour.
+    return;
+  }
+
   java_bytecode_convert_methodt java_bytecode_convert_method(
     symbol_table,
     message_handler,