diff --git a/include/klee/Module/KInstruction.h b/include/klee/Module/KInstruction.h
index 6d7df7973d..2ec40f3392 100644
--- a/include/klee/Module/KInstruction.h
+++ b/include/klee/Module/KInstruction.h
@@ -73,7 +73,7 @@ struct KInstruction : public KValue {
   /// register indices.
   int *operands;
   KBlock *parent;
-  mutable std::optional<LocationInfo> locationInfo;
+  mutable std::optional<ref<LocationInfo>> locationInfo;
 
 private:
   // Instruction index in the basic block
diff --git a/include/klee/Module/LocationInfo.h b/include/klee/Module/LocationInfo.h
index 043e85cac4..4ddc73fcaa 100644
--- a/include/klee/Module/LocationInfo.h
+++ b/include/klee/Module/LocationInfo.h
@@ -10,9 +10,13 @@
 #ifndef KLEE_LOCATIONINFO_H
 #define KLEE_LOCATIONINFO_H
 
+#include "klee/ADT/Ref.h"
+
 #include <cstdint>
+#include <functional>
 #include <optional>
 #include <string>
+#include <unordered_set>
 
 namespace llvm {
 class Function;
@@ -23,12 +27,16 @@ class Module;
 
 namespace klee {
 struct PhysicalLocationJson;
-}
+struct LocationInfo;
+} // namespace klee
 
 namespace klee {
 
 /// @brief Immutable struct representing location in source code.
 struct LocationInfo {
+  /// @brief Required by klee::ref-managed objects
+  class ReferenceCounter _refCount;
+
   /// @brief Path to source file for that location.
   const std::string file;
 
@@ -44,14 +52,73 @@ struct LocationInfo {
   /// @return SARIFs representation of location.
   PhysicalLocationJson serialize() const;
 
+  static ref<LocationInfo> create(std::string file, uint64_t line,
+                                  std::optional<uint64_t> column) {
+    LocationInfo *locationInfo = new LocationInfo(file, line, column);
+    return createCachedLocationInfo(locationInfo);
+  }
+
   bool operator==(const LocationInfo &rhs) const {
     return file == rhs.file && line == rhs.line && column == rhs.column;
   }
+
+  bool equals(const LocationInfo &b) const { return *this == b; }
+
+  ~LocationInfo() {
+    if (isCached) {
+      toBeCleared = true;
+      cachedLocationInfo.cache.erase(this);
+    }
+  }
+
+private:
+  LocationInfo(std::string file, uint64_t line, std::optional<uint64_t> column)
+      : file(file), line(line), column(column) {}
+
+  struct LocationInfoHash {
+    std::size_t operator()(LocationInfo *const s) const noexcept {
+      std::size_t r = 0;
+      std::size_t h1 = std::hash<std::string>{}(s->file);
+      std::size_t h2 = std::hash<uint64_t>{}(s->line);
+      std::size_t h3 = std::hash<std::optional<uint64_t>>{}(s->column);
+      r ^= h1 + 0x9e3779b9 + (r << 6) + (r >> 2);
+      r ^= h2 + 0x9e3779b9 + (r << 6) + (r >> 2);
+      r ^= h3 + 0x9e3779b9 + (r << 6) + (r >> 2);
+      return r;
+    }
+  };
+
+  struct LocationInfoCmp {
+    bool operator()(LocationInfo *const a, LocationInfo *const b) const {
+      return *a == *b;
+    }
+  };
+
+  using CacheType =
+      std::unordered_set<LocationInfo *, LocationInfoHash, LocationInfoCmp>;
+
+  struct LocationInfoCacheSet {
+    CacheType cache;
+    ~LocationInfoCacheSet() {
+      while (cache.size() != 0) {
+        ref<LocationInfo> tmp = *cache.begin();
+        tmp->isCached = false;
+        cache.erase(cache.begin());
+      }
+    }
+  };
+
+  static LocationInfoCacheSet cachedLocationInfo;
+  bool isCached = false;
+  bool toBeCleared = false;
+
+  static ref<LocationInfo>
+  createCachedLocationInfo(ref<LocationInfo> locationInfo);
 };
 
-LocationInfo getLocationInfo(const llvm::Function *func);
-LocationInfo getLocationInfo(const llvm::Instruction *inst);
-LocationInfo getLocationInfo(const llvm::GlobalVariable *global);
+ref<LocationInfo> getLocationInfo(const llvm::Function *func);
+ref<LocationInfo> getLocationInfo(const llvm::Instruction *inst);
+ref<LocationInfo> getLocationInfo(const llvm::GlobalVariable *global);
 
 } // namespace klee
 
diff --git a/lib/Core/CodeLocation.cpp b/lib/Core/CodeLocation.cpp
index ee62003580..fc498a8b26 100644
--- a/lib/Core/CodeLocation.cpp
+++ b/lib/Core/CodeLocation.cpp
@@ -24,8 +24,8 @@ CodeLocation::CodeLocation(const Path::PathIndex &pathIndex,
                            uint64_t sourceCodeLine,
                            std::optional<uint64_t> sourceCodeColumn)
     : pathIndex(pathIndex), source(source),
-      location(LocationInfo{sourceFilename, sourceCodeLine, sourceCodeColumn}) {
-}
+      location(LocationInfo::create(sourceFilename, sourceCodeLine,
+                                    sourceCodeColumn)) {}
 
 ref<CodeLocation>
 CodeLocation::create(const Path::PathIndex &pathIndex, const KValue *source,
@@ -44,7 +44,7 @@ CodeLocation::create(const KValue *source, const std::string &sourceFilename,
 }
 
 PhysicalLocationJson CodeLocation::serialize() const {
-  return location.serialize();
+  return location->serialize();
 }
 
 bool CodeLocation::equals(const CodeLocation &b) const {
diff --git a/lib/Core/CodeLocation.h b/lib/Core/CodeLocation.h
index 2e46ca8755..7cae990096 100644
--- a/lib/Core/CodeLocation.h
+++ b/lib/Core/CodeLocation.h
@@ -16,6 +16,7 @@
 #include <cstdint>
 #include <optional>
 #include <string>
+#include <unordered_set>
 
 namespace klee {
 
@@ -35,7 +36,7 @@ struct CodeLocation {
   const KValue *source;
 
   /// @brief Location in source code.
-  const LocationInfo location;
+  const ref<LocationInfo> location;
 
 private:
   CodeLocation(const Path::PathIndex &pathIndex, const KValue *source,
diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp
index ab94e30b2c..6014b1b33a 100644
--- a/lib/Core/Executor.cpp
+++ b/lib/Core/Executor.cpp
@@ -104,6 +104,7 @@
 #include <cassert>
 #include <cerrno>
 #include <cinttypes>
+#include <cstddef>
 #include <cstdint>
 #include <cstring>
 #include <cxxabi.h>
diff --git a/lib/Core/StatsTracker.cpp b/lib/Core/StatsTracker.cpp
index d9e5996e95..51a1754aad 100644
--- a/lib/Core/StatsTracker.cpp
+++ b/lib/Core/StatsTracker.cpp
@@ -758,7 +758,7 @@ void StatsTracker::writeIStats() {
       // Always try to write the filename before the function name, as otherwise
       // KCachegrind can create two entries for the function, one with an
       // unnamed file and one without.
-      auto fnlFile = getLocationInfo(&fn).file;
+      auto fnlFile = getLocationInfo(&fn)->file;
       if (fnlFile != sourceFile) {
         of << "fl=" << fnlFile << "\n";
         sourceFile = fnlFile;
@@ -772,9 +772,9 @@ void StatsTracker::writeIStats() {
           auto instrLI = getLocationInfo(instrPtr);
 
           unsigned index = executor.kmodule->getGlobalIndex(instrPtr);
-          if (instrLI.file != sourceFile) {
-            of << "fl=" << instrLI.file << "\n";
-            sourceFile = instrLI.file;
+          if (instrLI->file != sourceFile) {
+            of << "fl=" << instrLI->file << "\n";
+            sourceFile = instrLI->file;
           }
 
           {
@@ -783,7 +783,7 @@ void StatsTracker::writeIStats() {
             of << asmLine.value() << " ";
           }
 
-          of << instrLI.line << " ";
+          of << instrLI->line << " ";
           for (unsigned i = 0; i < nStats; i++)
             if (istatsMask.test(i))
               of << sm.getIndexedValue(sm.getStatistic(i), index) << " ";
@@ -797,8 +797,8 @@ void StatsTracker::writeIStats() {
                 const Function *f = fit.first;
                 CallSiteInfo &csi = fit.second;
                 auto fli = getLocationInfo(f);
-                if (fli.file != "" && fli.file != sourceFile)
-                  of << "cfl=" << fli.file << "\n";
+                if (fli->file != "" && fli->file != sourceFile)
+                  of << "cfl=" << fli->file << "\n";
                 of << "cfn=" << f->getName().str() << "\n";
                 of << "calls=" << csi.count << " ";
 
@@ -808,7 +808,7 @@ void StatsTracker::writeIStats() {
                   of << asmLine.value() << " ";
                 }
 
-                of << fli.line << "\n";
+                of << fli->line << "\n";
 
                 {
                   auto asmLine = executor.kmodule->getAsmLine(instrPtr);
@@ -816,7 +816,7 @@ void StatsTracker::writeIStats() {
                   of << asmLine.value() << " ";
                 }
 
-                of << instrLI.line << " ";
+                of << instrLI->line << " ";
                 for (unsigned i = 0; i < nStats; i++) {
                   if (istatsMask.test(i)) {
                     Statistic &s = sm.getStatistic(i);
diff --git a/lib/Module/KInstruction.cpp b/lib/Module/KInstruction.cpp
index 999a309562..e0dc4435fc 100644
--- a/lib/Module/KInstruction.cpp
+++ b/lib/Module/KInstruction.cpp
@@ -73,21 +73,21 @@ size_t KInstruction::getLine() const {
   if (!this->locationInfo.has_value()) {
     this->locationInfo.emplace(getLocationInfo(inst()));
   }
-  return this->locationInfo.value().line;
+  return this->locationInfo.value()->line;
 }
 
 size_t KInstruction::getColumn() const {
   if (!this->locationInfo.has_value()) {
     this->locationInfo.emplace(getLocationInfo(inst()));
   }
-  return this->locationInfo.value().column.value_or(0);
+  return this->locationInfo.value()->column.value_or(0);
 }
 
 std::string KInstruction::getSourceFilepath() const {
   if (!this->locationInfo.has_value()) {
     this->locationInfo.emplace(getLocationInfo(inst()));
   }
-  return this->locationInfo.value().file;
+  return this->locationInfo.value()->file;
 }
 
 std::string KInstruction::getSourceLocationString() const {
diff --git a/lib/Module/KModule.cpp b/lib/Module/KModule.cpp
index f3a9437f15..96b9983751 100644
--- a/lib/Module/KModule.cpp
+++ b/lib/Module/KModule.cpp
@@ -461,11 +461,11 @@ KGlobalVariable::KGlobalVariable(llvm::GlobalVariable *global, unsigned id)
     : KValue(global, KValue::Kind::GLOBAL_VARIABLE), id(id) {}
 
 std::string KGlobalVariable::getSourceFilepath() const {
-  return getLocationInfo(globalVariable()).file;
+  return getLocationInfo(globalVariable())->file;
 }
 // Line number where the global variable is defined
 size_t KGlobalVariable::getLine() const {
-  return getLocationInfo(globalVariable()).line;
+  return getLocationInfo(globalVariable())->line;
 }
 
 bool KGlobalVariable::operator<(const KValue &rhs) const {
@@ -531,12 +531,12 @@ KFunction::KFunction(llvm::Function *_function, KModule *_km,
 
 size_t KFunction::getLine() const {
   auto locationInfo = getLocationInfo(function());
-  return locationInfo.line;
+  return locationInfo->line;
 }
 
 std::string KFunction::getSourceFilepath() const {
   auto locationInfo = getLocationInfo(function());
-  return locationInfo.file;
+  return locationInfo->file;
 }
 
 KFunction::~KFunction() {
diff --git a/lib/Module/LocationInfo.cpp b/lib/Module/LocationInfo.cpp
index dec8d317d5..bfaf48fb02 100644
--- a/lib/Module/LocationInfo.cpp
+++ b/lib/Module/LocationInfo.cpp
@@ -44,18 +44,34 @@ PhysicalLocationJson LocationInfo::serialize() const {
 
 ////////////////////////////////////////////////////////////////
 
-LocationInfo getLocationInfo(const llvm::Function *func) {
+LocationInfo::LocationInfoCacheSet LocationInfo::cachedLocationInfo;
+
+ref<LocationInfo>
+LocationInfo::createCachedLocationInfo(ref<LocationInfo> locationInfo) {
+  std::pair<CacheType::const_iterator, bool> success =
+      cachedLocationInfo.cache.insert(locationInfo.get());
+
+  if (success.second) {
+    // Cache miss
+    locationInfo->isCached = true;
+    return locationInfo;
+  }
+  // Cache hit
+  return (ref<LocationInfo>)*(success.first);
+}
+
+ref<LocationInfo> getLocationInfo(const llvm::Function *func) {
   const auto dsub = func->getSubprogram();
 
   if (dsub != nullptr) {
     auto path = dsub->getFilename();
-    return {path.str(), dsub->getLine(), {}};
+    return LocationInfo::create(path.str(), dsub->getLine(), {});
   }
 
-  return {"", 0, {}};
+  return LocationInfo::create("", 0, {});
 }
 
-LocationInfo getLocationInfo(const llvm::Instruction *inst) {
+ref<LocationInfo> getLocationInfo(const llvm::Instruction *inst) {
   // Retrieve debug information associated with instruction
   const auto &dl = inst->getDebugLoc();
 
@@ -74,13 +90,13 @@ LocationInfo getLocationInfo(const llvm::Instruction *inst) {
         column = LexicalBlock->getColumn();
       }
     }
-    return {full_path.str(), line, {column}};
+    return LocationInfo::create(full_path.str(), line, {column});
   }
 
   return getLocationInfo(inst->getParent()->getParent());
 }
 
-LocationInfo getLocationInfo(const llvm::GlobalVariable *globalVar) {
+ref<LocationInfo> getLocationInfo(const llvm::GlobalVariable *globalVar) {
   // Retrieve debug information associated with global variable.
   // LLVM does not expose API for getting single DINode with location
   // information.
@@ -91,20 +107,19 @@ LocationInfo getLocationInfo(const llvm::GlobalVariable *globalVar) {
     // Return location from any debug info for global variable.
     if (const llvm::DIGlobalVariable *debugInfoGlobalVar =
             debugInfoEntry->getVariable()) {
-      return {debugInfoGlobalVar->getFilename().str(),
-              debugInfoGlobalVar->getLine(),
-              {}};
+      return LocationInfo::create(debugInfoGlobalVar->getFilename().str(),
+                                  debugInfoGlobalVar->getLine(), {});
     }
   }
 
   // For `extern` variables return `external` file.
   if (globalVar->hasExternalLinkage()) {
-    return {"external", 0, {}};
+    return LocationInfo::create("external", 0, {});
   }
 
   // Fallback to empty location if there is no appropriate debug
   // info.
-  return {"", 0, {}};
+  return LocationInfo::create("", 0, {});
 }
 
 } // namespace klee
diff --git a/lib/Module/SarifReport.cpp b/lib/Module/SarifReport.cpp
index 13a5fae844..580233a2b6 100644
--- a/lib/Module/SarifReport.cpp
+++ b/lib/Module/SarifReport.cpp
@@ -357,19 +357,19 @@ bool Location::isInside(const llvm::Function *f,
   auto firstLoc = getLocationInfo(first);
   auto lastLoc = getLocationInfo(last);
   if (!startColumn.has_value()) {
-    if (firstLoc.line > endLine) {
+    if (firstLoc->line > endLine) {
       return false;
     }
-    return startLine <= lastLoc.line;
+    return startLine <= lastLoc->line;
   }
   for (const auto &block : *f) {
     for (const auto &inst : block) {
       auto locInfo = getLocationInfo(&inst);
-      if (!isa<DbgInfoIntrinsic>(&inst) && locInfo.line <= endLine &&
-          locInfo.line >= startLine && locInfo.column <= *endColumn &&
-          locInfo.column >= *startColumn &&
-          origInsts.at(locInfo.line)
-                  .at(locInfo.column.value_or(0))
+      if (!isa<DbgInfoIntrinsic>(&inst) && locInfo->line <= endLine &&
+          locInfo->line >= startLine && locInfo->column <= *endColumn &&
+          locInfo->column >= *startColumn &&
+          origInsts.at(locInfo->line)
+                  .at(locInfo->column.value_or(0))
                   .count(inst.getOpcode()) != 0) {
         return true;
       }
diff --git a/test/Industry/CoverageBranches/btor2c-lazyMod.h_b04.c b/test/Industry/CoverageBranches/btor2c-lazyMod.h_b04.c
new file mode 100644
index 0000000000..bc6506c601
--- /dev/null
+++ b/test/Industry/CoverageBranches/btor2c-lazyMod.h_b04.c
@@ -0,0 +1,133 @@
+// This file is part of the SV-Benchmarks collection of verification tasks:
+// https://gitlab.com/sosy-lab/benchmarking/sv-benchmarks
+//
+// SPDX-FileCopyrightText: 2020 Aman Goel
+// SPDX-FileCopyrightText: 2022 The SV-Benchmarks Community
+//
+// SPDX-License-Identifier: GPL-3.0-or-later
+
+// This C program is converted from Btor2 by Btor2C version sha1:a0fa249
+//   with arguments: { architecture=64, lazy_modulo=true, use_memmove=false, unroll_inner_loops=false, shortest_type=true, diff_type=true, decimal_constant=true, zero_init=false, sra_extend_sign=true }
+// Comments from the original Btor2 file:
+// ; source: https://github.com/aman-goel/avr/tree/92362931700b66684418a991d018c9fbdbebc06f/tests
+// ; BTOR description generated by Yosys 0.9+431 (git sha1 4a3b5437, clang 4.0.1-6 -fPIC -Os) for module main.
+extern unsigned char __VERIFIER_nondet_uchar();
+extern unsigned short __VERIFIER_nondet_ushort();
+extern unsigned int __VERIFIER_nondet_uint();
+extern unsigned long __VERIFIER_nondet_ulong();
+extern void abort(void);
+extern void __assert_fail(const char *, const char *, unsigned int, const char *);
+void reach_error() { __assert_fail("0", "h_b04.c", 0, "reach_error"); }
+void __VERIFIER_assert(int cond) { if (!(cond)) { ERROR: { reach_error(); abort(); } } }
+void assume_abort_if_not(int cond) { if (!cond) { abort(); } }
+int main() {
+  // Defining sorts ...
+  typedef unsigned char SORT_1;  // BV with 1 bits
+  const SORT_1 mask_SORT_1 = (SORT_1)-1 >> (sizeof(SORT_1) * 8 - 1);
+  const SORT_1 msb_SORT_1 = (SORT_1)1 << (1 - 1);
+  typedef unsigned char SORT_4;  // BV with 8 bits
+  const SORT_4 mask_SORT_4 = (SORT_4)-1 >> (sizeof(SORT_4) * 8 - 8);
+  const SORT_4 msb_SORT_4 = (SORT_4)1 << (8 - 1);
+  typedef unsigned int SORT_12;  // BV with 32 bits
+  const SORT_12 mask_SORT_12 = (SORT_12)-1 >> (sizeof(SORT_12) * 8 - 32);
+  const SORT_12 msb_SORT_12 = (SORT_12)1 << (32 - 1);
+  // Initializing constants ...
+  const SORT_4 var_8 = 0;
+  const SORT_12 var_14 = 1;
+  const SORT_1 var_25 = 1;
+  const SORT_1 var_42 = 0;
+  // Collecting input declarations ...
+  SORT_1 input_2;
+  SORT_1 input_3;
+  SORT_4 input_5;
+  SORT_1 input_6;
+  SORT_1 input_7;
+  SORT_4 input_29;
+  SORT_4 input_31;
+  SORT_4 input_33;
+  SORT_4 input_35;
+  SORT_4 input_37;
+  SORT_4 input_39;
+  // Collecting state declarations ...
+  SORT_4 state_9 = __VERIFIER_nondet_uchar() & mask_SORT_4;
+  SORT_4 state_17 = __VERIFIER_nondet_uchar() & mask_SORT_4;
+  SORT_1 state_43 = __VERIFIER_nondet_uchar() & mask_SORT_1;
+  // Initializing states ...
+  SORT_4 init_10_arg_1 = var_8;
+  state_9 = init_10_arg_1;
+  SORT_4 init_18_arg_1 = var_8;
+  state_17 = init_18_arg_1;
+  SORT_1 init_44_arg_1 = var_42;
+  state_43 = init_44_arg_1;
+  for (;;) {
+    // Getting external input values ...
+    input_2 = __VERIFIER_nondet_uchar();
+    input_3 = __VERIFIER_nondet_uchar();
+    input_5 = __VERIFIER_nondet_uchar();
+    input_6 = __VERIFIER_nondet_uchar();
+    input_7 = __VERIFIER_nondet_uchar();
+    input_29 = __VERIFIER_nondet_uchar();
+    input_31 = __VERIFIER_nondet_uchar();
+    input_33 = __VERIFIER_nondet_uchar();
+    input_35 = __VERIFIER_nondet_uchar();
+    input_37 = __VERIFIER_nondet_uchar();
+    input_39 = __VERIFIER_nondet_uchar();
+    // Assuming invariants ...
+    // Asserting properties ...
+    SORT_4 var_11_arg_0 = state_9;
+    SORT_1 var_11 = var_11_arg_0 >> 7;
+    SORT_1 var_13_arg_0 = var_11;
+    var_13_arg_0 = var_13_arg_0 & mask_SORT_1;
+    SORT_12 var_13 = var_13_arg_0;
+    SORT_12 var_15_arg_0 = var_13;
+    SORT_12 var_15_arg_1 = var_14;
+    SORT_1 var_15 = var_15_arg_0 == var_15_arg_1;
+    SORT_1 var_16_arg_0 = var_15;
+    SORT_1 var_16 = ~var_16_arg_0;
+    SORT_4 var_19_arg_0 = state_17;
+    SORT_1 var_19 = var_19_arg_0 >> 7;
+    SORT_1 var_20_arg_0 = var_19;
+    var_20_arg_0 = var_20_arg_0 & mask_SORT_1;
+    SORT_12 var_20 = var_20_arg_0;
+    SORT_12 var_21_arg_0 = var_20;
+    SORT_12 var_21_arg_1 = var_14;
+    SORT_1 var_21 = var_21_arg_0 == var_21_arg_1;
+    SORT_1 var_22_arg_0 = var_16;
+    SORT_1 var_22_arg_1 = var_21;
+    SORT_1 var_22 = var_22_arg_0 | var_22_arg_1;
+    SORT_1 var_26_arg_0 = var_22;
+    SORT_1 var_26 = ~var_26_arg_0;
+    SORT_1 var_27_arg_0 = var_25;
+    SORT_1 var_27_arg_1 = var_26;
+    SORT_1 var_27 = var_27_arg_0 & var_27_arg_1;
+    var_27 = var_27 & mask_SORT_1;
+    SORT_1 bad_28_arg_0 = var_27;
+    __VERIFIER_assert(!(bad_28_arg_0));
+    // Computing next states ...
+    SORT_1 var_45_arg_0 = state_43;
+    SORT_4 var_45_arg_1 = input_5;
+    SORT_4 var_45_arg_2 = state_9;
+    SORT_4 var_45 = var_45_arg_0 ? var_45_arg_1 : var_45_arg_2;
+    SORT_4 next_46_arg_1 = var_45;
+    SORT_1 var_47_arg_0 = state_43;
+    SORT_4 var_47_arg_1 = input_5;
+    SORT_4 var_47_arg_2 = state_17;
+    SORT_4 var_47 = var_47_arg_0 ? var_47_arg_1 : var_47_arg_2;
+    SORT_4 next_48_arg_1 = var_47;
+    SORT_1 var_49_arg_0 = state_43;
+    SORT_1 var_49_arg_1 = var_42;
+    SORT_1 var_49_arg_2 = var_25;
+    SORT_1 var_49 = var_49_arg_0 ? var_49_arg_1 : var_49_arg_2;
+    var_49 = var_49 & mask_SORT_1;
+    SORT_1 next_50_arg_1 = var_49;
+    // Assigning next states ...
+    state_9 = next_46_arg_1;
+    state_17 = next_48_arg_1;
+    state_43 = next_50_arg_1;
+  }
+  return 0;
+}
+
+// REQUIRES: bitwuzla
+// REQUIRES: target-x86_64
+// RUN: %kleef --property-file=%S/coverage-branches.prp --max-memory=7000000000 --max-cputime-soft=300 --64 --debug %s 2>&1 | FileCheck %s
diff --git a/tools/klee/main.cpp b/tools/klee/main.cpp
index c3f2101bf4..68dafcd323 100644
--- a/tools/klee/main.cpp
+++ b/tools/klee/main.cpp
@@ -2059,8 +2059,8 @@ int main(int argc, char **argv, char **envp) {
     for (const auto &Func : *mainModule) {
       for (const auto &instr : llvm::instructions(Func)) {
         auto locationInfo = getLocationInfo(&instr);
-        origInstructions[locationInfo.file][locationInfo.line]
-                        [locationInfo.column.value_or(0)]
+        origInstructions[locationInfo->file][locationInfo->line]
+                        [locationInfo->column.value_or(0)]
                             .insert(instr.getOpcode());
       }
     }
@@ -2077,7 +2077,7 @@ int main(int argc, char **argv, char **envp) {
       for (const auto &loc : path.locations) {
         std::vector<llvm::Function *> funcs;
         for (auto &f : *mainModule) {
-          if (loc->isInside(&f, origInstructions[getLocationInfo(&f).file])) {
+          if (loc->isInside(&f, origInstructions[getLocationInfo(&f)->file])) {
             funcs.push_back(&f);
           }
         }