diff --git a/include/klee/Core/Interpreter.h b/include/klee/Core/Interpreter.h
index 5cd177ca00..8d47552eeb 100644
--- a/include/klee/Core/Interpreter.h
+++ b/include/klee/Core/Interpreter.h
@@ -32,6 +32,7 @@ class BasicBlock;
 class Function;
 class LLVMContext;
 class Module;
+class Type;
 class raw_ostream;
 class raw_fd_ostream;
 } // namespace llvm
@@ -61,6 +62,13 @@ class InterpreterHandler {
                                const char *suffix) = 0;
 };
 
+enum class MockStrategy {
+  None,          // No mocks are generated
+  Naive,         // For each function call new symbolic value is generated
+  Deterministic, // Each function is treated as uninterpreted function in SMT.
+                 // Compatible with Z3 solver only
+};
+
 class Interpreter {
 public:
   enum class GuidanceKind {
@@ -77,6 +85,8 @@ class Interpreter {
     std::string LibraryDir;
     std::string EntryPoint;
     std::string OptSuffix;
+    std::string MainCurrentName;
+    std::string MainNameAfterMock;
     bool Optimize;
     bool Simplify;
     bool CheckDivZero;
@@ -86,13 +96,16 @@ class Interpreter {
 
     ModuleOptions(const std::string &_LibraryDir,
                   const std::string &_EntryPoint, const std::string &_OptSuffix,
-                  bool _Optimize, bool _Simplify, bool _CheckDivZero,
-                  bool _CheckOvershift, bool _WithFPRuntime,
-                  bool _WithPOSIXRuntime)
+                  const std::string &_MainCurrentName,
+                  const std::string &_MainNameAfterMock, bool _Optimize,
+                  bool _Simplify, bool _CheckDivZero, bool _CheckOvershift,
+                  bool _WithFPRuntime, bool _WithPOSIXRuntime)
         : LibraryDir(_LibraryDir), EntryPoint(_EntryPoint),
-          OptSuffix(_OptSuffix), Optimize(_Optimize), Simplify(_Simplify),
-          CheckDivZero(_CheckDivZero), CheckOvershift(_CheckOvershift),
-          WithFPRuntime(_WithFPRuntime), WithPOSIXRuntime(_WithPOSIXRuntime) {}
+          OptSuffix(_OptSuffix), MainCurrentName(_MainCurrentName),
+          MainNameAfterMock(_MainNameAfterMock), Optimize(_Optimize),
+          Simplify(_Simplify), CheckDivZero(_CheckDivZero),
+          CheckOvershift(_CheckOvershift), WithFPRuntime(_WithFPRuntime),
+          WithPOSIXRuntime(_WithPOSIXRuntime) {}
   };
 
   enum LogType {
@@ -110,10 +123,11 @@ class Interpreter {
     unsigned MakeConcreteSymbolic;
     GuidanceKind Guidance;
     nonstd::optional<SarifReport> Paths;
+    enum MockStrategy MockStrategy;
 
     InterpreterOptions(nonstd::optional<SarifReport> Paths)
         : MakeConcreteSymbolic(false), Guidance(GuidanceKind::NoGuidance),
-          Paths(std::move(Paths)) {}
+          Paths(std::move(Paths)), MockStrategy(MockStrategy::None) {}
   };
 
 protected:
@@ -142,7 +156,11 @@ class Interpreter {
             const ModuleOptions &opts,
             const std::unordered_set<std::string> &mainModuleFunctions,
             const std::unordered_set<std::string> &mainModuleGlobals,
-            std::unique_ptr<InstructionInfoTable> origInfos) = 0;
+            std::unique_ptr<InstructionInfoTable> origInfos,
+            const std::set<std::string> &ignoredExternals) = 0;
+
+  virtual std::map<std::string, llvm::Type *>
+  getAllExternals(const std::set<std::string> &ignoredExternals) = 0;
 
   // supply a tree stream writer which the interpreter will use
   // to record the concrete path (as a stream of '0' and '1' bytes).
diff --git a/include/klee/Expr/IndependentSet.h b/include/klee/Expr/IndependentSet.h
index 9173d90678..0027228cf4 100644
--- a/include/klee/Expr/IndependentSet.h
+++ b/include/klee/Expr/IndependentSet.h
@@ -86,6 +86,7 @@ class IndependentElementSet {
   constraints_ty exprs; // All expressions (constraints) that are associated
                         // with this factor
   SymcreteOrderedSet symcretes; // All symcretes associated with this factor
+  std::set<std::string> uninterpretedFunctions;
 
   IndependentElementSet();
   IndependentElementSet(ref<Expr> e);
diff --git a/include/klee/Expr/SourceBuilder.h b/include/klee/Expr/SourceBuilder.h
index 7b57e2f8c9..827dc092e9 100644
--- a/include/klee/Expr/SourceBuilder.h
+++ b/include/klee/Expr/SourceBuilder.h
@@ -5,6 +5,8 @@
 #include "klee/Expr/SymbolicSource.h"
 #include "klee/Module/KModule.h"
 
+#include "llvm/IR/Function.h"
+
 namespace klee {
 
 class SourceBuilder {
@@ -28,6 +30,12 @@ class SourceBuilder {
   static ref<SymbolicSource> value(const llvm::Value &_allocSite, int _index,
                                    KModule *km);
   static ref<SymbolicSource> irreproducible(const std::string &name);
+  static ref<SymbolicSource> mockNaive(const KModule *kModule,
+                                       const llvm::Function &kFunction,
+                                       unsigned version);
+  static ref<SymbolicSource>
+  mockDeterministic(const KModule *kModule, const llvm::Function &kFunction,
+                    const std::vector<ref<Expr>> &args);
 };
 
 }; // namespace klee
diff --git a/include/klee/Expr/SymbolicSource.h b/include/klee/Expr/SymbolicSource.h
index be65580f7b..2f52844268 100644
--- a/include/klee/Expr/SymbolicSource.h
+++ b/include/klee/Expr/SymbolicSource.h
@@ -17,10 +17,12 @@ DISABLE_WARNING_POP
 
 namespace klee {
 
+class Expr;
 class Array;
 class Expr;
 class ConstantExpr;
 class KModule;
+struct KFunction;
 
 class SymbolicSource {
 protected:
@@ -41,7 +43,9 @@ class SymbolicSource {
     LazyInitializationSize,
     Instruction,
     Argument,
-    Irreproducible
+    Irreproducible,
+    MockNaive,
+    MockDeterministic
   };
 
 public:
@@ -361,6 +365,58 @@ class IrreproducibleSource : public SymbolicSource {
   }
 };
 
+class MockSource : public SymbolicSource {
+public:
+  const KModule *km;
+  const llvm::Function &function;
+  MockSource(const KModule *_km, const llvm::Function &_function)
+      : km(_km), function(_function) {}
+
+  static bool classof(const SymbolicSource *S) {
+    return S->getKind() == Kind::MockNaive ||
+           S->getKind() == Kind::MockDeterministic;
+  }
+};
+
+class MockNaiveSource : public MockSource {
+public:
+  const unsigned version;
+
+  MockNaiveSource(const KModule *km, const llvm::Function &function,
+                  unsigned _version)
+      : MockSource(km, function), version(_version) {}
+
+  Kind getKind() const override { return Kind::MockNaive; }
+  std::string getName() const override { return "mockNaive"; }
+
+  static bool classof(const SymbolicSource *S) {
+    return S->getKind() == Kind::MockNaive;
+  }
+
+  unsigned computeHash() override;
+
+  int internalCompare(const SymbolicSource &b) const override;
+};
+
+class MockDeterministicSource : public MockSource {
+public:
+  const std::vector<ref<Expr>> args;
+
+  MockDeterministicSource(const KModule *_km, const llvm::Function &_function,
+                          const std::vector<ref<Expr>> &_args);
+
+  Kind getKind() const override { return Kind::MockDeterministic; }
+  std::string getName() const override { return "mockDeterministic"; }
+
+  static bool classof(const SymbolicSource *S) {
+    return S->getKind() == Kind::MockDeterministic;
+  }
+
+  unsigned computeHash() override;
+
+  int internalCompare(const SymbolicSource &b) const override;
+};
+
 } // namespace klee
 
 #endif /* KLEE_SYMBOLICSOURCE_H */
diff --git a/include/klee/klee.h b/include/klee/klee.h
index 9c40ef335c..5995ff2e24 100644
--- a/include/klee/klee.h
+++ b/include/klee/klee.h
@@ -201,5 +201,6 @@ long double klee_rintl(long double d);
 // stdin/stdout
 void klee_init_env(int *argcPtr, char ***argvPtr);
 void check_stdin_read();
+void *__klee_wrapped_malloc(size_t size);
 
 #endif /* KLEE_H */
diff --git a/lib/Core/CMakeLists.txt b/lib/Core/CMakeLists.txt
index edcd9eeb5b..7d2aa7d74e 100644
--- a/lib/Core/CMakeLists.txt
+++ b/lib/Core/CMakeLists.txt
@@ -22,6 +22,7 @@ add_library(kleeCore
   Memory.cpp
   MemoryManager.cpp
   PForest.cpp
+  MockBuilder.cpp
   PTree.cpp
   Searcher.cpp
   SeedInfo.cpp
diff --git a/lib/Core/ExecutionState.cpp b/lib/Core/ExecutionState.cpp
index 9288283849..f5fcdd6857 100644
--- a/lib/Core/ExecutionState.cpp
+++ b/lib/Core/ExecutionState.cpp
@@ -18,6 +18,7 @@
 #include "klee/Module/KInstruction.h"
 #include "klee/Module/KModule.h"
 #include "klee/Support/Casting.h"
+#include "klee/Support/ErrorHandling.h"
 #include "klee/Support/OptionCategories.h"
 
 #include "klee/Support/CompilerWarning.h"
diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp
index d219f82761..5a1c3c2721 100644
--- a/lib/Core/Executor.cpp
+++ b/lib/Core/Executor.cpp
@@ -20,6 +20,7 @@
 #include "ImpliedValue.h"
 #include "Memory.h"
 #include "MemoryManager.h"
+#include "MockBuilder.h"
 #include "PForest.h"
 #include "PTree.h"
 #include "Searcher.h"
@@ -465,6 +466,11 @@ Executor::Executor(LLVMContext &ctx, const InterpreterOptions &opts,
 
   guidanceKind = opts.Guidance;
 
+  if (CoreSolverToUse != Z3_SOLVER &&
+      interpreterOpts.MockStrategy == MockStrategy::Deterministic) {
+    klee_error("Deterministic mocks can be generated with Z3 solver only.\n");
+  }
+
   const time::Span maxTime{MaxTime};
   if (maxTime)
     timers.add(std::make_unique<Timer>(maxTime, [&] {
@@ -530,10 +536,22 @@ Executor::setModule(std::vector<std::unique_ptr<llvm::Module>> &userModules,
                     const ModuleOptions &opts,
                     const std::unordered_set<std::string> &mainModuleFunctions,
                     const std::unordered_set<std::string> &mainModuleGlobals,
-                    std::unique_ptr<InstructionInfoTable> origInfos) {
+                    std::unique_ptr<InstructionInfoTable> origInfos,
+                    const std::set<std::string> &ignoredExternals) {
   assert(!kmodule && !userModules.empty() &&
          "can only register one module"); // XXX gross
 
+  if (ExternalCalls == ExternalCallPolicy::All &&
+      interpreterOpts.MockStrategy != MockStrategy::None) {
+    llvm::Function *mainFn =
+        userModules.front()->getFunction(opts.MainCurrentName);
+    if (!mainFn) {
+      klee_error("Entry function '%s' not found in module.",
+                 opts.MainCurrentName.c_str());
+    }
+    mainFn->setName(opts.MainNameAfterMock);
+  }
+
   kmodule = std::make_unique<KModule>();
 
   // 1.) Link the modules together && 2.) Apply different instrumentation
@@ -558,6 +576,42 @@ Executor::setModule(std::vector<std::unique_ptr<llvm::Module>> &userModules,
     kmodule->instrument(opts);
   }
 
+  if (ExternalCalls == ExternalCallPolicy::All &&
+      interpreterOpts.MockStrategy != MockStrategy::None) {
+    // TODO: move this to function
+    std::map<std::string, llvm::Type *> externals =
+        getAllExternals(ignoredExternals);
+    MockBuilder builder(kmodule->module.get(), opts.MainCurrentName,
+                        opts.MainNameAfterMock, externals);
+    std::unique_ptr<llvm::Module> mockModule = builder.build();
+    if (!mockModule) {
+      klee_error("Unable to generate mocks");
+    }
+    // TODO: change this to bc file
+    std::unique_ptr<llvm::raw_fd_ostream> f(
+        interpreterHandler->openOutputFile("externals.ll"));
+    auto mainFn = mockModule->getFunction(opts.MainCurrentName);
+    mainFn->setName(opts.EntryPoint);
+    *f << *mockModule;
+    mainFn->setName(opts.MainCurrentName);
+
+    std::vector<std::unique_ptr<llvm::Module>> mockModules;
+    mockModules.push_back(std::move(mockModule));
+    kmodule->link(mockModules, 0);
+
+    for (auto &global : kmodule->module->globals()) {
+      if (global.isDeclaration()) {
+        llvm::Constant *zeroInitializer =
+            llvm::Constant::getNullValue(global.getValueType());
+        if (!zeroInitializer) {
+          klee_error("Unable to get zero initializer for '%s'",
+                     global.getName().str().c_str());
+        }
+        global.setInitializer(zeroInitializer);
+      }
+    }
+  }
+
   // 3.) Optimise and prepare for KLEE
 
   // Create a list of functions that should be preserved if used
@@ -609,6 +663,37 @@ Executor::setModule(std::vector<std::unique_ptr<llvm::Module>> &userModules,
   return kmodule->module.get();
 }
 
+std::map<std::string, llvm::Type *>
+Executor::getAllExternals(const std::set<std::string> &ignoredExternals) {
+  std::map<std::string, llvm::Type *> externals;
+  for (const auto &f : kmodule->module->functions()) {
+    if (f.isDeclaration() && !f.use_empty() &&
+        !ignoredExternals.count(f.getName().str()))
+      // NOTE: here we detect all the externals, even linked.
+      externals.insert(std::make_pair(f.getName(), f.getFunctionType()));
+  }
+
+  for (const auto &global : kmodule->module->globals()) {
+    if (global.isDeclaration() &&
+        !ignoredExternals.count(global.getName().str()))
+      externals.insert(std::make_pair(global.getName(), global.getValueType()));
+  }
+
+  for (const auto &alias : kmodule->module->aliases()) {
+    auto it = externals.find(alias.getName().str());
+    if (it != externals.end()) {
+      externals.erase(it);
+    }
+  }
+
+  for (const auto &e : externals) {
+    klee_message("Mocking external %s %s",
+                 e.second->isFunctionTy() ? "function" : "variable",
+                 e.first.c_str());
+  }
+  return externals;
+}
+
 Executor::~Executor() {
   delete typeSystemManager;
   delete externalDispatcher;
@@ -6439,6 +6524,48 @@ void Executor::executeMakeSymbolic(ExecutionState &state,
   }
 }
 
+void Executor::executeMakeMock(ExecutionState &state, KInstruction *target,
+                               std::vector<ref<Expr>> &arguments) {
+  KFunction *kf = target->parent->parent;
+  std::string name = "@call_" + kf->getName().str();
+  uint64_t width =
+      kmodule->targetData->getTypeSizeInBits(kf->function->getReturnType());
+  KType *type = typeSystemManager->getWrappedType(
+      llvm::PointerType::get(kf->function->getReturnType(),
+                             kmodule->targetData->getAllocaAddrSpace()));
+
+  IDType moID;
+  bool success = state.addressSpace.resolveOne(cast<ConstantExpr>(arguments[0]),
+                                               type, moID);
+  assert(success && "memory object for mock should already be allocated");
+  const MemoryObject *mo = state.addressSpace.findObject(moID).first;
+  assert(mo && "memory object for mock should already be allocated");
+  mo->setName(name);
+
+  ref<SymbolicSource> source;
+  switch (interpreterOpts.MockStrategy) {
+  case MockStrategy::None:
+    klee_error("klee_make_mock is not allowed when mock strategy is none");
+    break;
+  case MockStrategy::Naive:
+    source = SourceBuilder::mockNaive(kmodule.get(), *kf->function,
+                                      updateNameVersion(state, name));
+    break;
+  case MockStrategy::Deterministic:
+    std::vector<ref<Expr>> args(kf->numArgs);
+    for (size_t i = 0; i < kf->numArgs; i++) {
+      args[i] = getArgumentCell(state, kf, i).value;
+    }
+    source =
+        SourceBuilder::mockDeterministic(kmodule.get(), *kf->function, args);
+    break;
+  }
+  executeMakeSymbolic(state, mo, type, source, false);
+  const ObjectState *os = state.addressSpace.findObject(mo->id).second;
+  auto result = os->read(0, width);
+  bindLocal(target, state, result);
+}
+
 /***/
 
 ExecutionState *Executor::formState(Function *f) {
diff --git a/lib/Core/Executor.h b/lib/Core/Executor.h
index 582c22f0f0..3575f64f3b 100644
--- a/lib/Core/Executor.h
+++ b/lib/Core/Executor.h
@@ -420,6 +420,9 @@ class Executor : public Interpreter {
                            KType *type, const ref<SymbolicSource> source,
                            bool isLocal);
 
+  void executeMakeMock(ExecutionState &state, KInstruction *target,
+                       std::vector<ref<Expr>> &arguments);
+
   void updateStateWithSymcretes(ExecutionState &state,
                                 const Assignment &assignment);
 
@@ -724,7 +727,11 @@ class Executor : public Interpreter {
             const ModuleOptions &opts,
             const std::unordered_set<std::string> &mainModuleFunctions,
             const std::unordered_set<std::string> &mainModuleGlobals,
-            std::unique_ptr<InstructionInfoTable> origInfos) override;
+            std::unique_ptr<InstructionInfoTable> origInfos,
+            const std::set<std::string> &ignoredExternals) override;
+
+  std::map<std::string, llvm::Type *>
+  getAllExternals(const std::set<std::string> &ignoredExternals) override;
 
   void useSeeds(const std::vector<struct KTest *> *seeds) override {
     usingSeeds = seeds;
diff --git a/lib/Core/MockBuilder.cpp b/lib/Core/MockBuilder.cpp
new file mode 100644
index 0000000000..1c430e9fa0
--- /dev/null
+++ b/lib/Core/MockBuilder.cpp
@@ -0,0 +1,172 @@
+#include "MockBuilder.h"
+
+#include "klee/Support/ErrorHandling.h"
+
+#include "klee/Support/CompilerWarning.h"
+DISABLE_WARNING_PUSH
+DISABLE_WARNING_DEPRECATED_DECLARATIONS
+#include "llvm/IR/IRBuilder.h"
+#include "llvm/IR/Module.h"
+DISABLE_WARNING_POP
+
+#include <memory>
+
+namespace klee {
+
+MockBuilder::MockBuilder(const llvm::Module *initModule,
+                         std::string mockEntrypoint, std::string userEntrypoint,
+                         std::map<std::string, llvm::Type *> externals)
+    : userModule(initModule), externals(std::move(externals)),
+      mockEntrypoint(std::move(mockEntrypoint)),
+      userEntrypoint(std::move(userEntrypoint)) {}
+
+std::unique_ptr<llvm::Module> MockBuilder::build() {
+  initMockModule();
+  buildMockMain();
+  buildExternalFunctionsDefinitions();
+  return std::move(mockModule);
+}
+
+void MockBuilder::initMockModule() {
+  mockModule = std::make_unique<llvm::Module>(userModule->getName().str() +
+                                                  "__klee_externals",
+                                              userModule->getContext());
+  mockModule->setTargetTriple(userModule->getTargetTriple());
+  mockModule->setDataLayout(userModule->getDataLayout());
+  builder = std::make_unique<llvm::IRBuilder<>>(mockModule->getContext());
+}
+
+// Set up entrypoint in new module. Here we'll define external globals and then
+// call user's entrypoint.
+void MockBuilder::buildMockMain() {
+  llvm::Function *userMainFn = userModule->getFunction(userEntrypoint);
+  if (!userMainFn) {
+    klee_error("Entry function '%s' not found in module.",
+               userEntrypoint.c_str());
+  }
+  mockModule->getOrInsertFunction(mockEntrypoint, userMainFn->getFunctionType(),
+                                  userMainFn->getAttributes());
+  llvm::Function *mockMainFn = mockModule->getFunction(mockEntrypoint);
+  if (!mockMainFn) {
+    klee_error("Entry function '%s' not found in module.",
+               mockEntrypoint.c_str());
+  }
+  auto globalsInitBlock =
+      llvm::BasicBlock::Create(mockModule->getContext(), "entry", mockMainFn);
+  builder->SetInsertPoint(globalsInitBlock);
+  // Define all the external globals
+  buildExternalGlobalsDefinitions();
+
+  auto userMainCallee = mockModule->getOrInsertFunction(
+      userEntrypoint, userMainFn->getFunctionType());
+  std::vector<llvm::Value *> args;
+  args.reserve(userMainFn->arg_size());
+  for (auto it = mockMainFn->arg_begin(); it != mockMainFn->arg_end(); it++) {
+    args.push_back(it);
+  }
+  auto callUserMain = builder->CreateCall(userMainCallee, args);
+  builder->CreateRet(callUserMain);
+}
+
+void MockBuilder::buildExternalGlobalsDefinitions() {
+  for (const auto &it : externals) {
+    if (it.second->isFunctionTy()) {
+      continue;
+    }
+    const std::string &extName = it.first;
+    llvm::Type *type = it.second;
+    mockModule->getOrInsertGlobal(extName, type);
+    auto *global = mockModule->getGlobalVariable(extName);
+    if (!global) {
+      klee_error("Unable to add global variable '%s' to module",
+                 extName.c_str());
+    }
+    global->setLinkage(llvm::GlobalValue::ExternalLinkage);
+    if (!type->isSized()) {
+      continue;
+    }
+
+    auto *zeroInitializer = llvm::Constant::getNullValue(it.second);
+    if (!zeroInitializer) {
+      klee_error("Unable to get zero initializer for '%s'", extName.c_str());
+    }
+    global->setInitializer(zeroInitializer);
+    buildCallKleeMakeSymbol("klee_make_symbolic", global, type,
+                            "@obj_" + extName);
+  }
+}
+
+void MockBuilder::buildExternalFunctionsDefinitions() {
+  for (const auto &it : externals) {
+    if (!it.second->isFunctionTy()) {
+      continue;
+    }
+    std::string extName = it.first;
+    auto *type = llvm::cast<llvm::FunctionType>(it.second);
+    mockModule->getOrInsertFunction(extName, type);
+    llvm::Function *func = mockModule->getFunction(extName);
+    if (!func) {
+      klee_error("Unable to find function '%s' in module", extName.c_str());
+    }
+    if (!func->empty()) {
+      continue;
+    }
+    auto *BB =
+        llvm::BasicBlock::Create(mockModule->getContext(), "entry", func);
+    builder->SetInsertPoint(BB);
+
+    if (!func->getReturnType()->isSized()) {
+      builder->CreateRet(nullptr);
+      continue;
+    }
+
+    auto *mockReturnValue =
+        builder->CreateAlloca(func->getReturnType(), nullptr);
+    buildCallKleeMakeSymbol("klee_make_mock", mockReturnValue,
+                            func->getReturnType(), "@call_" + extName);
+#if LLVM_VERSION_CODE >= LLVM_VERSION(14, 0)
+    auto *loadInst =
+        builder->CreateLoad(func->getReturnType(), mockReturnValue, "klee_var");
+#else
+    auto *loadInst = builder->CreateLoad(mockReturnValue, "klee_var");
+#endif
+    builder->CreateRet(loadInst);
+  }
+}
+
+void MockBuilder::buildCallKleeMakeSymbol(const std::string &klee_function_name,
+                                          llvm::Value *source, llvm::Type *type,
+                                          const std::string &symbol_name) {
+  auto *klee_mk_symb_type = llvm::FunctionType::get(
+      llvm::Type::getVoidTy(mockModule->getContext()),
+      {llvm::Type::getInt8PtrTy(mockModule->getContext()),
+       llvm::Type::getInt64Ty(mockModule->getContext()),
+       llvm::Type::getInt8PtrTy(mockModule->getContext())},
+      false);
+  auto kleeMakeSymbolCallee =
+      mockModule->getOrInsertFunction(klee_function_name, klee_mk_symb_type);
+  auto bitcastInst = builder->CreateBitCast(
+      source, llvm::Type::getInt8PtrTy(mockModule->getContext()));
+  auto str_name = builder->CreateGlobalString(symbol_name);
+  auto mockReturnValue = builder->CreateAlloca(str_name->getType());
+  builder->CreateStore(str_name, mockReturnValue);
+  auto mockStr = builder->CreateLoad(str_name->getType(), mockReturnValue);
+  auto bitcastStr = builder->CreateBitCast(
+      mockStr, llvm::Type::getInt8PtrTy(mockModule->getContext()));
+#if LLVM_VERSION_CODE >= LLVM_VERSION(14, 0)
+  auto ptrTy = llvm::Type::getInt8Ty(mockModule->getContext());
+  auto gep = builder->CreateConstInBoundsGEP1_64(ptrTy, bitcastStr, 0);
+#else
+  auto gep = builder->CreateConstInBoundsGEP1_64(bitcastStr, 0);
+#endif
+  builder->CreateCall(
+      kleeMakeSymbolCallee,
+      {bitcastInst,
+       llvm::ConstantInt::get(
+           mockModule->getContext(),
+           llvm::APInt(64, mockModule->getDataLayout().getTypeStoreSize(type),
+                       false)),
+       gep});
+}
+
+} // namespace klee
diff --git a/lib/Core/MockBuilder.h b/lib/Core/MockBuilder.h
new file mode 100644
index 0000000000..eff3fdeb02
--- /dev/null
+++ b/lib/Core/MockBuilder.h
@@ -0,0 +1,44 @@
+#ifndef KLEE_MOCKBUILDER_H
+#define KLEE_MOCKBUILDER_H
+
+#include "klee/Support/CompilerWarning.h"
+DISABLE_WARNING_PUSH
+DISABLE_WARNING_DEPRECATED_DECLARATIONS
+#include "llvm/IR/IRBuilder.h"
+#include "llvm/IR/Module.h"
+DISABLE_WARNING_POP
+
+#include <map>
+#include <set>
+#include <string>
+
+namespace klee {
+
+class MockBuilder {
+private:
+  const llvm::Module *userModule;
+  std::unique_ptr<llvm::Module> mockModule;
+  std::unique_ptr<llvm::IRBuilder<>> builder;
+  std::map<std::string, llvm::Type *> externals;
+
+  const std::string mockEntrypoint, userEntrypoint;
+
+  void initMockModule();
+  void buildMockMain();
+  void buildExternalGlobalsDefinitions();
+  void buildExternalFunctionsDefinitions();
+  void buildCallKleeMakeSymbol(const std::string &klee_function_name,
+                               llvm::Value *source, llvm::Type *type,
+                               const std::string &symbol_name);
+
+public:
+  MockBuilder(const llvm::Module *initModule, std::string mockEntrypoint,
+              std::string userEntrypoint,
+              std::map<std::string, llvm::Type *> externals);
+
+  std::unique_ptr<llvm::Module> build();
+};
+
+} // namespace klee
+
+#endif // KLEE_MOCKBUILDER_H
diff --git a/lib/Core/SpecialFunctionHandler.cpp b/lib/Core/SpecialFunctionHandler.cpp
index 60c65f14ba..8f97931cc7 100644
--- a/lib/Core/SpecialFunctionHandler.cpp
+++ b/lib/Core/SpecialFunctionHandler.cpp
@@ -112,6 +112,7 @@ static SpecialFunctionHandler::HandlerInfo handlerInfo[] = {
 #endif
     add("klee_is_symbolic", handleIsSymbolic, true),
     add("klee_make_symbolic", handleMakeSymbolic, false),
+    add("klee_make_mock", handleMakeMock, false),
     add("klee_mark_global", handleMarkGlobal, false),
     add("klee_prefer_cex", handlePreferCex, false),
     add("klee_posix_prefer_cex", handlePosixPreferCex, false),
@@ -934,6 +935,28 @@ void SpecialFunctionHandler::handleMakeSymbolic(
   }
 }
 
+void SpecialFunctionHandler::handleMakeMock(ExecutionState &state,
+                                            KInstruction *target,
+                                            std::vector<ref<Expr>> &arguments) {
+  std::string name;
+
+  if (arguments.size() != 3) {
+    executor.terminateStateOnUserError(state,
+                                       "Incorrect number of arguments to "
+                                       "klee_make_mock(void*, size_t, char*)");
+    return;
+  }
+
+  name = arguments[2]->isZero() ? "" : readStringAtAddress(state, arguments[2]);
+
+  if (name.length() == 0) {
+    executor.terminateStateOnUserError(
+        state, "Empty name of function in klee_make_mock");
+    return;
+  }
+  executor.executeMakeMock(state, target, arguments);
+}
+
 void SpecialFunctionHandler::handleMarkGlobal(
     ExecutionState &state, KInstruction *target,
     std::vector<ref<Expr>> &arguments) {
diff --git a/lib/Core/SpecialFunctionHandler.h b/lib/Core/SpecialFunctionHandler.h
index 78f920450e..6528b98c36 100644
--- a/lib/Core/SpecialFunctionHandler.h
+++ b/lib/Core/SpecialFunctionHandler.h
@@ -127,6 +127,7 @@ class SpecialFunctionHandler {
   HANDLER(handleGetValue);
   HANDLER(handleIsSymbolic);
   HANDLER(handleMakeSymbolic);
+  HANDLER(handleMakeMock);
   HANDLER(handleMalloc);
   HANDLER(handleMemalign);
   HANDLER(handleMarkGlobal);
diff --git a/lib/Expr/ExprPPrinter.cpp b/lib/Expr/ExprPPrinter.cpp
index bde8d30d6d..c544c23b26 100644
--- a/lib/Expr/ExprPPrinter.cpp
+++ b/lib/Expr/ExprPPrinter.cpp
@@ -413,6 +413,18 @@ class PPrinter : public ExprPPrinter {
          << " " << s->index;
     } else if (auto s = dyn_cast<IrreproducibleSource>(source)) {
       PC << s->name;
+    } else if (auto s = dyn_cast<MockNaiveSource>(source)) {
+      PC << s->km->functionMap.at(&s->function)->getName() << ' ' << s->version;
+    } else if (auto s = dyn_cast<MockDeterministicSource>(source)) {
+      PC << s->km->functionMap.at(&s->function)->getName() << ' ';
+      PC << "(";
+      for (unsigned i = 0; i < s->args.size(); i++) {
+        print(s->args[i], PC);
+        if (i != s->args.size() - 1) {
+          PC << " ";
+        }
+      }
+      PC << ')';
     } else {
       assert(0 && "Not implemented");
     }
diff --git a/lib/Expr/ExprUtil.cpp b/lib/Expr/ExprUtil.cpp
index 87bed5d731..518e922dc8 100644
--- a/lib/Expr/ExprUtil.cpp
+++ b/lib/Expr/ExprUtil.cpp
@@ -54,6 +54,16 @@ void klee::findReads(ref<Expr> e, bool visitUpdates,
             cast<LazyInitializationSource>(re->updates.root->source)->pointer);
       }
 
+      if (ref<MockDeterministicSource> mockSource =
+              dyn_cast_or_null<MockDeterministicSource>(
+                  re->updates.root->source)) {
+        for (auto arg : mockSource->args) {
+          if (visited.insert(arg).second) {
+            stack.push_back(arg);
+          }
+        }
+      }
+
       if (visitUpdates) {
         // XXX this is probably suboptimal. We want to avoid a potential
         // explosion traversing update lists which can be quite
diff --git a/lib/Expr/IndependentSet.cpp b/lib/Expr/IndependentSet.cpp
index d4fade9ef1..0e491e4416 100644
--- a/lib/Expr/IndependentSet.cpp
+++ b/lib/Expr/IndependentSet.cpp
@@ -6,6 +6,7 @@
 #include "klee/Expr/ExprUtil.h"
 #include "klee/Expr/SymbolicSource.h"
 #include "klee/Expr/Symcrete.h"
+#include "klee/Module/KModule.h"
 #include "klee/Solver/Solver.h"
 
 #include <list>
@@ -35,6 +36,11 @@ IndependentElementSet::IndependentElementSet(ref<Expr> e) {
     if (re->updates.root->isConstantArray() && !re->updates.head)
       continue;
 
+    if (ref<MockDeterministicSource> mockSource =
+            dyn_cast_or_null<MockDeterministicSource>(array->source)) {
+      uninterpretedFunctions.insert(mockSource->function.getName().str());
+    }
+
     if (!wholeObjects.count(array)) {
       if (ConstantExpr *CE = dyn_cast<ConstantExpr>(re->index)) {
         // if index constant, then add to set of constraints operating
@@ -106,14 +112,15 @@ IndependentElementSet::IndependentElementSet(ref<Symcrete> s) {
 }
 
 IndependentElementSet::IndependentElementSet(const IndependentElementSet &ies)
-    : elements(ies.elements), wholeObjects(ies.wholeObjects), exprs(ies.exprs) {
-}
+    : elements(ies.elements), wholeObjects(ies.wholeObjects), exprs(ies.exprs),
+      uninterpretedFunctions(ies.uninterpretedFunctions) {}
 
 IndependentElementSet &
 IndependentElementSet::operator=(const IndependentElementSet &ies) {
   elements = ies.elements;
   wholeObjects = ies.wholeObjects;
   exprs = ies.exprs;
+  uninterpretedFunctions = ies.uninterpretedFunctions;
   return *this;
 }
 
@@ -173,6 +180,13 @@ bool IndependentElementSet::intersects(const IndependentElementSet &b) {
         return true;
     }
   }
+  for (std::set<std::string>::iterator it = uninterpretedFunctions.begin(),
+                                       ie = uninterpretedFunctions.end();
+       it != ie; ++it) {
+    if (b.uninterpretedFunctions.count(*it)) {
+      return true;
+    }
+  }
   // No need to check symcretes here, arrays must be sufficient.
   return false;
 }
diff --git a/lib/Expr/Parser.cpp b/lib/Expr/Parser.cpp
index b072cec826..1196471f71 100644
--- a/lib/Expr/Parser.cpp
+++ b/lib/Expr/Parser.cpp
@@ -330,6 +330,8 @@ class ParserImpl : public Parser {
   SourceResult ParseLazyInitializationSizeSource();
   SourceResult ParseInstructionSource();
   SourceResult ParseArgumentSource();
+  SourceResult ParseMockNaiveSource();
+  SourceResult ParseMockDeterministicSource();
 
   /*** Diagnostics ***/
 
@@ -501,6 +503,12 @@ SourceResult ParserImpl::ParseSource() {
   } else if (type == "argument") {
     assert(km);
     source = ParseArgumentSource();
+  } else if (type == "mockNaive") {
+    assert(km);
+    source = ParseMockNaiveSource();
+  } else if (type == "mockDeterministic") {
+    assert(km);
+    source = ParseMockDeterministicSource();
   } else {
     assert(0);
   }
@@ -599,6 +607,34 @@ SourceResult ParserImpl::ParseInstructionSource() {
   return SourceBuilder::instruction(*KI->inst, index, km);
 }
 
+SourceResult ParserImpl::ParseMockNaiveSource() {
+  auto name = Tok.getString();
+  auto kf = km->functionNameMap[name];
+  ConsumeExpectedToken(Token::Identifier);
+  auto versionExpr = ParseNumber(64).get();
+  auto version = dyn_cast<ConstantExpr>(versionExpr);
+  assert(version);
+  return SourceBuilder::mockNaive(km, *kf->function, version->getZExtValue());
+}
+
+SourceResult ParserImpl::ParseMockDeterministicSource() {
+  auto name = Tok.getString();
+  auto kf = km->functionNameMap[name];
+  ConsumeExpectedToken(Token::Identifier);
+  ConsumeLParen();
+  std::vector<ref<Expr>> args;
+  args.reserve(kf->numArgs);
+  for (unsigned i = 0; i < kf->numArgs; i++) {
+    auto expr = ParseExpr(TypeResult());
+    if (!expr.isValid()) {
+      return {false, nullptr};
+    }
+    args.push_back(expr.get());
+  }
+  ConsumeRParen();
+  return SourceBuilder::mockDeterministic(km, *kf->function, args);
+}
+
 /// ParseCommandDecl - Parse a command declaration. The lexer should
 /// be positioned at the opening '('.
 ///
diff --git a/lib/Expr/SourceBuilder.cpp b/lib/Expr/SourceBuilder.cpp
index a667a19ba2..c40ce3dccd 100644
--- a/lib/Expr/SourceBuilder.cpp
+++ b/lib/Expr/SourceBuilder.cpp
@@ -86,4 +86,21 @@ ref<SymbolicSource> SourceBuilder::irreproducible(const std::string &name) {
   ref<SymbolicSource> r(new IrreproducibleSource(name + llvm::utostr(++id)));
   r->computeHash();
   return r;
-}
\ No newline at end of file
+}
+
+ref<SymbolicSource> SourceBuilder::mockNaive(const KModule *km,
+                                             const llvm::Function &function,
+                                             unsigned int version) {
+  ref<SymbolicSource> r(new MockNaiveSource(km, function, version));
+  r->computeHash();
+  return r;
+}
+
+ref<SymbolicSource>
+SourceBuilder::mockDeterministic(const KModule *km,
+                                 const llvm::Function &function,
+                                 const std::vector<ref<Expr>> &args) {
+  ref<SymbolicSource> r(new MockDeterministicSource(km, function, args));
+  r->computeHash();
+  return r;
+}
diff --git a/lib/Expr/SymbolicSource.cpp b/lib/Expr/SymbolicSource.cpp
index 0e7f8b1086..3857d53db7 100644
--- a/lib/Expr/SymbolicSource.cpp
+++ b/lib/Expr/SymbolicSource.cpp
@@ -163,4 +163,65 @@ unsigned InstructionSource::computeHash() {
   return hashValue;
 }
 
+unsigned MockNaiveSource::computeHash() {
+  unsigned res = (getKind() * SymbolicSource::MAGIC_HASH_CONSTANT) + version;
+  unsigned funcID = km->functionIDMap.at(&function);
+  res = (res * SymbolicSource::MAGIC_HASH_CONSTANT) + funcID;
+  hashValue = res;
+  return res;
+}
+
+int MockNaiveSource::internalCompare(const SymbolicSource &b) const {
+  if (getKind() != b.getKind()) {
+    return getKind() < b.getKind() ? -1 : 1;
+  }
+  const MockNaiveSource &mnb = static_cast<const MockNaiveSource &>(b);
+  if (version != mnb.version) {
+    return version < mnb.version ? -1 : 1;
+  }
+  unsigned funcID = km->functionIDMap.at(&function);
+  unsigned bFuncID = mnb.km->functionIDMap.at(&mnb.function);
+  if (funcID != bFuncID) {
+    return funcID < bFuncID ? -1 : 1;
+  }
+  return 0;
+}
+
+MockDeterministicSource::MockDeterministicSource(
+    const KModule *km, const llvm::Function &function,
+    const std::vector<ref<Expr>> &_args)
+    : MockSource(km, function), args(_args) {}
+
+unsigned MockDeterministicSource::computeHash() {
+  unsigned res = getKind();
+  res = (res * SymbolicSource::MAGIC_HASH_CONSTANT) +
+        km->functionIDMap.at(&function);
+  for (const auto &arg : args) {
+    res = (res * SymbolicSource::MAGIC_HASH_CONSTANT) + arg->hash();
+  }
+  hashValue = res;
+  return res;
+}
+
+int MockDeterministicSource::internalCompare(const SymbolicSource &b) const {
+  if (getKind() != b.getKind()) {
+    return getKind() < b.getKind() ? -1 : 1;
+  }
+  const MockDeterministicSource &mdb =
+      static_cast<const MockDeterministicSource &>(b);
+  unsigned funcID = km->functionIDMap.at(&function);
+  unsigned bFuncID = mdb.km->functionIDMap.at(&mdb.function);
+  if (funcID != bFuncID) {
+    return funcID < bFuncID ? -1 : 1;
+  }
+  assert(args.size() == mdb.args.size() &&
+         "the same functions should have the same arguments number");
+  for (unsigned i = 0; i < args.size(); i++) {
+    if (args[i] != mdb.args[i]) {
+      return args[i] < mdb.args[i] ? -1 : 1;
+    }
+  }
+  return 0;
+}
+
 } // namespace klee
diff --git a/lib/Solver/Z3Builder.cpp b/lib/Solver/Z3Builder.cpp
index 39cdf1918d..799ce046d5 100644
--- a/lib/Solver/Z3Builder.cpp
+++ b/lib/Solver/Z3Builder.cpp
@@ -13,6 +13,7 @@
 #include "klee/ADT/Bits.h"
 #include "klee/Expr/Expr.h"
 #include "klee/Expr/SymbolicSource.h"
+#include "klee/Module/KModule.h"
 #include "klee/Solver/Solver.h"
 #include "klee/Solver/SolverStats.h"
 #include "klee/Support/ErrorHandling.h"
@@ -257,6 +258,37 @@ Z3ASTHandle Z3Builder::getInitialArray(const Array *root) {
       array_expr = buildConstantArray(unique_name.c_str(), root->getDomain(),
                                       root->getRange(),
                                       symbolicSizeConstantSource->defaultValue);
+    } else if (ref<MockDeterministicSource> mockDeterministicSource =
+                   dyn_cast<MockDeterministicSource>(root->source)) {
+      size_t num_args = mockDeterministicSource->args.size();
+      std::vector<Z3ASTHandle> argsHandled(num_args);
+      std::vector<Z3SortHandle> argsSortHandled(num_args);
+      std::vector<Z3_ast> args(num_args);
+      std::vector<Z3_sort> argsSort(num_args);
+      for (size_t i = 0; i < num_args; i++) {
+        ref<Expr> kid = mockDeterministicSource->args[i];
+        int kidWidth = kid->getWidth();
+        argsHandled[i] = construct(kid, &kidWidth);
+        args[i] = argsHandled[i];
+        argsSortHandled[i] = Z3SortHandle(Z3_get_sort(ctx, args[i]), ctx);
+        argsSort[i] = argsSortHandled[i];
+      }
+
+      Z3SortHandle domainSort = getBvSort(root->getDomain());
+      Z3SortHandle rangeSort = getBvSort(root->getRange());
+      Z3SortHandle retValSort = getArraySort(domainSort, rangeSort);
+
+      Z3FuncDeclHandle func;
+      func = Z3FuncDeclHandle(
+          Z3_mk_func_decl(
+              ctx,
+              Z3_mk_string_symbol(
+                  ctx,
+                  mockDeterministicSource->function.getName().str().c_str()),
+              num_args, argsSort.data(), retValSort),
+          ctx);
+      array_expr =
+          Z3ASTHandle(Z3_mk_app(ctx, func, num_args, args.data()), ctx);
     } else {
       array_expr =
           buildArray(unique_name.c_str(), root->getDomain(), root->getRange());
diff --git a/lib/Solver/Z3Builder.h b/lib/Solver/Z3Builder.h
index 001ac13a9c..d906f455c4 100644
--- a/lib/Solver/Z3Builder.h
+++ b/lib/Solver/Z3Builder.h
@@ -91,6 +91,13 @@ typedef Z3NodeHandle<Z3_sort> Z3SortHandle;
 template <> void Z3NodeHandle<Z3_sort>::dump() __attribute__((used));
 template <> unsigned Z3NodeHandle<Z3_sort>::hash() __attribute__((used));
 
+// Specialize for Z3_func_decl
+template <> inline ::Z3_ast Z3NodeHandle<Z3_func_decl>::as_ast() {
+  return ::Z3_func_decl_to_ast(context, node);
+}
+typedef Z3NodeHandle<Z3_func_decl> Z3FuncDeclHandle;
+template <> void Z3NodeHandle<Z3_func_decl>::dump() __attribute__((used));
+
 // Specialise for Z3_ast
 template <> inline ::Z3_ast Z3NodeHandle<Z3_ast>::as_ast() { return node; }
 typedef Z3NodeHandle<Z3_ast> Z3ASTHandle;
diff --git a/runtime/CMakeLists.txt b/runtime/CMakeLists.txt
index ada82c0f33..d1c8a17d2f 100644
--- a/runtime/CMakeLists.txt
+++ b/runtime/CMakeLists.txt
@@ -90,12 +90,14 @@ add_subdirectory(Freestanding)
 add_subdirectory(Intrinsic)
 add_subdirectory(klee-libc)
 add_subdirectory(Fortify)
+add_subdirectory(Mocks)
 
 set(RUNTIME_LIBRARIES
         RuntimeFreestanding
         RuntimeIntrinsic
         RuntimeKLEELibc
         RuntimeFortify
+        RuntimeMocks
         )
 
 if (ENABLE_KLEE_EH_CXX)
diff --git a/runtime/Mocks/CMakeLists.txt b/runtime/Mocks/CMakeLists.txt
new file mode 100644
index 0000000000..efd6497470
--- /dev/null
+++ b/runtime/Mocks/CMakeLists.txt
@@ -0,0 +1,19 @@
+#===------------------------------------------------------------------------===#
+#
+#                     The KLEE Symbolic Virtual Machine
+#
+# This file is distributed under the University of Illinois Open Source
+# License. See LICENSE.TXT for details.
+#
+#===------------------------------------------------------------------------===#
+
+set(LIB_PREFIX "RuntimeMocks")
+set(SRC_FILES
+        models.c
+        )
+
+# Build it
+include("${CMAKE_SOURCE_DIR}/cmake/compile_bitcode_library.cmake")
+prefix_with_path("${SRC_FILES}" "${CMAKE_CURRENT_SOURCE_DIR}/" runtime_mocks_files)
+
+add_bitcode_library_targets("${LIB_PREFIX}" "${runtime_mocks_files}" "" "")
diff --git a/runtime/Mocks/models.c b/runtime/Mocks/models.c
new file mode 100644
index 0000000000..ad95634b47
--- /dev/null
+++ b/runtime/Mocks/models.c
@@ -0,0 +1,36 @@
+#include "stddef.h"
+
+extern void klee_make_symbolic(void *array, size_t nbytes, const char *name);
+extern void *malloc(size_t size);
+extern void *calloc(size_t num, size_t size);
+extern void *realloc(void *ptr, size_t new_size);
+
+void *__klee_wrapped_malloc(size_t size) {
+  char retNull;
+  klee_make_symbolic(&retNull, sizeof(retNull), "retNullMalloc");
+  if (retNull) {
+    return 0;
+  }
+  void *array = malloc(size);
+  return array;
+}
+
+void *__klee_wrapped_calloc(size_t num, size_t size) {
+  char retNull;
+  klee_make_symbolic(&retNull, sizeof(retNull), "retNullCalloc");
+  if (retNull) {
+    return 0;
+  }
+  void *array = calloc(num, size);
+  return array;
+}
+
+void *__klee_wrapped_realloc(void *ptr, size_t new_size) {
+  char retNull;
+  klee_make_symbolic(&retNull, sizeof(retNull), "retNullRealloc");
+  if (retNull) {
+    return 0;
+  }
+  void *array = realloc(ptr, new_size);
+  return array;
+}
diff --git a/runtime/Runtest/CMakeLists.txt b/runtime/Runtest/CMakeLists.txt
index df5f2c23be..33d190a262 100644
--- a/runtime/Runtest/CMakeLists.txt
+++ b/runtime/Runtest/CMakeLists.txt
@@ -9,6 +9,8 @@
 
 add_library(kleeRuntest SHARED
   intrinsics.c
+  # Mocks:
+  ${CMAKE_SOURCE_DIR}/runtime/Mocks/models.c
   # HACK:
   ${CMAKE_SOURCE_DIR}/lib/Basic/KTest.cpp
 )
diff --git a/runtime/Runtest/intrinsics.c b/runtime/Runtest/intrinsics.c
index 34a9e9d2c8..3e6bdd8efd 100644
--- a/runtime/Runtest/intrinsics.c
+++ b/runtime/Runtest/intrinsics.c
@@ -72,8 +72,7 @@ void recursively_allocate(KTestObject *obj, size_t index, void *addr,
   return;
 }
 
-void klee_make_symbolic(void *array, size_t nbytes, const char *name) {
-
+static void klee_make_symbol(void *array, size_t nbytes, const char *name) {
   if (!name)
     name = "unnamed";
 
@@ -154,6 +153,14 @@ void klee_make_symbolic(void *array, size_t nbytes, const char *name) {
   }
 }
 
+void klee_make_symbolic(void *array, size_t nbytes, const char *name) {
+  klee_make_symbol(array, nbytes, name);
+}
+
+void klee_make_mock(void *ret_array, size_t ret_nbytes, const char *fname) {
+  klee_make_symbol(ret_array, ret_nbytes, fname);
+}
+
 void klee_silent_exit(int x) { exit(x); }
 
 uintptr_t klee_choose(uintptr_t n) {
diff --git a/scripts/run_tests_with_mocks.py b/scripts/run_tests_with_mocks.py
new file mode 100755
index 0000000000..5843a37ad0
--- /dev/null
+++ b/scripts/run_tests_with_mocks.py
@@ -0,0 +1,26 @@
+#!/usr/bin/env python3
+
+# This script builds executable file using initial bitcode file and artifacts produced by KLEE.
+# To run the script provide all the arguments you want to pass to clang for building executable.
+#
+# NOTE: Pre-last argument should be a path to KLEE output directory which contains redefinitions.txt and externals.ll.
+# NOTE: Last argument is path to initial bitcode.
+#
+# Example: python3 run_tests_with_mocks.py -I ~/klee/include/ -L ~/klee/build/lib/ -lkleeRuntest klee-last a.bc
+#
+# You can read more about replaying test cases here: http://klee.github.io/tutorials/testing-function/
+
+import subprocess as sp
+import sys
+import os
+
+klee_out_dir = sys.argv[-2]
+bitcode = sys.argv[-1]
+
+filename = os.path.splitext(bitcode)[0]
+object_file = f'{filename}.o'
+sp.run(f'clang -c {bitcode} -o {object_file}', shell=True)
+sp.run(f'llvm-objcopy {object_file} --redefine-syms {klee_out_dir}/redefinitions.txt', shell=True)
+clang_args = ' '.join(sys.argv[1:len(sys.argv) - 2])
+print(f'clang {clang_args} {klee_out_dir}/externals.ll {object_file}')
+sp.run(f'clang {clang_args} {klee_out_dir}/externals.ll {object_file}', shell=True)
diff --git a/test/CMakeLists.txt b/test/CMakeLists.txt
index 17723d865f..c7d14ed87e 100644
--- a/test/CMakeLists.txt
+++ b/test/CMakeLists.txt
@@ -15,6 +15,7 @@ set(LLVM_TOOLS_DIR "${LLVM_TOOLS_BINARY_DIR}")
 set(LLVMCC "${LLVMCC} -I${CMAKE_SOURCE_DIR}/include")
 set(LLVMCXX "${LLVMCXX} -I${CMAKE_SOURCE_DIR}/include")
 set(NATIVE_CC "${CMAKE_C_COMPILER} ${CMAKE_C_FLAGS} -I ${CMAKE_SOURCE_DIR}/include")
+set(NATIVE_OBJCOPY "${CMAKE_OBJCOPY}")
 set(NATIVE_CXX "${CMAKE_CXX_COMPILER} ${CMAKE_CXX_FLAGS} -I ${CMAKE_SOURCE_DIR}/include")
 set(TARGET_TRIPLE "${TARGET_TRIPLE}")
 
diff --git a/test/Feature/MockPointersDeterministic.c b/test/Feature/MockPointersDeterministic.c
new file mode 100644
index 0000000000..16450714e3
--- /dev/null
+++ b/test/Feature/MockPointersDeterministic.c
@@ -0,0 +1,23 @@
+// REQUIRES: z3
+// RUN: %clang %s -g -emit-llvm %O0opt -c -o %t.bc
+
+// RUN: rm -rf %t.klee-out-1
+// RUN: %klee --solver-backend=z3 --output-dir=%t.klee-out-1 --min-number-elements-li=0 --use-sym-size-li --skip-not-lazy-initialized --external-calls=all --mock-strategy=deterministic %t.bc 2>&1 | FileCheck %s -check-prefix=CHECK-1
+// CHECK-1: memory error: null pointer exception
+// CHECK-1: KLEE: done: completed paths = 1
+// CHECK-1: KLEE: done: partially completed paths = 2
+// CHECK-1: KLEE: done: generated tests = 3
+
+#include <assert.h>
+
+extern int *age();
+
+int main() {
+  if (age() != age()) {
+    assert(0 && "age is deterministic");
+  }
+  if (*age() != *age()) {
+    assert(0 && "age is deterministic");
+  }
+  return *age();
+}
\ No newline at end of file
diff --git a/test/Feature/MockStrategies.c b/test/Feature/MockStrategies.c
new file mode 100644
index 0000000000..524fbba3a2
--- /dev/null
+++ b/test/Feature/MockStrategies.c
@@ -0,0 +1,37 @@
+// REQUIRES: z3
+// RUN: %clang %s -g -emit-llvm %O0opt -c -o %t.bc
+
+// RUN: rm -rf %t.klee-out-1
+// RUN: %klee --output-dir=%t.klee-out-1 --external-calls=all --mock-strategy=none %t.bc 2>&1 | FileCheck %s -check-prefix=CHECK-1
+// CHECK-1: failed external call
+// CHECK-1: KLEE: done: completed paths = 1
+// CHECK-1: KLEE: done: generated tests = 2
+
+// RUN: rm -rf %t.klee-out-2
+// RUN: %klee --output-dir=%t.klee-out-2 --external-calls=all --mock-strategy=naive %t.bc 2>&1 | FileCheck %s -check-prefix=CHECK-2
+// CHECK-2: ASSERTION FAIL: 0
+// CHECK-2: KLEE: done: completed paths = 2
+// CHECK-2: KLEE: done: generated tests = 3
+
+// RUN: rm -rf %t.klee-out-3
+// RUN: not %klee --output-dir=%t.klee-out-3 --solver-backend=stp --external-calls=all --mock-strategy=deterministic %t.bc 2>&1 | FileCheck %s -check-prefix=CHECK-3
+// CHECK-3: KLEE: ERROR: Deterministic mocks can be generated with Z3 solver only.
+
+// RUN: rm -rf %t.klee-out-4
+// RUN: %klee --output-dir=%t.klee-out-4 --solver-backend=z3 --external-calls=all --mock-strategy=deterministic %t.bc 2>&1 | FileCheck %s -check-prefix=CHECK-4
+// CHECK-4: KLEE: done: completed paths = 2
+// CHECK-4: KLEE: done: generated tests = 2
+
+#include <assert.h>
+
+extern int foo(int x, int y);
+
+int main() {
+  int a, b;
+  klee_make_symbolic(&a, sizeof(a), "a");
+  klee_make_symbolic(&b, sizeof(b), "b");
+  if (a == b && foo(a + b, b) != foo(2 * b, a)) {
+    assert(0);
+  }
+  return 0;
+}
diff --git a/test/Replay/libkleeruntest/replay_mocks.c b/test/Replay/libkleeruntest/replay_mocks.c
new file mode 100644
index 0000000000..bb9c9e7691
--- /dev/null
+++ b/test/Replay/libkleeruntest/replay_mocks.c
@@ -0,0 +1,21 @@
+// REQUIRES: geq-llvm-11.0
+// REQUIRES: not-darwin
+// RUN: %clang %s -emit-llvm -g %O0opt -c -o %t.bc
+// RUN: rm -rf %t.klee-out
+// RUN: %klee --output-dir=%t.klee-out --external-calls=all --mock-strategy=naive %t.bc
+// RUN: %clang -c %t.bc -o %t.o
+// RUN: %llc %t.klee-out/externals.ll -filetype=obj -o %t_externals.o
+// RUN: %objcopy --redefine-syms %t.klee-out/redefinitions.txt %t.o
+// RUN: %cc -no-pie %t_externals.o %t.o %libkleeruntest -Wl,-rpath %libkleeruntestdir -o %t_runner
+// RUN: test -f %t.klee-out/test000001.ktest
+// RUN: env KTEST_FILE=%t.klee-out/test000001.ktest %t_runner
+
+extern int variable;
+
+extern int foo(int);
+
+int main() {
+  int a;
+  klee_make_symbolic(&a, sizeof(a), "a");
+  return variable + foo(a);
+}
diff --git a/test/lit.cfg b/test/lit.cfg
index 75978e47b7..83d7a0f2a3 100644
--- a/test/lit.cfg
+++ b/test/lit.cfg
@@ -90,17 +90,27 @@ if config.test_exec_root is None:
 
 
 # Add substitutions from lit.site.cfg
-subs = [ 'clangxx', 'clang', 'cc', 'cxx', 'O0opt', 'c_prefixes_8', 'c_prefixes_10', 'cpp_prefixes_10' ]
+subs = [ 'clangxx', 'clang', 'cc', 'objcopy', 'cxx', 'O0opt', 'c_prefixes_8', 'c_prefixes_10', 'cpp_prefixes_10' ]
 for name in subs:
   value = getattr(config, name, None)
   if value == None:
     lit_config.fatal('{0} is not set'.format(name))
   config.substitutions.append( ('%' + name, value))
 
+config.substitutions.append(
+  ('%runmocks', os.path.join(klee_src_root, 'scripts/run_tests_with_mocks.py'))
+)
+
 # Add a substitution for lli.
 config.substitutions.append(
   ('%lli', os.path.join(llvm_tools_dir, 'lli'))
 )
+
+# Add a substitution for llc.
+config.substitutions.append(
+  ('%llc', os.path.join(llvm_tools_dir, 'llc'))
+)
+
 # Add a substitution for llvm-as
 config.substitutions.append(
   ('%llvmas', os.path.join(llvm_tools_dir, 'llvm-as'))
@@ -114,6 +124,11 @@ config.substitutions.append(
   ('%llvmlink', os.path.join(llvm_tools_dir, 'llvm-link'))
 )
 
+# Add a substitution for llvm-objcopy
+config.substitutions.append(
+  ('%llvmobjcopy', os.path.join(llvm_tools_dir, 'llvm-objcopy'))
+)
+
 # Add a substition for libkleeruntest
 config.substitutions.append(
   ('%libkleeruntestdir', os.path.dirname(config.libkleeruntest))
diff --git a/test/lit.site.cfg.in b/test/lit.site.cfg.in
index 15bc4a20a5..010cc5d152 100644
--- a/test/lit.site.cfg.in
+++ b/test/lit.site.cfg.in
@@ -35,6 +35,7 @@ config.clang = "@LLVMCC@"
 config.clangxx = "@LLVMCXX@"
 
 config.cc = "@NATIVE_CC@"
+config.objcopy = "@NATIVE_OBJCOPY@"
 config.cxx = "@NATIVE_CXX@"
 
 # NOTE: any changes to compiler flags also have to be applied to
diff --git a/tools/klee/main.cpp b/tools/klee/main.cpp
index 68525c7f52..e8b3672302 100644
--- a/tools/klee/main.cpp
+++ b/tools/klee/main.cpp
@@ -341,6 +341,33 @@ cl::opt<bool> Libcxx(
     "libcxx",
     cl::desc("Link the llvm libc++ library into the bitcode (default=false)"),
     cl::init(false), cl::cat(LinkCat));
+
+/*** Mocking options ***/
+
+cl::OptionCategory MockCat("Mock category");
+
+cl::opt<bool> MockLinkedExternals(
+    "mock-linked-externals",
+    cl::desc("Mock modelled linked externals (default=false)"), cl::init(false),
+    cl::cat(MockCat));
+
+cl::opt<MockStrategy> MockUnlinkedStrategy(
+    "mock-strategy", cl::init(MockStrategy::None),
+    cl::desc("Specify strategy for mocking external calls"),
+    cl::values(
+        clEnumValN(MockStrategy::None, "none",
+                   "External calls are not mocked (default)"),
+        clEnumValN(MockStrategy::Naive, "naive",
+                   "Every time external function is called, new symbolic value "
+                   "is generated for its return value"),
+        clEnumValN(
+            MockStrategy::Deterministic, "deterministic",
+            "NOTE: this option is compatible with Z3 solver only. Each "
+            "external function is treated as a deterministic "
+            "function. Therefore, when function is called many times "
+            "with equal arguments, every time equal values will be returned.")),
+    cl::init(MockStrategy::None), cl::cat(MockCat));
+
 } // namespace
 
 namespace klee {
@@ -755,7 +782,7 @@ std::string KleeHandler::getRunTimeLibraryPath(const char *argv0) {
 
 void KleeHandler::setOutputDirectory(const std::string &directoryName) {
   // create output directory
-  if (directoryName == "") {
+  if (directoryName.empty()) {
     klee_error("Empty name of new directory");
   }
   SmallString<128> directory(directoryName);
@@ -860,10 +887,11 @@ static const char *modelledExternals[] = {
     "klee_check_memory_access", "klee_define_fixed_object", "klee_get_errno",
     "klee_get_valuef", "klee_get_valued", "klee_get_valuel", "klee_get_valuell",
     "klee_get_value_i32", "klee_get_value_i64", "klee_get_obj_size",
-    "klee_is_symbolic", "klee_make_symbolic", "klee_mark_global",
-    "klee_prefer_cex", "klee_posix_prefer_cex", "klee_print_expr",
-    "klee_print_range", "klee_report_error", "klee_set_forking",
-    "klee_silent_exit", "klee_warning", "klee_warning_once", "klee_stack_trace",
+    "klee_is_symbolic", "klee_make_symbolic", "klee_make_mock",
+    "klee_mark_global", "klee_prefer_cex", "klee_posix_prefer_cex",
+    "klee_print_expr", "klee_print_range", "klee_report_error",
+    "klee_set_forking", "klee_silent_exit", "klee_warning", "klee_warning_once",
+    "klee_stack_trace",
 #ifdef SUPPORT_KLEE_EH_CXX
     "_klee_eh_Unwind_RaiseException_impl", "klee_eh_typeid_for",
 #endif
@@ -954,12 +982,14 @@ static const char *dontCareExternals[] = {
     "getwd",
     "gettimeofday",
     "uname",
+    "ioctl",
 
     // fp stuff we just don't worry about yet
     "frexp",
     "ldexp",
     "__isnan",
     "__signbit",
+    "llvm.dbg.label",
 };
 
 // Extra symbols we aren't going to warn about with klee-libc
@@ -1432,6 +1462,41 @@ void wait_until_any_child_dies(
   }
 }
 
+void mockLinkedExternals(
+    const Interpreter::ModuleOptions &Opts, llvm::LLVMContext &ctx,
+    llvm::Module *mainModule,
+    std::vector<std::unique_ptr<llvm::Module>> &loadedLibsModules,
+    llvm::raw_string_ostream *redefineFile) {
+  std::string errorMsg;
+  std::vector<std::unique_ptr<llvm::Module>> mockModules;
+  SmallString<128> Path(Opts.LibraryDir);
+  llvm::sys::path::append(Path,
+                          "libkleeRuntimeMocks" + Opts.OptSuffix + ".bca");
+  klee_message("NOTE: Using mocks model %s for linked externals", Path.c_str());
+  if (!klee::loadFileAsOneModule(Path.c_str(), ctx, mockModules, errorMsg)) {
+    klee_error("error loading mocks model '%s': %s", Path.c_str(),
+               errorMsg.c_str());
+  }
+
+  for (auto &module : mockModules) {
+    for (const auto &fmodel : module->functions()) {
+      if (fmodel.getName().str().substr(0, 15) != "__klee_wrapped_") {
+        continue;
+      }
+      llvm::Function *f =
+          mainModule->getFunction(fmodel.getName().str().substr(15));
+      if (!f) {
+        continue;
+      }
+      klee_message("Renamed symbol %s to %s", f->getName().str().c_str(),
+                   fmodel.getName().str().c_str());
+      *redefineFile << f->getName() << ' ' << fmodel.getName() << '\n';
+      f->setName(fmodel.getName());
+    }
+    loadedLibsModules.push_back(std::move(module));
+  }
+}
+
 int main(int argc, char **argv, char **envp) {
   if (theInterpreter) {
     theInterpreter = nullptr;
@@ -1603,13 +1668,16 @@ int main(int argc, char **argv, char **envp) {
   }
 
   std::string LibraryDir = KleeHandler::getRunTimeLibraryPath(argv[0]);
-  Interpreter::ModuleOptions Opts(LibraryDir.c_str(), EntryPoint, opt_suffix,
-                                  /*Optimize=*/OptimizeModule,
-                                  /*Simplify*/ SimplifyModule,
-                                  /*CheckDivZero=*/CheckDivZero,
-                                  /*CheckOvershift=*/CheckOvershift,
-                                  /*WithFPRuntime=*/WithFPRuntime,
-                                  /*WithPOSIXRuntime=*/WithPOSIXRuntime);
+  Interpreter::ModuleOptions Opts(
+      LibraryDir.c_str(), EntryPoint, opt_suffix,
+      /*MainCurrentName=*/EntryPoint,
+      /*MainNameAfterMock=*/"__klee_mock_wrapped_main",
+      /*Optimize=*/OptimizeModule,
+      /*Simplify*/ SimplifyModule,
+      /*CheckDivZero=*/CheckDivZero,
+      /*CheckOvershift=*/CheckOvershift,
+      /*WithFPRuntime=*/WithFPRuntime,
+      /*WithPOSIXRuntime=*/WithPOSIXRuntime);
 
   // Get the main function
   for (auto &module : loadedUserModules) {
@@ -1622,6 +1690,11 @@ int main(int argc, char **argv, char **envp) {
   if (EntryPoint.empty())
     klee_error("entry-point cannot be empty");
 
+  llvm::Function *initialMainFn = mainModule->getFunction(EntryPoint);
+  if (!initialMainFn) {
+    klee_error("Entry function '%s' not found in module.", EntryPoint.c_str());
+  }
+
   for (auto &module : loadedUserModules) {
     entryFn = module->getFunction(EntryPoint);
     if (entryFn)
@@ -1631,6 +1704,17 @@ int main(int argc, char **argv, char **envp) {
   if (!entryFn)
     klee_error("Entry function '%s' not found in module.", EntryPoint.c_str());
 
+  std::string redefinitions;
+  llvm::raw_string_ostream o_redefinitions(redefinitions);
+  if (MockLinkedExternals) {
+    mockLinkedExternals(Opts, ctx, mainModule, loadedLibsModules,
+                        &o_redefinitions);
+  }
+
+  if (MockUnlinkedStrategy != MockStrategy::None) {
+    o_redefinitions << EntryPoint << ' ' << Opts.MainNameAfterMock << '\n';
+  }
+
   if (WithPOSIXRuntime) {
     SmallString<128> Path(Opts.LibraryDir);
     llvm::sys::path::append(Path, "libkleeRuntimePOSIX" + opt_suffix + ".bca");
@@ -1795,6 +1879,7 @@ int main(int argc, char **argv, char **envp) {
   Interpreter::InterpreterOptions IOpts(paths);
   IOpts.MakeConcreteSymbolic = MakeConcreteSymbolic;
   IOpts.Guidance = UseGuidedSearch;
+  IOpts.MockStrategy = MockUnlinkedStrategy;
   std::unique_ptr<Interpreter> interpreter(
       Interpreter::create(ctx, IOpts, handler.get()));
   theInterpreter = interpreter.get();
@@ -1806,12 +1891,43 @@ int main(int argc, char **argv, char **envp) {
   }
   handler->getInfoStream() << "PID: " << getpid() << "\n";
 
+  if (MockLinkedExternals || MockUnlinkedStrategy != MockStrategy::None) {
+    o_redefinitions.flush();
+    auto f_redefinitions = handler->openOutputFile("redefinitions.txt");
+    *f_redefinitions << redefinitions;
+  }
+
   // Get the desired main function.  klee_main initializes uClibc
   // locale and other data and then calls main.
 
+  std::set<std::string> ignoredExternals;
+  ignoredExternals.insert(modelledExternals,
+                          modelledExternals + NELEMS(modelledExternals));
+  ignoredExternals.insert(dontCareExternals,
+                          dontCareExternals + NELEMS(dontCareExternals));
+  ignoredExternals.insert(unsafeExternals,
+                          unsafeExternals + NELEMS(unsafeExternals));
+
+  switch (Libc) {
+  case LibcType::KleeLibc:
+    ignoredExternals.insert(dontCareKlee, dontCareKlee + NELEMS(dontCareKlee));
+    break;
+  case LibcType::UcLibc:
+    ignoredExternals.insert(dontCareUclibc,
+                            dontCareUclibc + NELEMS(dontCareUclibc));
+    break;
+  case LibcType::FreestandingLibc: /* silence compiler warning */
+    break;
+  }
+
+  if (WithPOSIXRuntime) {
+    ignoredExternals.insert("syscall");
+  }
+
+  Opts.MainCurrentName = initialMainFn->getName();
   auto finalModule = interpreter->setModule(
       loadedUserModules, loadedLibsModules, Opts, mainModuleFunctions,
-      mainModuleGlobals, std::move(origInfos));
+      mainModuleGlobals, std::move(origInfos), ignoredExternals);
 
   externalsAndGlobalsCheck(finalModule);
   if (InteractiveMode) {