Some SV-COMP benchmarks provide an existing implementation of

``__VERIFIER_assert()`` which conflicts with ours. Remove their
implementation if it is detected.

1 files changed, 10 insertions, 0 deletions

diff --git a/lib/Module/KModule.cpp b/lib/Module/KModule.cpp
index e22b3d24..f3487baf 100644
--- a/lib/Module/KModule.cpp
+++ b/lib/Module/KModule.cpp
@@ -374,6 +374,16 @@ void KModule::prepare(const Interpreter::ModuleOptions &opts,
 #else
     runtimeFileName += ".bca";
 #endif
+
+    // Some SV-COMP benchmarks might provide their own implementation of
+    // __VERIFIER functions. Remove them
+    llvm::Function* existingVERIFIER_assert = module->getFunction("__VERIFIER_assert");
+    if (existingVERIFIER_assert) {
+      existingVERIFIER_assert->deleteBody();
+      klee_warning("Deleting existing implementation of %s", existingVERIFIER_assert->getName().data());
+    }
+
+
     llvm::sys::path::append(LibPath, runtimeFileName.str());
     module = linkWithLibrary(module, LibPath.str());