diff --git a/configs/options.json b/configs/options.json
index 32f20ebbf73..bf33270c392 100644
--- a/configs/options.json
+++ b/configs/options.json
@@ -24,7 +24,7 @@
                 "--suppress-external-warnings",
                 "--libc=klee",
                 "--skip-not-lazy-initialized",
-                "--external-calls=all",
+                "--external-calls=mock",
                 "--output-source=false",
                 "--output-istats=false",
                 "--output-stats=false",
@@ -32,7 +32,6 @@
                 "--max-sym-alloc=${maxSymAlloc}",
                 "--max-forks=${maxForks}",
                 "--max-solver-time=${maxSolverTime}s",
-                "--mock-all-externals",
                 "--smart-resolve-entry-function",
                 "--extern-calls-can-return-null",
                 "--align-symbolic-pointers=false",
@@ -49,4 +48,4 @@
             ]
         }
     ]
-}
\ No newline at end of file
+}
diff --git a/include/klee/Core/Interpreter.h b/include/klee/Core/Interpreter.h
index bdebe1a221a..758337277ad 100644
--- a/include/klee/Core/Interpreter.h
+++ b/include/klee/Core/Interpreter.h
@@ -68,11 +68,14 @@ using FLCtoOpcode = std::unordered_map<
     std::unordered_map<
         unsigned, std::unordered_map<unsigned, std::unordered_set<unsigned>>>>;
 
-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
+/*** External call policy options ***/
+
+enum class ExternalCallPolicy {
+  None,       // No external calls allowed
+  Concrete,   // Only external calls with concrete arguments allowed
+  All,        // All external calls allowed
+  Mock,       // For each function call new symbolic value is generated
+  MockDeterm, // Each function is treated as uninterpreted function in SMT.
 };
 
 class Interpreter {
@@ -135,11 +138,11 @@ class Interpreter {
     unsigned MakeConcreteSymbolic;
     GuidanceKind Guidance;
     nonstd::optional<SarifReport> Paths;
-    enum MockStrategy MockStrategy;
+    enum ExternalCallPolicy ExternalCall;
 
     InterpreterOptions(nonstd::optional<SarifReport> Paths)
         : MakeConcreteSymbolic(false), Guidance(GuidanceKind::NoGuidance),
-          Paths(std::move(Paths)), MockStrategy(MockStrategy::None) {}
+          Paths(std::move(Paths)), ExternalCall(ExternalCallPolicy::None) {}
   };
 
 protected:
diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp
index 7eaae36ffea..0894363a3f5 100644
--- a/lib/Core/Executor.cpp
+++ b/lib/Core/Executor.cpp
@@ -289,30 +289,6 @@ cl::opt<bool>
                                   "querying the solver (default=true)"),
                          cl::cat(SolvingCat));
 
-/*** External call policy options ***/
-
-enum class ExternalCallPolicy {
-  None,     // No external calls allowed
-  Concrete, // Only external calls with concrete arguments allowed
-  All,      // All external calls allowed
-};
-
-cl::opt<ExternalCallPolicy> ExternalCalls(
-    "external-calls", cl::desc("Specify the external call policy"),
-    cl::values(
-        clEnumValN(
-            ExternalCallPolicy::None, "none",
-            "No external function calls are allowed.  Note that KLEE always "
-            "allows some external calls with concrete arguments to go through "
-            "(in particular printf and puts), regardless of this option."),
-        clEnumValN(ExternalCallPolicy::Concrete, "concrete",
-                   "Only external function calls with concrete arguments are "
-                   "allowed (default)"),
-        clEnumValN(ExternalCallPolicy::All, "all",
-                   "All external function calls are allowed.  This concretizes "
-                   "any symbolic arguments in calls to external functions.")),
-    cl::init(ExternalCallPolicy::Concrete), cl::cat(ExtCallsCat));
-
 cl::opt<bool> SuppressExternalWarnings(
     "suppress-external-warnings", cl::init(false),
     cl::desc("Supress warnings about calling external functions."),
@@ -332,10 +308,6 @@ cl::opt<bool>
                                "If false, fails on externall calls."),
                       cl::cat(ExtCallsCat));
 
-cl::opt<bool> MockAllExternals("mock-all-externals", cl::init(false),
-                               cl::desc("If true, all externals are mocked."),
-                               cl::cat(ExtCallsCat));
-
 /*** Seeding options ***/
 
 cl::opt<bool> AlwaysOutputSeeds(
@@ -496,7 +468,7 @@ Executor::Executor(LLVMContext &ctx, const InterpreterOptions &opts,
       inhibitForking(false), coverOnTheFly(false),
       haltExecution(HaltExecution::NotHalt), ivcEnabled(false),
       debugLogBuffer(debugBufferString) {
-  if (interpreterOpts.MockStrategy == MockStrategy::Deterministic &&
+  if (interpreterOpts.ExternalCall == ExternalCallPolicy::MockDeterm &&
       CoreSolverToUse != Z3_SOLVER) {
     klee_error("Deterministic mocks can be generated with Z3 solver only.\n");
   }
@@ -573,8 +545,8 @@ llvm::Module *Executor::setModule(
   assert(!kmodule && !userModules.empty() &&
          "can only register one module"); // XXX gross
 
-  if (ExternalCalls == ExternalCallPolicy::All &&
-      interpreterOpts.MockStrategy != MockStrategy::None) {
+  if (interpreterOpts.ExternalCall == ExternalCallPolicy::Mock ||
+      interpreterOpts.ExternalCall == ExternalCallPolicy::MockDeterm) {
     llvm::Function *mainFn =
         userModules.front()->getFunction(opts.MainCurrentName);
     if (!mainFn) {
@@ -608,8 +580,8 @@ llvm::Module *Executor::setModule(
     kmodule->instrument(opts);
   }
 
-  if ((ExternalCalls == ExternalCallPolicy::All &&
-       interpreterOpts.MockStrategy != MockStrategy::None) ||
+  if (interpreterOpts.ExternalCall == ExternalCallPolicy::Mock ||
+      interpreterOpts.ExternalCall == ExternalCallPolicy::MockDeterm ||
       !opts.AnnotationsFile.empty()) {
     MockBuilder mockBuilder(kmodule->module.get(), opts, ignoredExternals,
                             redefinitions, interpreterHandler);
@@ -975,11 +947,7 @@ void Executor::initializeGlobalObjects(ExecutionState &state) {
       } else {
         addr = externalDispatcher->resolveSymbol(v.getName().str());
       }
-      if (MockAllExternals && !addr) {
-        executeMakeSymbolic(
-            state, mo, typeSystemManager->getWrappedType(v.getType()),
-            SourceBuilder::irreproducible("mockExternGlobalObject"), false);
-      } else if (!addr) {
+      if (!addr) {
         klee_error("Unable to load symbol(%.*s) while initializing globals",
                    static_cast<int>(v.getName().size()), v.getName().data());
       } else {
@@ -2887,7 +2855,7 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) {
 
     if (auto *asmValue =
             dyn_cast<InlineAsm>(fp)) { // TODO: move to `executeCall`
-      if (ExternalCalls != ExternalCallPolicy::None) {
+      if (interpreterOpts.ExternalCall != ExternalCallPolicy::None) {
         KInlineAsm callable(asmValue);
         callExternalFunction(state, ki, &callable, arguments);
       } else {
@@ -4882,7 +4850,7 @@ void Executor::callExternalFunction(ExecutionState &state, KInstruction *target,
       return;
   }
 
-  if (ExternalCalls == ExternalCallPolicy::None &&
+  if (interpreterOpts.ExternalCall == ExternalCallPolicy::None &&
       !okExternals.count(callable->getName().str())) {
     klee_warning("Disallowed call to external function: %s\n",
                  callable->getName().str().c_str());
@@ -4890,28 +4858,6 @@ void Executor::callExternalFunction(ExecutionState &state, KInstruction *target,
     return;
   }
 
-  if (ExternalCalls == ExternalCallPolicy::All && MockAllExternals) {
-    std::string TmpStr;
-    llvm::raw_string_ostream os(TmpStr);
-    os << "calling external: " << callable->getName().str() << "(";
-    for (unsigned i = 0; i < arguments.size(); i++) {
-      os << arguments[i];
-      if (i != arguments.size() - 1)
-        os << ", ";
-    }
-    os << ") at " << state.pc->getSourceLocationString();
-
-    if (AllExternalWarnings)
-      klee_warning("%s", os.str().c_str());
-    else if (!SuppressExternalWarnings)
-      klee_warning_once(callable->getValue(), "%s", os.str().c_str());
-
-    if (target->inst->getType()->isSized()) {
-      prepareMockValue(state, "mockExternResult", target);
-    }
-    return;
-  }
-
   // normal external function handling path
   // allocate 512 bits for each argument (+return value) to support
   // fp80's and SIMD vectors as parameters for external calls;
@@ -4931,8 +4877,9 @@ void Executor::callExternalFunction(ExecutionState &state, KInstruction *target,
   for (std::vector<ref<Expr>>::iterator ai = arguments.begin(),
                                         ae = arguments.end();
        ai != ae; ++ai) {
-    if (ExternalCalls ==
-        ExternalCallPolicy::All) { // don't bother checking uniqueness
+    if (interpreterOpts.ExternalCall == ExternalCallPolicy::All ||
+        interpreterOpts.ExternalCall == ExternalCallPolicy::Mock ||
+        interpreterOpts.ExternalCall == ExternalCallPolicy::MockDeterm) { // don't bother checking uniqueness
       *ai = optimizer.optimizeExpr(*ai, true);
       ref<ConstantExpr> ce;
       bool success = solver->getValue(state.constraints.cs(), *ai, ce,
@@ -6082,10 +6029,10 @@ void Executor::executeMemoryOperation(
 
     ref<SolverResponse> response;
     solver->setTimeout(coreSolverTimeout);
-    bool success = solver->getResponse(state->constraints.cs(), inBounds,
-                                       response, state->queryMetaData);
+    bool solverResponse = solver->getResponse(state->constraints.cs(), inBounds,
+                                              response, state->queryMetaData);
     solver->setTimeout(time::Span());
-    if (!success) {
+    if (!solverResponse) {
       state->pc = state->prevPC;
       terminateStateOnSolverError(*state, "Query timed out (bounds check).");
       return;
diff --git a/lib/Core/SpecialFunctionHandler.cpp b/lib/Core/SpecialFunctionHandler.cpp
index 0066bb2e116..cf53aa70003 100644
--- a/lib/Core/SpecialFunctionHandler.cpp
+++ b/lib/Core/SpecialFunctionHandler.cpp
@@ -991,16 +991,14 @@ void SpecialFunctionHandler::handleMakeMock(ExecutionState &state,
 
     if (res) {
       ref<SymbolicSource> source;
-      switch (executor.interpreterOpts.MockStrategy) {
-      case MockStrategy::None:
-        klee_error("klee_make_mock is not allowed when mock strategy is none");
-        break;
-      case MockStrategy::Naive:
+      switch (executor.interpreterOpts.ExternalCall) {
+      case ExternalCallPolicy::Mock: {
         source =
             SourceBuilder::mockNaive(executor.kmodule.get(), *kf->function,
                                      executor.updateNameVersion(state, name));
         break;
-      case MockStrategy::Deterministic:
+      }
+      case ExternalCallPolicy::MockDeterm: {
         std::vector<ref<Expr>> args(kf->getNumArgs());
         for (size_t i = 0; i < kf->getNumArgs(); i++) {
           args[i] = executor.getArgumentCell(state, kf, i).value;
@@ -1009,6 +1007,13 @@ void SpecialFunctionHandler::handleMakeMock(ExecutionState &state,
                                                   *kf->function, args);
         break;
       }
+      case ExternalCallPolicy::Concrete:
+      case ExternalCallPolicy::All:
+      case ExternalCallPolicy::None: {
+        klee_error("klee_make_mock is not allowed when mock strategy is none");
+        break;
+      }
+      }
       executor.executeMakeSymbolic(state, mo, old->getDynamicType(), source,
                                    false);
     } else {
diff --git a/lib/Solver/Z3Builder.cpp b/lib/Solver/Z3Builder.cpp
index e3ea9b22afb..7cc873980c3 100644
--- a/lib/Solver/Z3Builder.cpp
+++ b/lib/Solver/Z3Builder.cpp
@@ -266,18 +266,16 @@ Z3ASTHandle Z3Builder::getInitialArray(const Array *root) {
     } else if (ref<MockDeterministicSource> mockDeterministicSource =
                    dyn_cast<MockDeterministicSource>(root->source)) {
       size_t num_args = mockDeterministicSource->args.size();
-      // TODO looks like too much vectors
-      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];
+        Z3ASTHandle argsHandle = construct(kid, &kidWidth);
+        args[i] = argsHandle;
+        Z3SortHandle z3SortHandle =
+            Z3SortHandle(Z3_get_sort(ctx, args[i]), ctx);
+        argsSort[i] = z3SortHandle;
       }
 
       Z3SortHandle domainSort = getBvSort(root->getDomain());
@@ -295,7 +293,7 @@ Z3ASTHandle Z3Builder::getInitialArray(const Array *root) {
           ctx);
       array_expr =
           Z3ASTHandle(Z3_mk_app(ctx, func, num_args, args.data()), ctx);
-    }  else {
+    } else {
       array_expr =
           buildArray(unique_name.c_str(), root->getDomain(), root->getRange());
     }
diff --git a/test/Feature/Annotation/AllocSource.c b/test/Feature/Annotation/AllocSource.c
index 2dc8cc4fe49..0c05748edb6 100644
--- a/test/Feature/Annotation/AllocSource.c
+++ b/test/Feature/Annotation/AllocSource.c
@@ -1,19 +1,19 @@
 // REQUIRES: z3
 // RUN: %clang -DAllocSource1 %s -g -emit-llvm %O0opt -c -o %t1.bc
 // RUN: rm -rf %t1.klee-out-1
-// RUN: %klee --solver-backend=z3 --output-dir=%t1.klee-out-1 --annotations=%S/AllocSource.json --external-calls=all --mock-all-externals --mock-external-calls --mock-linked-externals --mock-strategy=naive -emit-all-errors=true %t1.bc 2>&1 | FileCheck %s -check-prefix=CHECK-ALLOCSOURCE1
+// RUN: %klee --solver-backend=z3 --output-dir=%t1.klee-out-1 --annotations=%S/AllocSource.json --external-calls=mock --mock-modeled-functions -emit-all-errors=true %t1.bc 2>&1 | FileCheck %s -check-prefix=CHECK-ALLOCSOURCE1
 
 // RUN: %clang -DAllocSource2 %s -g -emit-llvm %O0opt -c -o %t2.bc
 // RUN: rm -rf %t2.klee-out-1
-// RUN: %klee --solver-backend=z3 --output-dir=%t2.klee-out-1 --annotations=%S/AllocSource.json --external-calls=all --mock-all-externals --mock-external-calls --mock-linked-externals --mock-strategy=naive -emit-all-errors=true %t2.bc 2>&1 | FileCheck %s -check-prefix=CHECK-ALLOCSOURCE2
+// RUN: %klee --solver-backend=z3 --output-dir=%t2.klee-out-1 --annotations=%S/AllocSource.json --external-calls=mock --mock-modeled-functions -emit-all-errors=true %t2.bc 2>&1 | FileCheck %s -check-prefix=CHECK-ALLOCSOURCE2
 
 // RUN: %clang -DAllocSource3 %s -g -emit-llvm %O0opt -c -o %t3.bc
 // RUN: rm -rf %t3.klee-out-1
-// RUN: %klee --solver-backend=z3 --output-dir=%t3.klee-out-1 --annotations=%S/AllocSource.json --external-calls=all --mock-all-externals --mock-external-calls --mock-linked-externals --mock-strategy=naive -emit-all-errors=true %t3.bc 2>&1 | FileCheck %s -check-prefix=CHECK-ALLOCSOURCE3
+// RUN: %klee --solver-backend=z3 --output-dir=%t3.klee-out-1 --annotations=%S/AllocSource.json --external-calls=mock --mock-modeled-functions -emit-all-errors=true %t3.bc 2>&1 | FileCheck %s -check-prefix=CHECK-ALLOCSOURCE3
 
 // RUN: %clang -DAllocSource4 %s -g -emit-llvm %O0opt -c -o %t4.bc
 // RUN: rm -rf %t4.klee-out-1
-// RUN: %klee --solver-backend=z3 --output-dir=%t4.klee-out-1 --annotations=%S/AllocSource.json --external-calls=all --mock-all-externals --mock-external-calls --mock-linked-externals --mock-strategy=naive -emit-all-errors=true %t4.bc 2>&1 | FileCheck %s -check-prefix=CHECK-ALLOCSOURCE4
+// RUN: %klee --solver-backend=z3 --output-dir=%t4.klee-out-1 --annotations=%S/AllocSource.json --external-calls=mock --mock-modeled-functions -emit-all-errors=true %t4.bc 2>&1 | FileCheck %s -check-prefix=CHECK-ALLOCSOURCE4
 
 #include <assert.h>
 
diff --git a/test/Feature/Annotation/Deref.c b/test/Feature/Annotation/Deref.c
index cb4097e8902..fafbe357cf7 100644
--- a/test/Feature/Annotation/Deref.c
+++ b/test/Feature/Annotation/Deref.c
@@ -1,36 +1,36 @@
 // REQUIRES: z3
 // RUN: %clang -DDeref1 %s -g -emit-llvm %O0opt -c -o %t1.bc
 // RUN: rm -rf %t1.klee-out-1
-// RUN: %klee --solver-backend=z3 --output-dir=%t1.klee-out-1 --annotations=%S/Deref.json --external-calls=all --mock-all-externals --mock-external-calls --mock-linked-externals --mock-strategy=naive -emit-all-errors=true %t1.bc 2>&1 | FileCheck %s -check-prefix=CHECK-DEREF1
+// RUN: %klee --solver-backend=z3 --output-dir=%t1.klee-out-1 --annotations=%S/Deref.json --external-calls=mock --mock-modeled-functions --emit-all-errors=true %t1.bc 2>&1 | FileCheck %s -check-prefix=CHECK-DEREF1
 
 // RUN: %clang -DDeref2 %s -g -emit-llvm %O0opt -c -o %t2.bc
 // RUN: rm -rf %t2.klee-out-1
-// RUN: %klee --solver-backend=z3 --output-dir=%t2.klee-out-1 --annotations=%S/Deref.json --external-calls=all --mock-all-externals --mock-external-calls --mock-linked-externals --mock-strategy=naive -emit-all-errors=true %t2.bc 2>&1 | FileCheck %s -check-prefix=CHECK-DEREF2
+// RUN: %klee --solver-backend=z3 --output-dir=%t2.klee-out-1 --annotations=%S/Deref.json --external-calls=mock --mock-modeled-functions --emit-all-errors=true %t2.bc 2>&1 | FileCheck %s -check-prefix=CHECK-DEREF2
 
 // RUN: %clang -DDeref3 %s -g -emit-llvm %O0opt -c -o %t3.bc
 // RUN: rm -rf %t3.klee-out-1
-// RUN: %klee --solver-backend=z3 --output-dir=%t3.klee-out-1 --annotations=%S/Deref.json --external-calls=all --mock-all-externals --mock-external-calls --mock-linked-externals --mock-strategy=naive -emit-all-errors=true %t3.bc 2>&1 | FileCheck %s -check-prefix=CHECK-DEREF3
+// RUN: %klee --solver-backend=z3 --output-dir=%t3.klee-out-1 --annotations=%S/Deref.json --external-calls=mock --mock-modeled-functions --emit-all-errors=true %t3.bc 2>&1 | FileCheck %s -check-prefix=CHECK-DEREF3
 
 // RUN: %clang -DDeref4 %s -g -emit-llvm %O0opt -c -o %t4.bc
 // RUN: rm -rf %t4.klee-out-1
-// RUN: %klee --solver-backend=z3 --output-dir=%t4.klee-out-1 --annotations=%S/Deref.json --external-calls=all --mock-all-externals --mock-external-calls --mock-linked-externals --mock-strategy=naive -emit-all-errors=true %t4.bc 2>&1 | FileCheck %s -check-prefix=CHECK-DEREF4
+// RUN: %klee --solver-backend=z3 --output-dir=%t4.klee-out-1 --annotations=%S/Deref.json --external-calls=mock --mock-modeled-functions --emit-all-errors=true %t4.bc 2>&1 | FileCheck %s -check-prefix=CHECK-DEREF4
 
 // RUN: %clang -DDeref5 %s -g -emit-llvm %O0opt -c -o %t5.bc
 // RUN: rm -rf %t5.klee-out-1
-// RUN: %klee --solver-backend=z3 --output-dir=%t5.klee-out-1 --annotations=%S/Deref.json --external-calls=all --mock-all-externals --mock-external-calls --mock-linked-externals --mock-strategy=naive -emit-all-errors=true %t5.bc 2>&1 | FileCheck %s -check-prefix=CHECK-DEREF5
+// RUN: %klee --solver-backend=z3 --output-dir=%t5.klee-out-1 --annotations=%S/Deref.json --external-calls=mock --mock-modeled-functions --emit-all-errors=true %t5.bc 2>&1 | FileCheck %s -check-prefix=CHECK-DEREF5
 
 // RUN: %clang -DDeref6 %s -g -emit-llvm %O0opt -c -o %t6.bc
 // RUN: rm -rf %t6.klee-out-1
-// RUN: %klee --solver-backend=z3 --output-dir=%t6.klee-out-1 --annotations=%S/Deref.json --external-calls=all --mock-all-externals --mock-external-calls --mock-linked-externals --mock-strategy=naive -emit-all-errors=true %t6.bc 2>&1 | FileCheck %s -check-prefix=CHECK-DEREF6
+// RUN: %klee --solver-backend=z3 --output-dir=%t6.klee-out-1 --annotations=%S/Deref.json --external-calls=mock --mock-modeled-functions --emit-all-errors=true %t6.bc 2>&1 | FileCheck %s -check-prefix=CHECK-DEREF6
 
 // RUN: %clang -DHASVALUE -DDeref1 -DDeref2 -DDeref3 -DDeref4 -DDeref5 -DDeref6 %s -g -emit-llvm %O0opt -c -o %t7.bc
 // RUN: rm -rf %t7.klee-out-1
-// RUN: %klee --solver-backend=z3 --output-dir=%t7.klee-out-1 --annotations=%S/Deref.json --external-calls=all --mock-all-externals --mock-external-calls --mock-linked-externals --mock-strategy=naive -emit-all-errors=true %t7.bc 2>&1 | FileCheck %s -check-prefix=CHECK-NODEREF
+// RUN: %klee --solver-backend=z3 --output-dir=%t7.klee-out-1 --annotations=%S/Deref.json --external-calls=mock --mock-modeled-functions --emit-all-errors=true %t7.bc 2>&1 | FileCheck %s -check-prefix=CHECK-NODEREF
 // CHECK-NODEREF-NOT: memory error: null pointer exception
 
 // RUN: %clang -DDeref1 -DDeref2 -DDeref3 -DDeref4 -DDeref5 -DDeref6 %s -g -emit-llvm %O0opt -c -o %t8.bc
 // RUN: rm -rf %t8.klee-out-1
-// RUN: %klee --solver-backend=z3 --output-dir=%t8.klee-out-1 --annotations=%S/EmptyAnnotation.json --external-calls=all --mock-all-externals --mock-external-calls --mock-linked-externals --mock-strategy=naive -emit-all-errors=true %t8.bc 2>&1 | FileCheck %s -check-prefix=CHECK-EMPTY
+// RUN: %klee --solver-backend=z3 --output-dir=%t8.klee-out-1 --annotations=%S/EmptyAnnotation.json --external-calls=mock --mock-modeled-functions --emit-all-errors=true %t8.bc 2>&1 | FileCheck %s -check-prefix=CHECK-EMPTY
 // CHECK-EMPTY-NOT: memory error: null pointer exception
 // CHECK-EMPTY: partially completed paths = 0
 // CHECK-EMPTY: generated tests = 1
diff --git a/test/Feature/Annotation/Free.c b/test/Feature/Annotation/Free.c
index fb364a82644..3ca6c9708dd 100644
--- a/test/Feature/Annotation/Free.c
+++ b/test/Feature/Annotation/Free.c
@@ -1,15 +1,15 @@
 // REQUIRES: z3
 // RUN: %clang -DFree1 %s -g -emit-llvm %O0opt -c -o %t1.bc
 // RUN: rm -rf %t1.klee-out-1
-// RUN: %klee --solver-backend=z3 --output-dir=%t1.klee-out-1 --annotations=%S/Free.json --external-calls=all --mock-all-externals --mock-external-calls --mock-linked-externals --mock-strategy=naive -emit-all-errors=true %t1.bc 2>&1 | FileCheck %s -check-prefix=CHECK-FREE1
+// RUN: %klee --solver-backend=z3 --output-dir=%t1.klee-out-1 --annotations=%S/Free.json --external-calls=mock --mock-modeled-functions --emit-all-errors=true %t1.bc 2>&1 | FileCheck %s -check-prefix=CHECK-FREE1
 
-// RUN: %clang %s -g -emit-llvm %O0opt -c -o %t1.bc
-// RUN: rm -rf %t1.klee-out-1
-// RUN: %klee --solver-backend=z3 --output-dir=%t1.klee-out-1 --annotations=%S/Free.json --external-calls=all --mock-all-externals --mock-external-calls --mock-linked-externals --mock-strategy=naive -emit-all-errors=true %t1.bc 2>&1 | FileCheck %s -check-prefix=CHECK-FREE2
+// RUN: %clang %s -g -emit-llvm %O0opt -c -o %t2.bc
+// RUN: rm -rf %t2.klee-out-1
+// RUN: %klee --solver-backend=z3 --output-dir=%t2.klee-out-1 --annotations=%S/Free.json --external-calls=mock --mock-modeled-functions --emit-all-errors=true %t2.bc 2>&1 | FileCheck %s -check-prefix=CHECK-FREE2
 
-// RUN: %clang -DFree3 %s -g -emit-llvm %O0opt -c -o %t1.bc
-// RUN: rm -rf %t1.klee-out-1
-// RUN: %klee --solver-backend=z3 --output-dir=%t1.klee-out-1 --annotations=%S/Free.json --external-calls=all --mock-all-externals --mock-external-calls --mock-linked-externals --mock-strategy=naive -emit-all-errors=true %t1.bc 2>&1 | FileCheck %s -check-prefix=CHECK-FREE3
+// RUN: %clang -DFree3 %s -g -emit-llvm %O0opt -c -o %t3.bc
+// RUN: rm -rf %t3.klee-out-1
+// RUN: %klee --solver-backend=z3 --output-dir=%t3.klee-out-1 --annotations=%S/Free.json --external-calls=mock --mock-modeled-functions --emit-all-errors=true %t3.bc 2>&1 | FileCheck %s -check-prefix=CHECK-FREE3
 
 #include <assert.h>
 
diff --git a/test/Feature/Annotation/General.c b/test/Feature/Annotation/General.c
index 76a122dc9d4..ad8a162e12a 100644
--- a/test/Feature/Annotation/General.c
+++ b/test/Feature/Annotation/General.c
@@ -1,17 +1,17 @@
 // REQUIRES: z3
 // RUN: %clang %s -g -emit-llvm %O0opt -c -o %t1.bc
 // RUN: rm -rf %t1.klee-out-1
-// RUN: %klee --solver-backend=z3 --output-dir=%t1.klee-out-1 --annotations=%S/BrokenAnnotation.json --external-calls=all --mock-all-externals --mock-external-calls --mock-linked-externals --mock-strategy=naive -emit-all-errors=true %t1.bc 2>%t.stderr.log || echo "Exit status must be 0"
+// RUN: %klee --solver-backend=z3 --output-dir=%t1.klee-out-1 --annotations=%S/BrokenAnnotation.json --external-calls=mock -emit-all-errors=true %t1.bc 2>%t.stderr.log || echo "Exit status must be 0"
 // RUN: FileCheck -check-prefix=CHECK-JSON --input-file=%t.stderr.log %s
 // CHECK-JSON: Annotation: Parsing JSON
 
 // RUN: %clang -DPTRARG %s -g -emit-llvm %O0opt -c -o %t2.bc
 // RUN: rm -rf %t2.klee-out-1
-// RUN: %klee --solver-backend=z3 --output-dir=%t2.klee-out-1 --annotations=%S/General.json --external-calls=all --mock-all-externals --mock-external-calls --mock-linked-externals --mock-strategy=naive -emit-all-errors=true %t2.bc 2>&1 | FileCheck %s -check-prefix=CHECK
+// RUN: %klee --solver-backend=z3 --output-dir=%t2.klee-out-1 --annotations=%S/General.json --external-calls=mock -emit-all-errors=true %t2.bc 2>&1 | FileCheck %s -check-prefix=CHECK
 
 // RUN: %clang -DPTRRET %s -g -emit-llvm %O0opt -c -o %t3.bc
 // RUN: rm -rf %t3.klee-out-1
-// RUN: %klee --solver-backend=z3 --output-dir=%t3.klee-out-1 --annotations=%S/General.json --external-calls=all --mock-all-externals --mock-external-calls --mock-linked-externals --mock-strategy=naive -emit-all-errors=true %t3.bc 2>&1 | FileCheck %s -check-prefix=CHECK
+// RUN: %klee --solver-backend=z3 --output-dir=%t3.klee-out-1 --annotations=%S/General.json --external-calls=mock -emit-all-errors=true %t3.bc 2>&1 | FileCheck %s -check-prefix=CHECK
 
 #include <assert.h>
 
diff --git a/test/Feature/Annotation/InitNull.c b/test/Feature/Annotation/InitNull.c
index 2f4d0c7b8c7..50df9542b7d 100644
--- a/test/Feature/Annotation/InitNull.c
+++ b/test/Feature/Annotation/InitNull.c
@@ -1,23 +1,23 @@
 // REQUIRES: z3
 // RUN: %clang -DInitNull1 %s -g -emit-llvm %O0opt -c -o %t1.bc
 // RUN: rm -rf %t1.klee-out-1
-// RUN: %klee --solver-backend=z3 --output-dir=%t1.klee-out-1 --annotations=%S/InitNull.json --external-calls=all --mock-all-externals --mock-external-calls --mock-linked-externals --mock-strategy=naive -emit-all-errors=true %t1.bc 2>&1 | FileCheck %s -check-prefix=CHECK-INITNULL1
+// RUN: %klee --solver-backend=z3 --output-dir=%t1.klee-out-1 --annotations=%S/InitNull.json --external-calls=mock -emit-all-errors=true %t1.bc 2>&1 | FileCheck %s -check-prefix=CHECK-INITNULL1
 
 // RUN: %clang -DInitNull2 %s -g -emit-llvm %O0opt -c -o %t2.bc
 // RUN: rm -rf %t2.klee-out-1
-// RUN: %klee --solver-backend=z3 --output-dir=%t2.klee-out-1 --annotations=%S/InitNull.json --external-calls=all --mock-all-externals --mock-external-calls --mock-linked-externals --mock-strategy=naive -emit-all-errors=true %t2.bc 2>&1 | FileCheck %s -check-prefix=CHECK-INITNULL2
+// RUN: %klee --solver-backend=z3 --output-dir=%t2.klee-out-1 --annotations=%S/InitNull.json --external-calls=mock -emit-all-errors=true %t2.bc 2>&1 | FileCheck %s -check-prefix=CHECK-INITNULL2
 
 // RUN: %clang -DInitNull3 %s -g -emit-llvm %O0opt -c -o %t3.bc
 // RUN: rm -rf %t3.klee-out-1
-// RUN: %klee --solver-backend=z3 --output-dir=%t3.klee-out-1 --annotations=%S/InitNull.json --external-calls=all --mock-all-externals --mock-external-calls --mock-linked-externals --mock-strategy=naive -emit-all-errors=true %t3.bc 2>&1 | FileCheck %s -check-prefix=CHECK-INITNULL3
+// RUN: %klee --solver-backend=z3 --output-dir=%t3.klee-out-1 --annotations=%S/InitNull.json --external-calls=mock -emit-all-errors=true %t3.bc 2>&1 | FileCheck %s -check-prefix=CHECK-INITNULL3
 
 // RUN: %clang -DInitNull4 %s -g -emit-llvm %O0opt -c -o %t4.bc
 // RUN: rm -rf %t4.klee-out-1
-// RUN: %klee --solver-backend=z3 --output-dir=%t4.klee-out-1 --annotations=%S/InitNull.json --external-calls=all --mock-all-externals --mock-external-calls --mock-linked-externals --mock-strategy=naive -emit-all-errors=true %t4.bc 2>&1 | FileCheck %s -check-prefix=CHECK-INITNULL4
+// RUN: %klee --solver-backend=z3 --output-dir=%t4.klee-out-1 --annotations=%S/InitNull.json --external-calls=mock -emit-all-errors=true %t4.bc 2>&1 | FileCheck %s -check-prefix=CHECK-INITNULL4
 
 // RUN: %clang -DInitNull1 -DInitNull2 -DInitNull3 -DInitNull4 %s -g -emit-llvm %O0opt -c -o %t5.bc
 // RUN: rm -rf %t5.klee-out-1
-// RUN: %klee --solver-backend=z3 --output-dir=%t5.klee-out-1 --annotations=%S/InitNullEmpty.json --external-calls=all --mock-all-externals --mock-external-calls --mock-linked-externals --mock-strategy=naive -emit-all-errors=true %t5.bc 2>&1 | FileCheck %s -check-prefix=CHECK-EMPTY
+// RUN: %klee --solver-backend=z3 --output-dir=%t5.klee-out-1 --annotations=%S/InitNullEmpty.json --external-calls=mock -emit-all-errors=true %t5.bc 2>&1 | FileCheck %s -check-prefix=CHECK-EMPTY
 // CHECK-EMPTY: ASSERTION FAIL: a != 0 && "A is Null"
 // CHECK-EMPTY: ASSERTION FAIL: a != 0 && "A is Null"
 // CHECK-EMPTY: partially completed paths = 2
diff --git a/test/Feature/MockPointersDeterministic.c b/test/Feature/MockPointersDeterministic.c
index 77881388521..d0ee2ccb25e 100644
--- a/test/Feature/MockPointersDeterministic.c
+++ b/test/Feature/MockPointersDeterministic.c
@@ -2,7 +2,7 @@
 // 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
+// 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=mock-determ %t.bc 2>&1 | FileCheck %s -check-prefix=CHECK-1
 // CHECK-1: memory error: null pointer exception
 // CHECK-1: memory error: out of bound pointer
 // CHECK-1: KLEE: done: completed paths = 1
diff --git a/test/Feature/MockStrategies.c b/test/Feature/MockStrategies.c
index 524fbba3a2d..36188179387 100644
--- a/test/Feature/MockStrategies.c
+++ b/test/Feature/MockStrategies.c
@@ -2,23 +2,23 @@
 // 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
+// RUN: %klee --output-dir=%t.klee-out-1 --external-calls=all %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
+// RUN: %klee --output-dir=%t.klee-out-2 --external-calls=mock %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
+// RUN: not %klee --output-dir=%t.klee-out-3 --solver-backend=stp --external-calls=mock-determ %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
+// RUN: %klee --output-dir=%t.klee-out-4 --solver-backend=z3 --external-calls=mock-determ %t.bc 2>&1 | FileCheck %s -check-prefix=CHECK-4
 // CHECK-4: KLEE: done: completed paths = 2
 // CHECK-4: KLEE: done: generated tests = 2
 
diff --git a/test/Industry/egcd3-ll_valuebound10.c b/test/Industry/egcd3-ll_valuebound10.c
index 5fd1bc76d19..a3809004c15 100644
--- a/test/Industry/egcd3-ll_valuebound10.c
+++ b/test/Industry/egcd3-ll_valuebound10.c
@@ -1,6 +1,6 @@
 // RUN: %clang %s -emit-llvm %O0opt -g -c -o %t1.bc
 // RUN: rm -rf %t.klee-out
-// RUN: %klee --output-dir=%t.klee-out --delete-dead-loops=false --emit-all-errors --mock-all-externals --use-forked-solver=false --max-memory=6008 --optimize --skip-not-lazy-initialized --output-source=false --output-stats=true --output-istats=true -istats-write-interval=90s --use-sym-size-alloc=true --cex-cache-validity-cores --symbolic-allocation-threshold=8192 --max-solver-time=5s --track-coverage=branches --use-iterative-deepening-search=max-cycles --cover-on-the-fly=false --delay-cover-on-the-fly=400000 --only-output-states-covering-new --dump-states-on-halt=true --search=dfs --search=random-state %t1.bc
+// RUN: %klee --output-dir=%t.klee-out --delete-dead-loops=false --emit-all-errors --use-forked-solver=false --max-memory=6008 --optimize --skip-not-lazy-initialized --output-source=false --output-stats=true --output-istats=true -istats-write-interval=90s --use-sym-size-alloc=true --cex-cache-validity-cores --symbolic-allocation-threshold=8192 --max-solver-time=5s --track-coverage=branches --use-iterative-deepening-search=max-cycles --cover-on-the-fly=false --delay-cover-on-the-fly=400000 --only-output-states-covering-new --dump-states-on-halt=true --search=dfs --search=random-state %t1.bc
 // RUN: %klee-stats --print-columns 'BCov(%)' --table-format=csv %t.klee-out > %t.stats
 // RUN: FileCheck -input-file=%t.stats %s
 // CHECK: BCov(%)
diff --git a/test/Industry/pals_lcr.3.ufo.UNBOUNDED.pals+Problem12_label00.c b/test/Industry/pals_lcr.3.ufo.UNBOUNDED.pals+Problem12_label00.c
index 0c49afc42ec..4e340cbd73f 100644
--- a/test/Industry/pals_lcr.3.ufo.UNBOUNDED.pals+Problem12_label00.c
+++ b/test/Industry/pals_lcr.3.ufo.UNBOUNDED.pals+Problem12_label00.c
@@ -1,7 +1,7 @@
 // REQUIRES: geq-llvm-14.0
 // RUN: %clang %s -emit-llvm %O0opt -g -c -o %t1.bc
 // RUN: rm -rf %t.klee-out
-// RUN: %klee --output-dir=%t.klee-out --optimize-aggressive=false --track-coverage=branches --delete-dead-loops=false --emit-all-errors --mock-all-externals --use-forked-solver=false --optimize --skip-not-lazy-initialized --output-source=false --output-stats=true --output-istats=true -istats-write-interval=3s --use-sym-size-alloc=true --cex-cache-validity-cores --symbolic-allocation-threshold=8192 --cover-on-the-fly=false --delay-cover-on-the-fly=400000 --only-output-states-covering-new --dump-states-on-halt=true --search=dfs --search=random-state --use-iterative-deepening-search=max-cycles --max-cycles=4 %t1.bc
+// RUN: %klee --output-dir=%t.klee-out --optimize-aggressive=false --track-coverage=branches --delete-dead-loops=false --emit-all-errors --external-calls=mock --use-forked-solver=false --optimize --skip-not-lazy-initialized --output-source=false --output-stats=true --output-istats=true -istats-write-interval=3s --use-sym-size-alloc=true --cex-cache-validity-cores --symbolic-allocation-threshold=8192 --cover-on-the-fly=false --delay-cover-on-the-fly=400000 --only-output-states-covering-new --dump-states-on-halt=true --search=dfs --search=random-state --use-iterative-deepening-search=max-cycles --max-cycles=4 %t1.bc
 // RUN: %klee-stats --print-columns 'BCov(%)' --table-format=csv %t.klee-out > %t.stats
 // RUN: FileCheck -input-file=%t.stats %s
 
diff --git a/test/Replay/libkleeruntest/replay_mocks.c b/test/Replay/libkleeruntest/replay_mocks.c
index 12995fe7cef..823ce386987 100644
--- a/test/Replay/libkleeruntest/replay_mocks.c
+++ b/test/Replay/libkleeruntest/replay_mocks.c
@@ -2,7 +2,7 @@
 // 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: %klee --output-dir=%t.klee-out --external-calls=mock %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
diff --git a/test/regression/2023-10-02-test-from-mocked-global.c b/test/regression/2023-10-02-test-from-mocked-global.c
index a62eeb9bba0..4ad699b0485 100644
--- a/test/regression/2023-10-02-test-from-mocked-global.c
+++ b/test/regression/2023-10-02-test-from-mocked-global.c
@@ -2,7 +2,7 @@
 // REQUIRES: not-darwin
 // RUN: %clang %s -g -emit-llvm %O0opt -c -o %t1.bc
 // RUN: rm -rf %t.klee-out
-// RUN: %klee --mock-all-externals --write-xml-tests --output-dir=%t.klee-out %t1.bc
+// RUN: %klee --external-calls=mock --write-xml-tests --output-dir=%t.klee-out %t1.bc
 // RUN: FileCheck --input-file %t.klee-out/test000001.xml %s
 
 extern void *__crc_mc44s803_attach __attribute__((__weak__));
@@ -13,4 +13,4 @@ int main() {
   return 0;
 }
 
-// CHECK-NOT: <input
\ No newline at end of file
+// CHECK: @external___crc_mc44s803_attach
diff --git a/test/regression/2023-10-13-kbfiltr.i.cil-2.c b/test/regression/2023-10-13-kbfiltr.i.cil-2.c
index d46b8535263..1c851a33ce5 100644
--- a/test/regression/2023-10-13-kbfiltr.i.cil-2.c
+++ b/test/regression/2023-10-13-kbfiltr.i.cil-2.c
@@ -1,7 +1,7 @@
 // REQUIRES: geq-llvm-14.0
 // RUN: %clang  -Wno-everything %s -emit-llvm %O0opt -g -c -o %t1.bc
 // RUN: rm -rf %t.klee-out
-// RUN: %klee --output-dir=%t.klee-out --optimize-aggressive=false --track-coverage=branches --optimize=true --mock-all-externals --external-calls=all --use-forked-solver=false --max-memory=6008 --skip-not-lazy-initialized --istats-write-interval=90s --use-sym-size-alloc=true --cex-cache-validity-cores --symbolic-allocation-threshold=8192 --write-kqueries --write-xml-tests --only-output-states-covering-new=true --dump-states-on-halt=true --emit-all-errors=true --search=bfs %t1.bc
+// RUN: %klee --output-dir=%t.klee-out --optimize-aggressive=false --track-coverage=branches --optimize=true --mock-all-externals --external-calls=mock --use-forked-solver=false --max-memory=6008 --skip-not-lazy-initialized --istats-write-interval=90s --use-sym-size-alloc=true --cex-cache-validity-cores --symbolic-allocation-threshold=8192 --write-kqueries --write-xml-tests --only-output-states-covering-new=true --dump-states-on-halt=true --emit-all-errors=true --search=bfs %t1.bc
 
 // RUN: test -f %t.klee-out/test000023_1.xml
 #include "klee-test-comp.c"
diff --git a/tools/klee/main.cpp b/tools/klee/main.cpp
index 688f8ae5783..90f9156a590 100644
--- a/tools/klee/main.cpp
+++ b/tools/klee/main.cpp
@@ -364,45 +364,49 @@ cl::opt<std::string> XMLMetadataProgramHash(
     llvm::cl::desc("Test-Comp hash sum of original file for xml metadata"),
     llvm::cl::cat(TestCompCat));
 
-
 /*** 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));
+    "mock-modeled-functions",
+    cl::desc("Link modeled mocks from libkleeRuntimeMocks (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::opt<ExternalCallPolicy> ExternalCalls(
+    "external-calls", cl::desc("Specify the external call policy"),
     cl::values(
-        clEnumValN(MockStrategy::None, "none",
-                   "External calls are not mocked (default)"),
-        clEnumValN(MockStrategy::Naive, "naive",
+        clEnumValN(
+            ExternalCallPolicy::None, "none",
+            "No external function calls are allowed.  Note that KLEE always "
+            "allows some external calls with concrete arguments to go through "
+            "(in particular printf and puts), regardless of this option."),
+        clEnumValN(ExternalCallPolicy::Concrete, "concrete",
+                   "Only external function calls with concrete arguments are "
+                   "allowed (default)"),
+        clEnumValN(ExternalCallPolicy::All, "all",
+                   "All external function calls are allowed.  This concretizes "
+                   "any symbolic arguments in calls to external functions."),
+        clEnumValN(ExternalCallPolicy::Mock, "mock",
                    "Every time external function is called, new symbolic value "
                    "is generated for its return value"),
-        clEnumValN(
-            MockStrategy::Deterministic, "deterministic",
+        clEnumValN(ExternalCallPolicy::MockDeterm, "mock-determ",
             "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));
+    cl::init(ExternalCallPolicy::Concrete), cl::cat(MockCat));
 
 /*** Annotations options ***/
 
-cl::OptionCategory AnnotCat("Annotations category");
-
 cl::opt<std::string>
     AnnotationsFile("annotations", cl::desc("Path to the annotation JSON file"),
-                    cl::value_desc("path file"), cl::cat(AnnotCat));
+                    cl::value_desc("path file"), cl::cat(MockCat));
 
 cl::opt<bool> AnnotateOnlyExternal(
     "annotate-only-external",
     cl::desc("Ignore annotations for defined function (default=false)"),
-    cl::init(false), cl::cat(AnnotCat));
+    cl::init(false), cl::cat(MockCat));
 
 } // namespace
 
@@ -1879,13 +1883,14 @@ int main(int argc, char **argv, char **envp) {
     klee_error("Entry function '%s' not found in module.", EntryPoint.c_str());
 
   std::vector<std::pair<std::string, std::string>> redefinitions;
+  if (ExternalCalls == ExternalCallPolicy::Mock ||
+      ExternalCalls == ExternalCallPolicy::MockDeterm) {
+    redefinitions.emplace_back(EntryPoint, Opts.MainNameAfterMock);
+  }
   if (MockLinkedExternals) {
     mockLinkedExternals(Opts, ctx, mainModule, loadedLibsModules,
                         redefinitions);
   }
-  if (MockUnlinkedStrategy != MockStrategy::None) {
-    redefinitions.emplace_back(EntryPoint, Opts.MainNameAfterMock);
-  }
 
   if (WithPOSIXRuntime) {
     SmallString<128> Path(Opts.LibraryDir);
@@ -2055,7 +2060,7 @@ int main(int argc, char **argv, char **envp) {
   Interpreter::InterpreterOptions IOpts(paths);
   IOpts.MakeConcreteSymbolic = MakeConcreteSymbolic;
   IOpts.Guidance = UseGuidedSearch;
-  IOpts.MockStrategy = MockUnlinkedStrategy;
+  IOpts.ExternalCall = ExternalCalls;
   std::unique_ptr<Interpreter> interpreter(
       Interpreter::create(ctx, IOpts, handler.get()));
   theInterpreter = interpreter.get();