diff --git a/include/klee/ADT/ImmutableList.h b/include/klee/ADT/ImmutableList.h
new file mode 100644
index 0000000000..20cb225fd8
--- /dev/null
+++ b/include/klee/ADT/ImmutableList.h
@@ -0,0 +1,106 @@
+//===---- ImmutableList.h ---------------------------------------*- C++ -*-===//
+//
+//                     The KLEE Symbolic Virtual Machine
+//
+// This file is distributed under the University of Illinois Open Source
+// License. See LICENSE.TXT for details.
+//
+//===----------------------------------------------------------------------===//
+
+#ifndef KLEE_IMMUTABLELIST_H
+#define KLEE_IMMUTABLELIST_H
+
+#include <memory>
+#include <vector>
+
+namespace klee {
+
+template <typename T> class ImmutableList {
+  struct ImmutableListNode {
+    std::shared_ptr<ImmutableListNode> prev;
+    const size_t prev_len;
+    std::vector<T> values;
+
+    [[nodiscard]] size_t size() const { return prev_len + values.size(); }
+
+    ImmutableListNode() : prev(nullptr), prev_len(0), values() {}
+
+    explicit ImmutableListNode(const ImmutableList<T> &il)
+        : prev_len(il.size()), values() {
+      std::shared_ptr<ImmutableListNode> pr = il.node;
+      while (pr && pr->values.empty()) {
+        pr = pr->prev;
+      }
+      if (pr && pr->size()) {
+        prev = pr;
+      } else {
+        prev = nullptr;
+      }
+    }
+  };
+
+  std::shared_ptr<ImmutableListNode> node;
+
+public:
+  [[nodiscard]] size_t size() const { return node ? node->size() : 0; }
+
+  struct iterator {
+    const ImmutableListNode *rootNode;
+    std::unique_ptr<iterator> it;
+    size_t get;
+
+  public:
+    explicit iterator(const ImmutableListNode *p)
+        : rootNode(p), it(nullptr), get(0) {
+      if (rootNode && rootNode->prev.get()) {
+        it = std::make_unique<iterator>(rootNode->prev.get());
+      }
+    }
+
+    bool operator==(const iterator &b) const {
+      return rootNode == b.rootNode && get == b.get;
+    }
+
+    bool operator!=(const iterator &b) const { return !(*this == b); }
+
+    iterator &operator++() {
+      ++get;
+      if (get < rootNode->prev_len) {
+        it->operator++();
+      }
+      return *this;
+    }
+
+    const T &operator*() const {
+      if (get < rootNode->prev_len) {
+        return **it;
+      }
+      return rootNode->values[get - rootNode->prev_len];
+    }
+
+    const T &operator->() const { return **this; }
+  };
+
+  [[nodiscard]] iterator begin() const { return iterator(node.get()); }
+
+  [[nodiscard]] iterator end() const {
+    auto it = iterator(node.get());
+    it.get = size();
+    return it;
+  }
+
+  void push_back(T &&value) {
+    if (!node) {
+      node = std::make_shared<ImmutableListNode>();
+    }
+    node->values.push_back(std::move(value));
+  }
+
+  ImmutableList() : node(){};
+  ImmutableList(const ImmutableList<T> &il)
+      : node(std::make_shared<ImmutableListNode>(il)) {}
+};
+
+} // namespace klee
+
+#endif /* KLEE_IMMUTABLELIST_H */
diff --git a/include/klee/Core/Interpreter.h b/include/klee/Core/Interpreter.h
index 6c7ff2f878..766380b486 100644
--- a/include/klee/Core/Interpreter.h
+++ b/include/klee/Core/Interpreter.h
@@ -41,7 +41,6 @@ class ExecutionState;
 struct SarifReport;
 class Interpreter;
 class TreeStreamWriter;
-class InstructionInfoTable;
 
 class InterpreterHandler {
 public:
@@ -61,6 +60,12 @@ class InterpreterHandler {
                                const char *suffix, bool isError = false) = 0;
 };
 
+/// [File][Line][Column] -> Opcode
+using FLCtoOpcode = std::unordered_map<
+    std::string,
+    std::unordered_map<
+        unsigned, std::unordered_map<unsigned, std::unordered_set<unsigned>>>>;
+
 class Interpreter {
 public:
   enum class GuidanceKind {
@@ -140,9 +145,9 @@ class Interpreter {
   setModule(std::vector<std::unique_ptr<llvm::Module>> &userModules,
             std::vector<std::unique_ptr<llvm::Module>> &libsModules,
             const ModuleOptions &opts,
-            const std::unordered_set<std::string> &mainModuleFunctions,
-            const std::unordered_set<std::string> &mainModuleGlobals,
-            std::unique_ptr<InstructionInfoTable> origInfos) = 0;
+            std::set<std::string> &&mainModuleFunctions,
+            std::set<std::string> &&mainModuleGlobals,
+            FLCtoOpcode &&origInstructions) = 0;
 
   // supply a tree stream writer which the interpreter will use
   // to record the concrete path (as a stream of '0' and '1' bytes).
@@ -194,7 +199,7 @@ class Interpreter {
 
   virtual void
   getCoveredLines(const ExecutionState &state,
-                  std::map<const std::string *, std::set<unsigned>> &res) = 0;
+                  std::map<std::string, std::set<unsigned>> &res) = 0;
 
   virtual void getBlockPath(const ExecutionState &state,
                             std::string &blockPath) = 0;
diff --git a/include/klee/Module/InstructionInfoTable.h b/include/klee/Module/InstructionInfoTable.h
deleted file mode 100644
index 8b91c0d8c8..0000000000
--- a/include/klee/Module/InstructionInfoTable.h
+++ /dev/null
@@ -1,113 +0,0 @@
-//===-- InstructionInfoTable.h ----------------------------------*- C++ -*-===//
-//
-//                     The KLEE Symbolic Virtual Machine
-//
-// This file is distributed under the University of Illinois Open Source
-// License. See LICENSE.TXT for details.
-//
-//===----------------------------------------------------------------------===//
-
-#ifndef KLEE_INSTRUCTIONINFOTABLE_H
-#define KLEE_INSTRUCTIONINFOTABLE_H
-
-#include "klee/Support/CompilerWarning.h"
-DISABLE_WARNING_PUSH
-DISABLE_WARNING_DEPRECATED_DECLARATIONS
-#include "llvm/ADT/Optional.h"
-#include "llvm/Support/raw_ostream.h"
-DISABLE_WARNING_POP
-
-#include <memory>
-#include <string>
-#include <unordered_map>
-#include <unordered_set>
-#include <vector>
-
-namespace llvm {
-class Function;
-class Instruction;
-class Module;
-} // namespace llvm
-
-namespace klee {
-
-/// @brief InstructionInfo stores debug information for a KInstruction.
-struct InstructionInfo {
-  /// @brief The instruction id.
-  unsigned id;
-  /// @brief Line number in source file.
-  unsigned line;
-  /// @brief Column number in source file.
-  unsigned column;
-  /// @brief Line number in generated assembly.ll.
-  llvm::Optional<uint64_t> assemblyLine;
-  /// @brief Source file name.
-  const std::string &file;
-
-public:
-  InstructionInfo(unsigned id, const std::string &file, unsigned line,
-                  unsigned column, llvm::Optional<uint64_t> assemblyLine)
-      : id{id}, line{line}, column{column},
-        assemblyLine{assemblyLine}, file{file} {}
-};
-
-/// @brief FunctionInfo stores debug information for a KFunction.
-struct FunctionInfo {
-  /// @brief The function id.
-  unsigned id;
-  /// @brief Line number in source file.
-  unsigned line;
-  /// @brief Line number in generated assembly.ll.
-  llvm::Optional<uint64_t> assemblyLine;
-  /// @brief Source file name.
-  const std::string &file;
-
-public:
-  FunctionInfo(unsigned id, const std::string &file, unsigned line,
-               llvm::Optional<uint64_t> assemblyLine)
-      : id{id}, line{line}, assemblyLine{assemblyLine}, file{file} {}
-
-  FunctionInfo(const FunctionInfo &) = delete;
-  FunctionInfo &operator=(FunctionInfo const &) = delete;
-
-  FunctionInfo(FunctionInfo &&) = default;
-};
-
-class InstructionInfoTable {
-public:
-  using Instructions = std::unordered_map<
-      std::string,
-      std::unordered_map<
-          unsigned int,
-          std::unordered_map<unsigned int, std::unordered_set<unsigned int>>>>;
-  using LocationToFunctionsMap =
-      std::unordered_map<std::string,
-                         std::unordered_set<const llvm::Function *>>;
-
-private:
-  std::unordered_map<const llvm::Instruction *,
-                     std::unique_ptr<InstructionInfo>>
-      infos;
-  std::unordered_map<const llvm::Function *, std::unique_ptr<FunctionInfo>>
-      functionInfos;
-  LocationToFunctionsMap fileNameToFunctions;
-  std::vector<std::unique_ptr<std::string>> internedStrings;
-  std::unordered_set<std::string> filesNames;
-  Instructions insts;
-
-public:
-  explicit InstructionInfoTable(
-      const llvm::Module &m, std::unique_ptr<llvm::raw_fd_ostream> assemblyFS,
-      bool withInstructions = false);
-
-  unsigned getMaxID() const;
-  const InstructionInfo &getInfo(const llvm::Instruction &) const;
-  const FunctionInfo &getFunctionInfo(const llvm::Function &) const;
-  const LocationToFunctionsMap &getFileNameToFunctions() const;
-  const std::unordered_set<std::string> &getFilesNames() const;
-  Instructions getInstructions();
-};
-
-} // namespace klee
-
-#endif /* KLEE_INSTRUCTIONINFOTABLE_H */
diff --git a/include/klee/Module/KInstruction.h b/include/klee/Module/KInstruction.h
index 865a752bfd..5c64de152c 100644
--- a/include/klee/Module/KInstruction.h
+++ b/include/klee/Module/KInstruction.h
@@ -10,16 +10,17 @@
 #ifndef KLEE_KINSTRUCTION_H
 #define KLEE_KINSTRUCTION_H
 
+#include "KModule.h"
 #include "klee/Config/Version.h"
-#include "klee/Module/InstructionInfoTable.h"
-
 #include "klee/Support/CompilerWarning.h"
+
 DISABLE_WARNING_PUSH
 DISABLE_WARNING_DEPRECATED_DECLARATIONS
 #include "llvm/Support/DataTypes.h"
 #include "llvm/Support/raw_ostream.h"
 DISABLE_WARNING_POP
 
+#include <unordered_map>
 #include <vector>
 
 namespace llvm {
@@ -28,7 +29,6 @@ class Instruction;
 
 namespace klee {
 class Executor;
-struct InstructionInfo;
 class KModule;
 struct KBlock;
 
@@ -36,26 +36,50 @@ struct KBlock;
 /// during execution.
 struct KInstruction {
   llvm::Instruction *inst;
-  const InstructionInfo *info;
 
   /// Value numbers for each operand. -1 is an invalid value,
   /// otherwise negative numbers are indices (negated and offset by
   /// 2) into the module constant table and positive numbers are
   /// register indices.
   int *operands;
-  /// Destination register index.
-  unsigned dest;
   KBlock *parent;
 
+private:
   // Instruction index in the basic block
-  unsigned index;
+  const unsigned globalIndex;
 
 public:
-  KInstruction() = default;
-  explicit KInstruction(const KInstruction &ki);
+  /// Unique index for KFunction and KInstruction inside KModule
+  /// from 0 to [KFunction + KInstruction]
+  [[nodiscard]] unsigned getGlobalIndex() const;
+  /// Instruction index in the basic block
+  [[nodiscard]] unsigned getIndex() const;
+  /// Destination register index.
+  [[nodiscard]] unsigned getDest() const;
+
+  KInstruction(const std::unordered_map<llvm::Instruction *, unsigned>
+                   &_instructionToRegisterMap,
+               llvm::Instruction *_inst, KModule *_km, KBlock *_kb,
+               unsigned &_globalIndexInc);
+
+  KInstruction() = delete;
+  explicit KInstruction(const KInstruction &ki) = delete;
   virtual ~KInstruction();
-  std::string getSourceLocation() const;
-  std::string toString() const;
+
+  [[nodiscard]] size_t getLine() const;
+  [[nodiscard]] size_t getColumn() const;
+  [[nodiscard]] std::string getSourceFilepath() const;
+
+  [[nodiscard]] std::string getSourceLocationString() const;
+  [[nodiscard]] std::string toString() const;
+
+  [[nodiscard]] inline KBlock *getKBlock() const { return parent; }
+  [[nodiscard]] inline KFunction *getKFunction() const {
+    return getKBlock()->parent;
+  }
+  [[nodiscard]] inline KModule *getKModule() const {
+    return getKFunction()->parent;
+  }
 };
 
 struct KGEPInstruction : KInstruction {
@@ -70,8 +94,14 @@ struct KGEPInstruction : KInstruction {
   uint64_t offset;
 
 public:
-  KGEPInstruction() = default;
-  explicit KGEPInstruction(const KGEPInstruction &ki);
+  KGEPInstruction(const std::unordered_map<llvm::Instruction *, unsigned>
+                      &_instructionToRegisterMap,
+                  llvm::Instruction *_inst, KModule *_km, KBlock *_kb,
+                  unsigned &_globalIndexInc)
+      : KInstruction(_instructionToRegisterMap, _inst, _km, _kb,
+                     _globalIndexInc) {}
+  KGEPInstruction() = delete;
+  explicit KGEPInstruction(const KGEPInstruction &ki) = delete;
 };
 } // namespace klee
 
diff --git a/include/klee/Module/KModule.h b/include/klee/Module/KModule.h
index e601d91e43..4965f78b27 100644
--- a/include/klee/Module/KModule.h
+++ b/include/klee/Module/KModule.h
@@ -12,7 +12,6 @@
 
 #include "klee/Config/Version.h"
 #include "klee/Core/Interpreter.h"
-#include "klee/Module/InstructionInfoTable.h"
 #include "klee/Module/KCallable.h"
 
 #include "klee/Support/CompilerWarning.h"
@@ -65,16 +64,11 @@ struct KBlock {
   unsigned numInstructions;
   KInstruction **instructions;
 
-  /// Whether instructions in this function should count as
-  /// "coverable" for statistics and search heuristics.
-  bool trackCoverage;
-
-  unsigned id;
-
 public:
   KBlock(KFunction *, llvm::BasicBlock *, KModule *,
-         std::unordered_map<llvm::Instruction *, unsigned> &,
-         std::unordered_map<unsigned, KInstruction *> &, KInstruction **);
+         const std::unordered_map<llvm::Instruction *, unsigned> &,
+         KInstruction **, unsigned &globalIndexInc);
+  KBlock() = delete;
   KBlock(const KBlock &) = delete;
   KBlock &operator=(const KBlock &) = delete;
   virtual ~KBlock() = default;
@@ -82,16 +76,15 @@ struct KBlock {
   virtual KBlockType getKBlockType() const { return KBlockType::Base; }
   static bool classof(const KBlock *) { return true; }
 
-  void handleKInstruction(std::unordered_map<llvm::Instruction *, unsigned>
-                              &instructionToRegisterMap,
-                          llvm::Instruction *inst, KModule *km,
-                          KInstruction *ki);
   KInstruction *getFirstInstruction() const noexcept { return instructions[0]; }
   KInstruction *getLastInstruction() const noexcept {
     return instructions[numInstructions - 1];
   }
   std::string getLabel() const;
   std::string toString() const;
+
+  /// Block number in function
+  [[nodiscard]] uintptr_t getId() const;
 };
 
 typedef std::function<bool(KBlock *)> KBlockPredicate;
@@ -101,10 +94,11 @@ struct KCallBlock : KBlock {
   std::set<llvm::Function *> calledFunctions;
 
 public:
+  KCallBlock() = delete;
   KCallBlock(KFunction *, llvm::BasicBlock *, KModule *,
-             std::unordered_map<llvm::Instruction *, unsigned> &,
-             std::unordered_map<unsigned, KInstruction *> &,
-             std::set<llvm::Function *>, KInstruction **);
+             const std::unordered_map<llvm::Instruction *, unsigned> &,
+             std::set<llvm::Function *>, KInstruction **,
+             unsigned &globalIndexInc);
   static bool classof(const KCallBlock *) { return true; }
   static bool classof(const KBlock *E) {
     return E->getKBlockType() == KBlockType::Call;
@@ -118,9 +112,10 @@ struct KCallBlock : KBlock {
 
 struct KReturnBlock : KBlock {
 public:
+  KReturnBlock() = delete;
   KReturnBlock(KFunction *, llvm::BasicBlock *, KModule *,
-               std::unordered_map<llvm::Instruction *, unsigned> &,
-               std::unordered_map<unsigned, KInstruction *> &, KInstruction **);
+               const std::unordered_map<llvm::Instruction *, unsigned> &,
+               KInstruction **, unsigned &globalIndexInc);
   static bool classof(const KReturnBlock *) { return true; }
   static bool classof(const KBlock *E) {
     return E->getKBlockType() == KBlockType::Return;
@@ -131,20 +126,14 @@ struct KReturnBlock : KBlock {
 struct KFunction : public KCallable {
 private:
   std::unordered_map<std::string, KBlock *> labelMap;
+  const unsigned globalIndex;
 
 public:
   KModule *parent;
   llvm::Function *function;
-
-  unsigned numArgs, numRegisters;
-  unsigned id;
-
-  std::unordered_map<unsigned, KInstruction *> registerToInstructionMap;
-  unsigned numInstructions;
-  unsigned numBlocks;
   KInstruction **instructions;
 
-  bool kleeHandled = false;
+  [[nodiscard]] KInstruction *getInstructionByRegister(size_t reg) const;
 
   std::unordered_map<const llvm::Instruction *, KInstruction *> instructionMap;
   std::vector<std::unique_ptr<KBlock>> blocks;
@@ -153,11 +142,16 @@ struct KFunction : public KCallable {
   std::vector<KBlock *> returnKBlocks;
   std::vector<KCallBlock *> kCallBlocks;
 
-  /// Whether instructions in this function should count as
-  /// "coverable" for statistics and search heuristics.
-  bool trackCoverage;
+  /// count of instructions in function
+  unsigned numInstructions;
+  [[nodiscard]] size_t getNumArgs() const;
+  [[nodiscard]] size_t getNumRegisters() const;
+  unsigned id;
+
+  bool kleeHandled = false;
 
-  explicit KFunction(llvm::Function *, KModule *);
+  explicit KFunction(llvm::Function *, KModule *, unsigned &);
+  KFunction() = delete;
   KFunction(const KFunction &) = delete;
   KFunction &operator=(const KFunction &) = delete;
 
@@ -187,12 +181,20 @@ struct KFunction : public KCallable {
   static bool classof(const KCallable *callable) {
     return callable->getKind() == CK_Function;
   }
+
+  [[nodiscard]] size_t getLine() const;
+  [[nodiscard]] std::string getSourceFilepath() const;
+
+  /// Unique index for KFunction and KInstruction inside KModule
+  /// from 0 to [KFunction + KInstruction]
+  [[nodiscard]] inline unsigned getGlobalIndex() const { return globalIndex; }
 };
 
 struct KBlockCompare {
   bool operator()(const KBlock *a, const KBlock *b) const {
-    return a->parent->id < b->parent->id ||
-           (a->parent->id == b->parent->id && a->id < b->id);
+    return a->parent->getGlobalIndex() < b->parent->getGlobalIndex() ||
+           (a->parent->getGlobalIndex() == b->parent->getGlobalIndex() &&
+            a->getId() < b->getId());
   }
 };
 
@@ -213,7 +215,8 @@ class KConstant {
 
 class KModule {
 private:
-  bool withPosixRuntime;
+  bool withPosixRuntime; // TODO move to opts
+  unsigned maxGlobalIndex;
 
 public:
   std::unique_ptr<llvm::Module> module;
@@ -224,19 +227,16 @@ class KModule {
   std::unordered_map<const llvm::Function *, KFunction *> functionMap;
   std::unordered_map<llvm::Function *, std::set<llvm::Function *>> callMap;
   std::unordered_map<std::string, KFunction *> functionNameMap;
-  std::unordered_map<const llvm::Function *, unsigned> functionIDMap;
+  [[nodiscard]] unsigned getFunctionId(const llvm::Function *) const;
 
   // Functions which escape (may be called indirectly)
   // XXX change to KFunction
   std::set<llvm::Function *> escapingFunctions;
 
-  std::unordered_set<std::string> mainModuleFunctions;
+  std::set<std::string> mainModuleFunctions;
+  std::set<std::string> mainModuleGlobals;
 
-  std::unordered_set<std::string> mainModuleGlobals;
-
-  InstructionInfoTable::Instructions origInfos;
-
-  std::unique_ptr<InstructionInfoTable> infos;
+  FLCtoOpcode origInstructions;
 
   std::vector<llvm::Constant *> constants;
   std::unordered_map<const llvm::Constant *, std::unique_ptr<KConstant>>
@@ -248,6 +248,9 @@ class KModule {
   // Functions which are part of KLEE runtime
   std::set<const llvm::Function *> internalFunctions;
 
+  // instruction to assembly.ll line empty if no statistic enabled
+  std::unordered_map<uintptr_t, uint64_t> asmLineMap;
+
   // Mark function with functionName as part of the KLEE runtime
   void addInternalFunction(const char *functionName);
   // Replace std functions with KLEE intrinsics
@@ -301,6 +304,14 @@ class KModule {
   bool inMainModule(const llvm::GlobalVariable &v);
 
   bool WithPOSIXRuntime() { return withPosixRuntime; }
+
+  std::optional<size_t> getAsmLine(const uintptr_t ref) const;
+  std::optional<size_t> getAsmLine(const llvm::Function *func) const;
+  std::optional<size_t> getAsmLine(const llvm::Instruction *inst) const;
+
+  inline unsigned getMaxGlobalIndex() const { return maxGlobalIndex; }
+  unsigned getGlobalIndex(const llvm::Function *func) const;
+  unsigned getGlobalIndex(const llvm::Instruction *inst) const;
 };
 } // namespace klee
 
diff --git a/include/klee/Module/LocationInfo.h b/include/klee/Module/LocationInfo.h
new file mode 100644
index 0000000000..36ac6bec4d
--- /dev/null
+++ b/include/klee/Module/LocationInfo.h
@@ -0,0 +1,35 @@
+////===-- LocationInfo.h ----------------------------------*- C++ -*-===//
+////
+////                     The KLEE Symbolic Virtual Machine
+////
+//// This file is distributed under the University of Illinois Open Source
+//// License. See LICENSE.TXT for details.
+////
+////===----------------------------------------------------------------------===//
+
+#ifndef KLEE_LOCATIONINFO_H
+#define KLEE_LOCATIONINFO_H
+
+#include <memory>
+#include <string>
+
+namespace llvm {
+class Function;
+class Instruction;
+class Module;
+} // namespace llvm
+
+namespace klee {
+
+struct LocationInfo {
+  std::string file;
+  size_t line;
+  size_t column;
+};
+
+LocationInfo getLocationInfo(const llvm::Function *func);
+LocationInfo getLocationInfo(const llvm::Instruction *inst);
+
+} // namespace klee
+
+#endif /* KLEE_LOCATIONINFO_H */
diff --git a/include/klee/Support/ErrorHandling.h b/include/klee/Support/ErrorHandling.h
index 4cc57c9744..098293d2e5 100644
--- a/include/klee/Support/ErrorHandling.h
+++ b/include/klee/Support/ErrorHandling.h
@@ -16,7 +16,7 @@
 #endif
 #endif
 
-#include <stdio.h>
+#include <cstdio>
 
 namespace klee {
 
diff --git a/lib/Basic/Statistics.cpp b/lib/Basic/Statistics.cpp
index 170ea839e0..50d9e8bf1f 100644
--- a/lib/Basic/Statistics.cpp
+++ b/lib/Basic/Statistics.cpp
@@ -50,7 +50,7 @@ Statistic *StatisticManager::getStatisticByName(const std::string &name) const {
   return 0;
 }
 
-StatisticManager *klee::theStatisticManager = 0;
+StatisticManager *klee::theStatisticManager = nullptr;
 
 static StatisticManager &getStatisticManager() {
   static StatisticManager sm;
diff --git a/lib/Core/DistanceCalculator.cpp b/lib/Core/DistanceCalculator.cpp
index ebfdb7eec6..24d1d47898 100644
--- a/lib/Core/DistanceCalculator.cpp
+++ b/lib/Core/DistanceCalculator.cpp
@@ -95,8 +95,6 @@ DistanceResult DistanceCalculator::computeDistance(KBlock *kb, TargetKind kind,
 DistanceResult DistanceCalculator::getDistance(
     const KInstruction *prevPC, const KInstruction *pc,
     const ExecutionStack::call_stack_ty &frames, KBlock *target) {
-  weight_type weight = 0;
-
   KBlock *kb = pc->parent;
   const auto &distanceToTargetFunction =
       codeGraphInfo.getBackwardDistance(target->parent);
@@ -196,7 +194,6 @@ WeightResult
 DistanceCalculator::tryGetLocalWeight(KBlock *kb, weight_type &weight,
                                       const std::vector<KBlock *> &localTargets,
                                       KBlock *target) const {
-  KFunction *currentKF = kb->parent;
   KBlock *currentKB = kb;
   const std::unordered_map<KBlock *, unsigned> &dist =
       codeGraphInfo.getDistance(currentKB);
diff --git a/lib/Core/ExecutionState.cpp b/lib/Core/ExecutionState.cpp
index 5ee6b7c8da..05142dd2c4 100644
--- a/lib/Core/ExecutionState.cpp
+++ b/lib/Core/ExecutionState.cpp
@@ -14,7 +14,6 @@
 #include "klee/Expr/ArrayExprVisitor.h"
 #include "klee/Expr/Expr.h"
 #include "klee/Module/Cell.h"
-#include "klee/Module/InstructionInfoTable.h"
 #include "klee/Module/KInstruction.h"
 #include "klee/Module/KModule.h"
 #include "klee/Support/Casting.h"
@@ -101,14 +100,14 @@ bool CallStackFrame::equals(const CallStackFrame &other) const {
   return kf == other.kf && caller == other.caller;
 }
 
-StackFrame::StackFrame(KFunction *kf) : kf(kf), varargs(0) {
-  locals = new Cell[kf->numRegisters];
+StackFrame::StackFrame(KFunction *kf) : kf(kf), varargs(nullptr) {
+  locals = new Cell[kf->getNumRegisters()];
 }
 
 StackFrame::StackFrame(const StackFrame &s)
     : kf(s.kf), allocas(s.allocas), varargs(s.varargs) {
-  locals = new Cell[kf->numRegisters];
-  for (unsigned i = 0; i < kf->numRegisters; i++)
+  locals = new Cell[kf->getNumRegisters()];
+  for (unsigned i = 0; i < kf->getNumRegisters(); i++)
     locals[i] = s.locals[i];
 }
 
@@ -119,7 +118,7 @@ InfoStackFrame::InfoStackFrame(KFunction *kf) : kf(kf) {}
 /***/
 ExecutionState::ExecutionState()
     : initPC(nullptr), pc(nullptr), prevPC(nullptr), incomingBBIndex(-1),
-      depth(0), ptreeNode(nullptr), steppedInstructions(0),
+      depth(0), ptreeNode(nullptr), symbolics(), steppedInstructions(0),
       steppedMemoryInstructions(0), instsSinceCovNew(0),
       roundingMode(llvm::APFloat::rmNearestTiesToEven),
       coveredNew(new box<bool>(false)), forkDisabled(false),
@@ -130,7 +129,7 @@ ExecutionState::ExecutionState()
 
 ExecutionState::ExecutionState(KFunction *kf)
     : initPC(kf->instructions), pc(initPC), prevPC(pc), incomingBBIndex(-1),
-      depth(0), ptreeNode(nullptr), steppedInstructions(0),
+      depth(0), ptreeNode(nullptr), symbolics(), steppedInstructions(0),
       steppedMemoryInstructions(0), instsSinceCovNew(0),
       roundingMode(llvm::APFloat::rmNearestTiesToEven),
       coveredNew(new box<bool>(false)), forkDisabled(false),
@@ -142,7 +141,7 @@ ExecutionState::ExecutionState(KFunction *kf)
 
 ExecutionState::ExecutionState(KFunction *kf, KBlock *kb)
     : initPC(kb->instructions), pc(initPC), prevPC(pc), incomingBBIndex(-1),
-      depth(0), ptreeNode(nullptr), steppedInstructions(0),
+      depth(0), ptreeNode(nullptr), symbolics(), steppedInstructions(0),
       steppedMemoryInstructions(0), instsSinceCovNew(0),
       roundingMode(llvm::APFloat::rmNearestTiesToEven),
       coveredNew(new box<bool>(false)), forkDisabled(false),
@@ -193,8 +192,8 @@ ExecutionState *ExecutionState::branch() {
 }
 
 bool ExecutionState::inSymbolics(const MemoryObject *mo) const {
-  for (auto i : symbolics) {
-    if (mo->id == i.memoryObject->id) {
+  for (const auto &symbolic : symbolics) {
+    if (mo->id == symbolic.memoryObject->id) {
       return true;
     }
   }
@@ -254,13 +253,12 @@ void ExecutionState::popFrame() {
 
 void ExecutionState::addSymbolic(const MemoryObject *mo, const Array *array,
                                  KType *type) {
-  symbolics.emplace_back(ref<const MemoryObject>(mo), array, type);
+  symbolics.push_back({mo, array, type});
 }
 
 ref<const MemoryObject>
 ExecutionState::findMemoryObject(const Array *array) const {
-  for (unsigned i = 0; i != symbolics.size(); ++i) {
-    const auto &symbolic = symbolics[i];
+  for (const auto &symbolic : symbolics) {
     if (array == symbolic.array) {
       return symbolic.memoryObject;
     }
@@ -387,13 +385,12 @@ void ExecutionState::dumpStack(llvm::raw_ostream &out) const {
     const StackFrame &sf = stack.valueStack().at(ri);
 
     Function *f = csf.kf->function;
-    const InstructionInfo &ii = *target->info;
     out << "\t#" << i;
-    if (ii.assemblyLine.hasValue()) {
-      std::stringstream AssStream;
-      AssStream << std::setw(8) << std::setfill('0')
-                << ii.assemblyLine.getValue();
-      out << AssStream.str();
+    auto assemblyLine = target->getKModule()->getAsmLine(target->inst);
+    if (assemblyLine.has_value()) {
+      std::stringstream AsmStream;
+      AsmStream << std::setw(8) << std::setfill('0') << assemblyLine.value();
+      out << AsmStream.str();
     }
     out << " in " << f->getName().str() << "(";
     // Yawn, we could go up and print varargs if we wanted to.
@@ -414,8 +411,9 @@ void ExecutionState::dumpStack(llvm::raw_ostream &out) const {
       }
     }
     out << ")";
-    if (ii.file != "")
-      out << " at " << ii.file << ":" << ii.line;
+    std::string filepath = target->getSourceFilepath();
+    if (!filepath.empty())
+      out << " at " << filepath << ":" << target->getLine();
     out << "\n";
     target = csf.caller;
   }
diff --git a/lib/Core/ExecutionState.h b/lib/Core/ExecutionState.h
index 424dfc4248..a0aa46619a 100644
--- a/lib/Core/ExecutionState.h
+++ b/lib/Core/ExecutionState.h
@@ -12,6 +12,7 @@
 
 #include "AddressSpace.h"
 
+#include "klee/ADT/ImmutableList.h"
 #include "klee/ADT/ImmutableSet.h"
 #include "klee/ADT/PersistentMap.h"
 #include "klee/ADT/PersistentSet.h"
@@ -53,9 +54,7 @@ struct KBlock;
 struct KInstruction;
 class MemoryObject;
 class PTreeNode;
-struct InstructionInfo;
 class Target;
-struct TranstionHash;
 
 llvm::raw_ostream &operator<<(llvm::raw_ostream &os, const MemoryMap &mm);
 
@@ -216,7 +215,8 @@ struct Symbolic {
   const Array *array;
   KType *type;
   Symbolic(ref<const MemoryObject> mo, const Array *a, KType *t)
-      : memoryObject(mo), array(a), type(t) {}
+      : memoryObject(std::move(mo)), array(a), type(t) {}
+  Symbolic(const Symbolic &other) = default;
   Symbolic &operator=(const Symbolic &other) = default;
 
   friend bool operator==(const Symbolic &lhs, const Symbolic &rhs) {
@@ -317,16 +317,14 @@ class ExecutionState {
   TreeOStream symPathOS;
 
   /// @brief Set containing which lines in which files are covered by this state
-  std::map<const std::string *, std::set<std::uint32_t>> coveredLines;
+  std::map<std::string, std::set<unsigned>> coveredLines;
 
   /// @brief Pointer to the process tree of the current state
   /// Copies of ExecutionState should not copy ptreeNode
   PTreeNode *ptreeNode = nullptr;
 
   /// @brief Ordered list of symbolics: used to generate test cases.
-  //
-  // FIXME: Move to a shared list structure (not critical).
-  std::vector<Symbolic> symbolics;
+  ImmutableList<Symbolic> symbolics;
 
   /// @brief map from memory accesses to accessed objects and access offsets.
   ExprHashMap<std::set<IDType>> resolvedPointers;
diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp
index 1d0c887e06..c58e1a51ac 100644
--- a/lib/Core/Executor.cpp
+++ b/lib/Core/Executor.cpp
@@ -51,7 +51,6 @@
 #include "klee/Expr/Symcrete.h"
 #include "klee/Module/Cell.h"
 #include "klee/Module/CodeGraphInfo.h"
-#include "klee/Module/InstructionInfoTable.h"
 #include "klee/Module/KCallable.h"
 #include "klee/Module/KInstruction.h"
 #include "klee/Module/KModule.h"
@@ -536,13 +535,11 @@ Executor::Executor(LLVMContext &ctx, const InterpreterOptions &opts,
   }
 }
 
-llvm::Module *
-Executor::setModule(std::vector<std::unique_ptr<llvm::Module>> &userModules,
-                    std::vector<std::unique_ptr<llvm::Module>> &libsModules,
-                    const ModuleOptions &opts,
-                    const std::unordered_set<std::string> &mainModuleFunctions,
-                    const std::unordered_set<std::string> &mainModuleGlobals,
-                    std::unique_ptr<InstructionInfoTable> origInfos) {
+llvm::Module *Executor::setModule(
+    std::vector<std::unique_ptr<llvm::Module>> &userModules,
+    std::vector<std::unique_ptr<llvm::Module>> &libsModules,
+    const ModuleOptions &opts, std::set<std::string> &&mainModuleFunctions,
+    std::set<std::string> &&mainModuleGlobals, FLCtoOpcode &&origInstructions) {
   assert(!kmodule && !userModules.empty() &&
          "can only register one module"); // XXX gross
 
@@ -596,16 +593,12 @@ Executor::setModule(std::vector<std::unique_ptr<llvm::Module>> &userModules,
   kmodule->checkModule();
 
   // 4.) Manifest the module
-  kmodule->mainModuleFunctions.insert(mainModuleFunctions.begin(),
-                                      mainModuleFunctions.end());
-  kmodule->mainModuleGlobals.insert(mainModuleGlobals.begin(),
-                                    mainModuleGlobals.end());
+  std::swap(kmodule->mainModuleFunctions, mainModuleFunctions);
+  std::swap(kmodule->mainModuleGlobals, mainModuleGlobals);
   kmodule->manifest(interpreterHandler, interpreterOpts.Guidance,
                     StatsTracker::useStatistics());
 
-  if (origInfos) {
-    kmodule->origInfos = origInfos->getInstructions();
-  }
+  kmodule->origInstructions = origInstructions;
 
   specialFunctionHandler->bind();
 
@@ -750,6 +743,7 @@ void Executor::allocateGlobalObjects(ExecutionState &state) {
                         true, nullptr, 8);
     errnoObj->isFixed = true;
 
+    // TODO: unused variable
     ObjectState *os = bindObjectInState(
         state, errnoObj, typeSystemManager->getWrappedType(pointerErrnoAddr),
         false);
@@ -1108,7 +1102,7 @@ ref<Expr> Executor::maxStaticPctChecks(ExecutionState &current,
     std::string msg("skipping fork and concretizing condition (MaxStatic*Pct "
                     "limit reached) at ");
     llvm::raw_string_ostream os(msg);
-    os << current.prevPC->getSourceLocation();
+    os << current.prevPC->getSourceLocationString();
     klee_warning_once(0, "%s", os.str().c_str());
 
     addConstraint(current, EqExpr::create(value, condition));
@@ -1526,8 +1520,8 @@ ref<klee::ConstantExpr> Executor::toConstant(ExecutionState &state, ref<Expr> e,
   std::string str;
   llvm::raw_string_ostream os(str);
   os << "silently concretizing (reason: " << reason << ") expression " << e
-     << " to value " << value << " (" << (*(state.pc)).info->file << ":"
-     << (*(state.pc)).info->line << ")";
+     << " to value " << value << " (" << state.pc->getSourceFilepath() << ":"
+     << state.pc->getLine() << ")";
 
   if (AllExternalWarnings)
     klee_warning("%s", os.str().c_str());
@@ -1606,10 +1600,13 @@ void Executor::printDebugInstructions(ExecutionState &state) {
   //   [src]     src location:asm line:state ID
   if (!DebugPrintInstructions.isSet(STDERR_COMPACT) &&
       !DebugPrintInstructions.isSet(FILE_COMPACT)) {
-    (*stream) << "     " << state.pc->getSourceLocation() << ':';
+    (*stream) << "     " << state.pc->getSourceLocationString() << ':';
   }
-  if (state.pc->info->assemblyLine.hasValue()) {
-    (*stream) << state.pc->info->assemblyLine.getValue() << ':';
+  {
+    auto asmLine = state.pc->getKModule()->getAsmLine(state.pc->inst);
+    if (asmLine.has_value()) {
+      (*stream) << asmLine.value() << ':';
+    }
   }
   (*stream) << state.getID() << ":";
   (*stream) << "[";
@@ -2574,7 +2571,7 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) {
       // requires that we still be in the context of the branch
       // instruction (it reuses its statistic id). Should be cleaned
       // up with convenient instruction specific data.
-      if (statsTracker && state.stack.callStack().back().kf->trackCoverage)
+      if (statsTracker)
         statsTracker->markBranchVisited(branches.first, branches.second);
 
       if (branches.first)
@@ -4253,9 +4250,9 @@ void Executor::reportProgressTowardsTargets(std::string prefix,
     repr << "in function " +
                 target->getBlock()->parent->function->getName().str();
     repr << " (lines ";
-    repr << target->getBlock()->getFirstInstruction()->info->line;
+    repr << target->getBlock()->getFirstInstruction()->getLine();
     repr << " to ";
-    repr << target->getBlock()->getLastInstruction()->info->line;
+    repr << target->getBlock()->getLastInstruction()->getLine();
     repr << ")";
     std::string targetString = repr.str();
     klee_message("%s for %s", distance.toString().c_str(),
@@ -4620,22 +4617,19 @@ void Executor::terminateStateEarlyUser(ExecutionState &state,
   terminateStateEarly(state, message, StateTerminationType::SilentExit);
 }
 
-const InstructionInfo &
-Executor::getLastNonKleeInternalInstruction(const ExecutionState &state,
-                                            Instruction **lastInstruction) {
+const KInstruction *
+Executor::getLastNonKleeInternalInstruction(const ExecutionState &state) {
   // unroll the stack of the applications state and find
   // the last instruction which is not inside a KLEE internal function
-  ExecutionStack::call_stack_ty::const_reverse_iterator
-      it = state.stack.callStack().rbegin(),
-      itE = state.stack.callStack().rend();
+  auto it = state.stack.callStack().rbegin();
+  auto itE = state.stack.callStack().rend();
 
   // don't check beyond the outermost function (i.e. main())
   itE--;
 
-  const InstructionInfo *ii = 0;
+  const KInstruction *ki = nullptr;
   if (kmodule->internalFunctions.count(it->kf->function) == 0) {
-    ii = state.prevPC->info;
-    *lastInstruction = state.prevPC->inst;
+    ki = state.prevPC;
     //  Cannot return yet because even though
     //  it->function is not an internal function it might of
     //  been called from an internal function.
@@ -4649,21 +4643,19 @@ Executor::getLastNonKleeInternalInstruction(const ExecutionState &state,
     // function
     const Function *f = (*it->caller).inst->getParent()->getParent();
     if (kmodule->internalFunctions.count(f)) {
-      ii = 0;
+      ki = nullptr;
       continue;
     }
-    if (!ii) {
-      ii = (*it->caller).info;
-      *lastInstruction = (*it->caller).inst;
+    if (!ki) {
+      ki = it->caller;
     }
   }
 
-  if (!ii) {
+  if (!ki) {
     // something went wrong, play safe and return the current instruction info
-    *lastInstruction = state.prevPC->inst;
-    return *state.prevPC->info;
+    return state.prevPC;
   }
-  return *ii;
+  return ki;
 }
 
 bool shouldExitOn(StateTerminationType reason) {
@@ -4722,14 +4714,14 @@ void Executor::terminateStateOnError(ExecutionState &state,
                                      const char *suffix) {
   std::string message = messaget.str();
   static std::set<std::pair<Instruction *, std::string>> emittedErrors;
-  Instruction *lastInst;
-  const InstructionInfo &ii =
-      getLastNonKleeInternalInstruction(state, &lastInst);
+  const KInstruction *ki = getLastNonKleeInternalInstruction(state);
+  Instruction *lastInst = ki->inst;
 
   if (EmitAllErrors ||
       emittedErrors.insert(std::make_pair(lastInst, message)).second) {
-    if (!ii.file.empty()) {
-      klee_message("ERROR: %s:%d: %s", ii.file.c_str(), ii.line,
+    std::string filepath = ki->getSourceFilepath();
+    if (!filepath.empty()) {
+      klee_message("ERROR: %s:%zu: %s", filepath.c_str(), ki->getLine(),
                    message.c_str());
     } else {
       klee_message("ERROR: (location information missing) %s", message.c_str());
@@ -4740,10 +4732,13 @@ void Executor::terminateStateOnError(ExecutionState &state,
     std::string MsgString;
     llvm::raw_string_ostream msg(MsgString);
     msg << "Error: " << message << '\n';
-    if (!ii.file.empty()) {
-      msg << "File: " << ii.file << '\n' << "Line: " << ii.line << '\n';
-      if (ii.assemblyLine.hasValue()) {
-        msg << "assembly.ll line: " << ii.assemblyLine.getValue() << '\n';
+    if (!filepath.empty()) {
+      msg << "File: " << filepath << '\n' << "Line: " << ki->getLine() << '\n';
+      {
+        auto asmLine = ki->getKModule()->getAsmLine(ki->inst);
+        if (asmLine.has_value()) {
+          msg << "assembly.ll line: " << asmLine.value() << '\n';
+        }
       }
       msg << "State: " << state.getID() << '\n';
     }
@@ -4832,7 +4827,7 @@ void Executor::callExternalFunction(ExecutionState &state, KInstruction *target,
       if (i != arguments.size() - 1)
         os << ", ";
     }
-    os << ") at " << state.pc->getSourceLocation();
+    os << ") at " << state.pc->getSourceLocationString();
 
     if (AllExternalWarnings)
       klee_warning("%s", os.str().c_str());
@@ -4950,7 +4945,7 @@ void Executor::callExternalFunction(ExecutionState &state, KInstruction *target,
       if (i != arguments.size() - 1)
         os << ", ";
     }
-    os << ") at " << state.pc->getSourceLocation();
+    os << ") at " << state.pc->getSourceLocationString();
 
     if (AllExternalWarnings)
       klee_warning("%s", os.str().c_str());
@@ -5875,7 +5870,7 @@ void Executor::collectReads(
     const std::vector<IDType> &resolvedMemoryObjects,
     const std::vector<Assignment> &resolveConcretizations,
     std::vector<ref<Expr>> &results) {
-  ref<Expr> base = address;
+  ref<Expr> base = address; // TODO: unused
   unsigned size = bytes;
   if (state.isGEPExpr(address)) {
     base = state.gepExprBases[address].first;
@@ -6852,7 +6847,7 @@ void Executor::prepareSymbolicValue(ExecutionState &state,
 
 void Executor::prepareSymbolicRegister(ExecutionState &state, StackFrame &sf,
                                        unsigned regNum) {
-  KInstruction *allocInst = sf.kf->registerToInstructionMap[regNum];
+  KInstruction *allocInst = sf.kf->getInstructionByRegister(regNum);
   prepareSymbolicValue(state, sf, allocInst);
 }
 
@@ -6935,7 +6930,7 @@ void Executor::logState(const ExecutionState &state, int id,
   *f << state.symbolics.size() << " symbolics total. "
      << "Symbolics:\n";
   size_t sc = 0;
-  for (auto &symbolic : state.symbolics) {
+  for (const auto &symbolic : state.symbolics) {
     *f << "Symbolic number " << sc++ << "\n";
     *f << "Associated memory object: " << symbolic.memoryObject.get()->id
        << "\n";
@@ -7048,15 +7043,17 @@ void Executor::setInitializationGraph(
       // The objects have to be symbolic
       bool pointerFound = false, pointeeFound = false;
       size_t pointerIndex = 0, pointeeIndex = 0;
-      for (size_t i = 0; i < symbolics.size(); i++) {
-        if (symbolics[i].memoryObject == pointerResolution.first) {
+      size_t i = 0;
+      for (auto &symbolic : symbolics) {
+        if (symbolic.memoryObject == pointerResolution.first) {
           pointerIndex = i;
           pointerFound = true;
         }
-        if (symbolics[i].memoryObject->id == pointer.second.first) {
+        if (symbolic.memoryObject->id == pointer.second.first) {
           pointeeIndex = i;
           pointeeFound = true;
         }
+        ++i;
       }
       if (pointerFound && pointeeFound) {
         ref<ConstantExpr> offset = model.evaluate(pointerResolution.second);
@@ -7157,8 +7154,9 @@ bool Executor::getSymbolicSolution(const ExecutionState &state, KTest &res) {
 
   std::vector<SparseStorage<unsigned char>> values;
   std::vector<const Array *> objects;
-  for (unsigned i = 0; i != symbolics.size(); ++i)
-    objects.push_back(symbolics[i].array);
+  for (auto &symbolic : symbolics) {
+    objects.push_back(symbolic.array);
+  }
   bool success = solver->getInitialValues(extendedConstraints.cs(), objects,
                                           values, state.queryMetaData);
   solver->setTimeout(time::Span());
@@ -7169,19 +7167,23 @@ bool Executor::getSymbolicSolution(const ExecutionState &state, KTest &res) {
     return false;
   }
 
-  res.objects = new KTestObject[symbolics.size()];
   res.numObjects = symbolics.size();
+  res.objects = new KTestObject[res.numObjects];
 
-  for (unsigned i = 0; i != symbolics.size(); ++i) {
-    auto mo = symbolics[i].memoryObject;
-    KTestObject *o = &res.objects[i];
-    o->name = const_cast<char *>(mo->name.c_str());
-    o->address = mo->address;
-    o->numBytes = values[i].size();
-    o->bytes = new unsigned char[o->numBytes];
-    std::copy(values[i].begin(), values[i].end(), o->bytes);
-    o->numPointers = 0;
-    o->pointers = nullptr;
+  {
+    size_t i = 0;
+    for (auto &symbolic : symbolics) {
+      auto mo = symbolic.memoryObject;
+      KTestObject *o = &res.objects[i];
+      o->name = const_cast<char *>(mo->name.c_str());
+      o->address = mo->address;
+      o->numBytes = values[i].size();
+      o->bytes = new unsigned char[o->numBytes];
+      std::copy(values[i].begin(), values[i].end(), o->bytes);
+      o->numPointers = 0;
+      o->pointers = nullptr;
+      ++i;
+    }
   }
 
   Assignment model = Assignment(objects, values);
@@ -7194,9 +7196,8 @@ bool Executor::getSymbolicSolution(const ExecutionState &state, KTest &res) {
   return true;
 }
 
-void Executor::getCoveredLines(
-    const ExecutionState &state,
-    std::map<const std::string *, std::set<unsigned>> &res) {
+void Executor::getCoveredLines(const ExecutionState &state,
+                               std::map<std::string, std::set<unsigned>> &res) {
   res = state.coveredLines;
 }
 
@@ -7355,9 +7356,9 @@ void Executor::dumpStates() {
            sfIt != sf_ie; ++sfIt) {
         *os << "('" << sfIt->kf->function->getName().str() << "',";
         if (next == es->stack.callStack().end()) {
-          *os << es->prevPC->info->line << "), ";
+          *os << es->prevPC->getLine() << "), ";
         } else {
-          *os << next->caller->info->line << "), ";
+          *os << next->caller->getLine() << "), ";
           ++next;
         }
       }
@@ -7366,8 +7367,8 @@ void Executor::dumpStates() {
       InfoStackFrame &sf = es->stack.infoStack().back();
       uint64_t md2u =
           computeMinDistToUncovered(es->pc, sf.minDistToUncoveredOnReturn);
-      uint64_t icnt = theStatisticManager->getIndexedValue(stats::instructions,
-                                                           es->pc->info->id);
+      uint64_t icnt = theStatisticManager->getIndexedValue(
+          stats::instructions, es->pc->getGlobalIndex());
       uint64_t cpicnt =
           sf.callPathNode->statistics.getValue(stats::instructions);
 
diff --git a/lib/Core/Executor.h b/lib/Core/Executor.h
index 26c2e9bba5..a7e0df7160 100644
--- a/lib/Core/Executor.h
+++ b/lib/Core/Executor.h
@@ -78,7 +78,6 @@ class ExecutionState;
 class ExternalDispatcher;
 class Expr;
 template <class T> class ExprHashMap;
-class InstructionInfoTable;
 class KCallable;
 struct KFunction;
 struct KInstruction;
@@ -482,7 +481,7 @@ class Executor : public Interpreter {
 
   ref<Expr> readDest(ExecutionState &state, StackFrame &frame,
                      const KInstruction *target) {
-    unsigned index = target->dest;
+    unsigned index = target->getDest();
     ref<Expr> reg = frame.locals[index].value;
     if (!reg) {
       prepareSymbolicRegister(state, frame, index);
@@ -496,7 +495,7 @@ class Executor : public Interpreter {
   }
 
   Cell &getDestCell(const StackFrame &frame, const KInstruction *target) {
-    return frame.locals[target->dest];
+    return frame.locals[target->getDest()];
   }
 
   const Cell &eval(const KInstruction *ki, unsigned index,
@@ -567,10 +566,9 @@ class Executor : public Interpreter {
                              const MemoryObject *mo = nullptr) const;
 
   // Determines the \param lastInstruction of the \param state which is not KLEE
-  // internal and returns its InstructionInfo
-  const InstructionInfo &
-  getLastNonKleeInternalInstruction(const ExecutionState &state,
-                                    llvm::Instruction **lastInstruction);
+  // internal and returns its KInstruction
+  const KInstruction *
+  getLastNonKleeInternalInstruction(const ExecutionState &state);
 
   /// Remove state from queue and delete state
   void terminateState(ExecutionState &state,
@@ -729,9 +727,9 @@ class Executor : public Interpreter {
   setModule(std::vector<std::unique_ptr<llvm::Module>> &userModules,
             std::vector<std::unique_ptr<llvm::Module>> &libsModules,
             const ModuleOptions &opts,
-            const std::unordered_set<std::string> &mainModuleFunctions,
-            const std::unordered_set<std::string> &mainModuleGlobals,
-            std::unique_ptr<InstructionInfoTable> origInfos) override;
+            std::set<std::string> &&mainModuleFunctions,
+            std::set<std::string> &&mainModuleGlobals,
+            FLCtoOpcode &&origInstructions) override;
 
   void useSeeds(const std::vector<struct KTest *> *seeds) override {
     usingSeeds = seeds;
@@ -801,9 +799,8 @@ class Executor : public Interpreter {
 
   bool getSymbolicSolution(const ExecutionState &state, KTest &res) override;
 
-  void getCoveredLines(
-      const ExecutionState &state,
-      std::map<const std::string *, std::set<unsigned>> &res) override;
+  void getCoveredLines(const ExecutionState &state,
+                       std::map<std::string, std::set<unsigned>> &res) override;
 
   void getBlockPath(const ExecutionState &state,
                     std::string &blockPath) override;
diff --git a/lib/Core/ExecutorUtil.cpp b/lib/Core/ExecutorUtil.cpp
index 467982c81f..9a4c6054a0 100644
--- a/lib/Core/ExecutorUtil.cpp
+++ b/lib/Core/ExecutorUtil.cpp
@@ -134,7 +134,7 @@ ref<klee::ConstantExpr> Executor::evalConstant(const Constant *c,
       std::string msg("Cannot handle constant ");
       llvm::raw_string_ostream os(msg);
       os << "'" << *c << "' at location "
-         << (ki ? ki->getSourceLocation() : "[unknown]");
+         << (ki ? ki->getSourceLocationString() : "[unknown]");
       klee_error("%s", os.str().c_str());
     }
   }
@@ -261,7 +261,7 @@ ref<ConstantExpr> Executor::evalConstantExpr(const llvm::ConstantExpr *ce,
       std::string msg(
           "Division/modulo by zero during constant folding at location ");
       llvm::raw_string_ostream os(msg);
-      os << (ki ? ki->getSourceLocation() : "[unknown]");
+      os << (ki ? ki->getSourceLocationString() : "[unknown]");
       klee_error("%s", os.str().c_str());
     }
     break;
@@ -271,7 +271,7 @@ ref<ConstantExpr> Executor::evalConstantExpr(const llvm::ConstantExpr *ce,
     if (op2->getLimitedValue() >= op1->getWidth()) {
       std::string msg("Overshift during constant folding at location ");
       llvm::raw_string_ostream os(msg);
-      os << (ki ? ki->getSourceLocation() : "[unknown]");
+      os << (ki ? ki->getSourceLocationString() : "[unknown]");
       klee_error("%s", os.str().c_str());
     }
   }
@@ -282,7 +282,7 @@ ref<ConstantExpr> Executor::evalConstantExpr(const llvm::ConstantExpr *ce,
   switch (ce->getOpcode()) {
   default:
     os << "'" << *ce << "' at location "
-       << (ki ? ki->getSourceLocation() : "[unknown]");
+       << (ki ? ki->getSourceLocationString() : "[unknown]");
     klee_error("%s", os.str().c_str());
 
   case Instruction::Trunc:
diff --git a/lib/Core/Memory.h b/lib/Core/Memory.h
index e43e4d015b..503faca93a 100644
--- a/lib/Core/Memory.h
+++ b/lib/Core/Memory.h
@@ -125,7 +125,7 @@ class MemoryObject {
   /// Get an identifying string for this allocation.
   void getAllocInfo(std::string &result) const;
 
-  void setName(std::string name) const { this->name = name; }
+  void setName(const std::string &_name) const { this->name = _name; }
 
   void updateTimestamp() const { this->timestamp = time++; }
 
diff --git a/lib/Core/Searcher.cpp b/lib/Core/Searcher.cpp
index 30adeb8ce7..08e725eacb 100644
--- a/lib/Core/Searcher.cpp
+++ b/lib/Core/Searcher.cpp
@@ -19,7 +19,6 @@
 #include "klee/ADT/DiscretePDF.h"
 #include "klee/ADT/RNG.h"
 #include "klee/ADT/WeightedQueue.h"
-#include "klee/Module/InstructionInfoTable.h"
 #include "klee/Module/KInstruction.h"
 #include "klee/Module/KModule.h"
 #include "klee/Module/Target.h"
@@ -389,8 +388,8 @@ double WeightedRandomSearcher::getWeight(ExecutionState *es) {
   case RP:
     return std::pow(0.5, es->depth);
   case InstCount: {
-    uint64_t count = theStatisticManager->getIndexedValue(stats::instructions,
-                                                          es->pc->info->id);
+    uint64_t count = theStatisticManager->getIndexedValue(
+        stats::instructions, es->pc->getGlobalIndex());
     double inv = 1. / std::max((uint64_t)1, count);
     return inv * inv;
   }
diff --git a/lib/Core/SpecialFunctionHandler.cpp b/lib/Core/SpecialFunctionHandler.cpp
index 6138eabe1b..a9d7457a88 100644
--- a/lib/Core/SpecialFunctionHandler.cpp
+++ b/lib/Core/SpecialFunctionHandler.cpp
@@ -921,7 +921,7 @@ void SpecialFunctionHandler::handleMakeSymbolic(
     assert(success && "FIXME: Unhandled solver failure");
 
     if (res) {
-      uint64_t sid = 0;
+      uint64_t sid = 0; // TODO: unused variable
       if (state.arrayNames.count(name)) {
         sid = state.arrayNames[name];
       }
diff --git a/lib/Core/StatsTracker.cpp b/lib/Core/StatsTracker.cpp
index e662644be3..3a1f3a11f2 100644
--- a/lib/Core/StatsTracker.cpp
+++ b/lib/Core/StatsTracker.cpp
@@ -13,9 +13,9 @@
 
 #include "klee/Config/Version.h"
 #include "klee/Core/TerminationTypes.h"
-#include "klee/Module/InstructionInfoTable.h"
 #include "klee/Module/KInstruction.h"
 #include "klee/Module/KModule.h"
+#include "klee/Module/LocationInfo.h"
 #include "klee/Solver/SolverStats.h"
 #include "klee/Statistics/Statistics.h"
 #include "klee/Support/ErrorHandling.h"
@@ -233,27 +233,25 @@ StatsTracker::StatsTracker(Executor &_executor, std::string _objectFilename,
   }
 
   if (useStatistics() || userSearcherRequiresMD2U())
-    theStatisticManager->useIndexedStats(km->infos->getMaxID());
+    theStatisticManager->useIndexedStats(km->getMaxGlobalIndex());
 
   for (auto &kfp : km->functions) {
     KFunction *kf = kfp.get();
-    kf->trackCoverage = 1;
 
     for (unsigned i = 0; i < kf->numInstructions; ++i) {
       KInstruction *ki = kf->instructions[i];
 
       if (OutputIStats) {
-        unsigned id = ki->info->id;
+        unsigned id = ki->getGlobalIndex();
         theStatisticManager->setIndex(id);
-        if (kf->trackCoverage && instructionIsCoverable(ki->inst))
+        if (instructionIsCoverable(ki->inst)) {
           ++stats::uncoveredInstructions;
+        }
       }
 
-      if (kf->trackCoverage) {
-        if (BranchInst *bi = dyn_cast<BranchInst>(ki->inst))
-          if (!bi->isUnconditional())
-            numBranches++;
-      }
+      if (BranchInst *bi = dyn_cast<BranchInst>(ki->inst))
+        if (!bi->isUnconditional())
+          numBranches++;
     }
   }
 
@@ -393,24 +391,24 @@ void StatsTracker::stepInstruction(ExecutionState &es) {
     }
 
     Instruction *inst = es.pc->inst;
-    const InstructionInfo &ii = *es.pc->info;
+    const KInstruction *ki = es.pc;
     InfoStackFrame &sf = es.stack.infoStack().back();
-    theStatisticManager->setIndex(ii.id);
+    theStatisticManager->setIndex(ki->getGlobalIndex());
     if (UseCallPaths)
       theStatisticManager->setContext(&sf.callPathNode->statistics);
 
     if (es.instsSinceCovNew)
       ++es.instsSinceCovNew;
 
-    if (sf.kf->trackCoverage && instructionIsCoverable(inst)) {
+    if (instructionIsCoverable(inst)) {
       if (!theStatisticManager->getIndexedValue(stats::coveredInstructions,
-                                                ii.id)) {
+                                                ki->getGlobalIndex())) {
         // Checking for actual stoppoints avoids inconsistencies due
         // to line number propogation.
         //
         // FIXME: This trick no longer works, we should fix this in the line
         // number propogation.
-        es.coveredLines[&ii.file].insert(ii.line);
+        es.coveredLines[ki->getSourceFilepath()].insert(ki->getLine());
         es.instsSinceCovNew = 1;
         ++stats::coveredInstructions;
         stats::uncoveredInstructions += (uint64_t)-1;
@@ -695,8 +693,8 @@ void StatsTracker::updateStateStatistics(uint64_t addend) {
                                             ie = executor.states.end();
        it != ie; ++it) {
     ExecutionState &state = **it;
-    const InstructionInfo &ii = *state.pc->info;
-    theStatisticManager->incrementIndexedValue(stats::states, ii.id, addend);
+    theStatisticManager->incrementIndexedValue(
+        stats::states, state.pc->getGlobalIndex(), addend);
     if (UseCallPaths)
       state.stack.infoStack().back().callPathNode->statistics.incrementValue(
           stats::states, addend);
@@ -765,66 +763,70 @@ void StatsTracker::writeIStats() {
 
   of << "ob=" << llvm::sys::path::filename(objectFilename).str() << "\n";
 
-  for (Module::iterator fnIt = m->begin(), fn_ie = m->end(); fnIt != fn_ie;
-       ++fnIt) {
-    if (!fnIt->isDeclaration()) {
+  for (auto &fn : *m) {
+    if (!fn.isDeclaration()) {
       // 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.
-      Function *fn = &*fnIt;
-      const FunctionInfo &ii = executor.kmodule->infos->getFunctionInfo(*fn);
-      if (ii.file != sourceFile) {
-        of << "fl=" << ii.file << "\n";
-        sourceFile = ii.file;
+      auto fnlFile = getLocationInfo(&fn).file;
+      if (fnlFile != sourceFile) {
+        of << "fl=" << fnlFile << "\n";
+        sourceFile = fnlFile;
       }
 
-      of << "fn=" << fnIt->getName().str() << "\n";
-      for (Function::iterator bbIt = fnIt->begin(), bb_ie = fnIt->end();
-           bbIt != bb_ie; ++bbIt) {
-        for (BasicBlock::iterator it = bbIt->begin(), ie = bbIt->end();
-             it != ie; ++it) {
-          Instruction *instr = &*it;
-          const InstructionInfo &ii = executor.kmodule->infos->getInfo(*instr);
-          unsigned index = ii.id;
-          if (ii.file != sourceFile) {
-            of << "fl=" << ii.file << "\n";
-            sourceFile = ii.file;
+      of << "fn=" << fn.getName().str() << "\n";
+      for (auto &bb : fn) {
+        for (auto &instr : bb) {
+          Instruction *instrPtr = &instr;
+
+          auto instrLI = getLocationInfo(instrPtr);
+
+          unsigned index = executor.kmodule->getGlobalIndex(instrPtr);
+          if (instrLI.file != sourceFile) {
+            of << "fl=" << instrLI.file << "\n";
+            sourceFile = instrLI.file;
           }
 
-          assert(ii.assemblyLine.hasValue());
-          of << ii.assemblyLine.getValue() << " ";
+          {
+            auto asmLine = executor.kmodule->getAsmLine(instrPtr);
+            assert(asmLine.has_value());
+            of << asmLine.value() << " ";
+          }
 
-          of << ii.line << " ";
+          of << instrLI.line << " ";
           for (unsigned i = 0; i < nStats; i++)
             if (istatsMask.test(i))
               of << sm.getIndexedValue(sm.getStatistic(i), index) << " ";
           of << "\n";
 
           if (UseCallPaths &&
-              (isa<CallInst>(instr) || isa<InvokeInst>(instr))) {
-            CallSiteSummaryTable::iterator it = callSiteStats.find(instr);
+              (isa<CallInst>(instrPtr) || isa<InvokeInst>(instrPtr))) {
+            CallSiteSummaryTable::iterator it = callSiteStats.find(instrPtr);
             if (it != callSiteStats.end()) {
-              for (auto fit = it->second.begin(), fie = it->second.end();
-                   fit != fie; ++fit) {
-                const Function *f = fit->first;
-                CallSiteInfo &csi = fit->second;
-                const FunctionInfo &fii =
-                    executor.kmodule->infos->getFunctionInfo(*f);
-
-                if (fii.file != "" && fii.file != sourceFile)
-                  of << "cfl=" << fii.file << "\n";
+              for (auto &fit : it->second) {
+                const Function *f = fit.first;
+                CallSiteInfo &csi = fit.second;
+                auto fli = getLocationInfo(f);
+                if (fli.file != "" && fli.file != sourceFile)
+                  of << "cfl=" << fli.file << "\n";
                 of << "cfn=" << f->getName().str() << "\n";
                 of << "calls=" << csi.count << " ";
 
-                assert(fii.assemblyLine.hasValue());
-                of << fii.assemblyLine.getValue() << " ";
+                {
+                  auto asmLine = executor.kmodule->getAsmLine(f);
+                  assert(asmLine.has_value());
+                  of << asmLine.value() << " ";
+                }
 
-                of << fii.line << "\n";
+                of << fli.line << "\n";
 
-                assert(ii.assemblyLine.hasValue());
-                of << ii.assemblyLine.getValue() << " ";
+                {
+                  auto asmLine = executor.kmodule->getAsmLine(instrPtr);
+                  assert(asmLine.has_value());
+                  of << asmLine.value() << " ";
+                }
 
-                of << ii.line << " ";
+                of << instrLI.line << " ";
                 for (unsigned i = 0; i < nStats; i++) {
                   if (istatsMask.test(i)) {
                     Statistic &s = sm.getStatistic(i);
@@ -889,12 +891,12 @@ uint64_t klee::computeMinDistToUncovered(const KInstruction *ki,
                                          uint64_t minDistAtRA) {
   StatisticManager &sm = *theStatisticManager;
   if (minDistAtRA == 0) { // unreachable on return, best is local
-    return sm.getIndexedValue(stats::minDistToUncovered, ki->info->id);
+    return sm.getIndexedValue(stats::minDistToUncovered, ki->getGlobalIndex());
   } else {
     uint64_t minDistLocal =
-        sm.getIndexedValue(stats::minDistToUncovered, ki->info->id);
+        sm.getIndexedValue(stats::minDistToUncovered, ki->getGlobalIndex());
     uint64_t distToReturn =
-        sm.getIndexedValue(stats::minDistToReturn, ki->info->id);
+        sm.getIndexedValue(stats::minDistToReturn, ki->getGlobalIndex());
 
     if (distToReturn == 0) { // return unreachable, best is local
       return minDistLocal;
@@ -910,7 +912,6 @@ void StatsTracker::computeReachableUncovered() {
   KModule *km = executor.kmodule.get();
   const auto m = km->module.get();
   static bool init = true;
-  const InstructionInfoTable &infos = *km->infos;
   StatisticManager &sm = *theStatisticManager;
 
   if (init) {
@@ -973,11 +974,10 @@ void StatsTracker::computeReachableUncovered() {
       // Not sure if I should bother to preorder here. XXX I should.
       for (Function::iterator bbIt = fnIt->begin(), bb_ie = fnIt->end();
            bbIt != bb_ie; ++bbIt) {
-        for (BasicBlock::iterator it = bbIt->begin(), ie = bbIt->end();
-             it != ie; ++it) {
-          Instruction *inst = &*it;
+        for (auto &it : *bbIt) {
+          Instruction *inst = &it;
           instructions.push_back(inst);
-          unsigned id = infos.getInfo(*inst).id;
+          unsigned id = km->getGlobalIndex(inst);
           sm.setIndexedValue(stats::minDistToReturn, id, isa<ReturnInst>(inst));
         }
       }
@@ -989,9 +989,8 @@ void StatsTracker::computeReachableUncovered() {
     bool changed;
     do {
       changed = false;
-      for (auto it = instructions.begin(), ie = instructions.end(); it != ie;
-           ++it) {
-        Instruction *inst = *it;
+      for (auto &instruction : instructions) {
+        Instruction *inst = instruction;
         unsigned bestThrough = 0;
 
         if (isa<CallInst>(inst) || isa<InvokeInst>(inst)) {
@@ -1011,15 +1010,15 @@ void StatsTracker::computeReachableUncovered() {
         }
 
         if (bestThrough) {
-          unsigned id = infos.getInfo(*(*it)).id;
+          unsigned id = km->getGlobalIndex(instruction);
           uint64_t best,
               cur = best = sm.getIndexedValue(stats::minDistToReturn, id);
-          std::vector<Instruction *> succs = getSuccs(*it);
+          std::vector<Instruction *> succs = getSuccs(instruction);
           for (std::vector<Instruction *>::iterator it2 = succs.begin(),
                                                     ie = succs.end();
                it2 != ie; ++it2) {
             uint64_t dist = sm.getIndexedValue(stats::minDistToReturn,
-                                               infos.getInfo(*(*it2)).id);
+                                               km->getGlobalIndex(*it2));
             if (dist) {
               uint64_t val = bestThrough + dist;
               if (best == 0 || val < best)
@@ -1055,7 +1054,7 @@ void StatsTracker::computeReachableUncovered() {
       for (BasicBlock::iterator it = bbIt->begin(), ie = bbIt->end(); it != ie;
            ++it) {
         Instruction *inst = &*it;
-        unsigned id = infos.getInfo(*inst).id;
+        unsigned id = km->getGlobalIndex(inst);
         instructions.push_back(inst);
         sm.setIndexedValue(
             stats::minDistToUncovered, id,
@@ -1070,29 +1069,24 @@ void StatsTracker::computeReachableUncovered() {
   bool changed;
   do {
     changed = false;
-    for (std::vector<Instruction *>::iterator it = instructions.begin(),
-                                              ie = instructions.end();
-         it != ie; ++it) {
-      Instruction *inst = *it;
+    for (auto inst : instructions) {
       uint64_t best, cur = best = sm.getIndexedValue(stats::minDistToUncovered,
-                                                     infos.getInfo(*inst).id);
+                                                     km->getGlobalIndex(inst));
       unsigned bestThrough = 0;
 
       if (isa<CallInst>(inst) || isa<InvokeInst>(inst)) {
         std::vector<Function *> &targets = callTargets[inst];
-        for (std::vector<Function *>::iterator fnIt = targets.begin(),
-                                               ie = targets.end();
-             fnIt != ie; ++fnIt) {
-          uint64_t dist = functionShortestPath[*fnIt];
+        for (auto &target : targets) {
+          uint64_t dist = functionShortestPath[target];
           if (dist) {
             dist = 1 + dist; // count instruction itself
             if (bestThrough == 0 || dist < bestThrough)
               bestThrough = dist;
           }
 
-          if (!(*fnIt)->isDeclaration()) {
+          if (!target->isDeclaration()) {
             uint64_t calleeDist = sm.getIndexedValue(
-                stats::minDistToUncovered, infos.getFunctionInfo(*(*fnIt)).id);
+                stats::minDistToUncovered, km->getGlobalIndex(target));
             if (calleeDist) {
               calleeDist = 1 + calleeDist; // count instruction itself
               if (best == 0 || calleeDist < best)
@@ -1106,11 +1100,9 @@ void StatsTracker::computeReachableUncovered() {
 
       if (bestThrough) {
         std::vector<Instruction *> succs = getSuccs(inst);
-        for (std::vector<Instruction *>::iterator it2 = succs.begin(),
-                                                  ie = succs.end();
-             it2 != ie; ++it2) {
+        for (auto &succ : succs) {
           uint64_t dist = sm.getIndexedValue(stats::minDistToUncovered,
-                                             infos.getInfo(*(*it2)).id);
+                                             km->getGlobalIndex(succ));
           if (dist) {
             uint64_t val = bestThrough + dist;
             if (best == 0 || val < best)
@@ -1120,7 +1112,7 @@ void StatsTracker::computeReachableUncovered() {
       }
 
       if (best != cur) {
-        sm.setIndexedValue(stats::minDistToUncovered, infos.getInfo(*inst).id,
+        sm.setIndexedValue(stats::minDistToUncovered, km->getGlobalIndex(inst),
                            best);
         changed = true;
       }
diff --git a/lib/Core/StatsTracker.h b/lib/Core/StatsTracker.h
index be0f39ae5b..52a85d560c 100644
--- a/lib/Core/StatsTracker.h
+++ b/lib/Core/StatsTracker.h
@@ -27,7 +27,6 @@ class raw_fd_ostream;
 namespace klee {
 class ExecutionState;
 class Executor;
-class InstructionInfoTable;
 class InterpreterHandler;
 struct KInstruction;
 struct InfoStackFrame;
diff --git a/lib/Core/TargetedExecutionManager.cpp b/lib/Core/TargetedExecutionManager.cpp
index 9f9b498738..a46a12e3c9 100644
--- a/lib/Core/TargetedExecutionManager.cpp
+++ b/lib/Core/TargetedExecutionManager.cpp
@@ -318,24 +318,27 @@ TargetedExecutionManager::LocationToBlocks
 TargetedExecutionManager::prepareAllLocations(KModule *kmodule,
                                               Locations &locations) const {
   LocationToBlocks locToBlocks;
-  const auto &infos = kmodule->infos;
+  std::unordered_map<std::string, std::unordered_set<const llvm::Function *>>
+      fileNameToFunctions;
+
+  for (const auto &kfunc : kmodule->functions) {
+    fileNameToFunctions[kfunc->getSourceFilepath()].insert(kfunc->function);
+  }
+
   for (auto it = locations.begin(); it != locations.end(); ++it) {
     auto loc = *it;
-    for (const auto &fileName : infos->getFilesNames()) {
-      if (kmodule->origInfos.count(fileName) == 0) {
+    for (const auto &[fileName, origInstsInFile] : kmodule->origInstructions) {
+      if (kmodule->origInstructions.count(fileName) == 0) {
         continue;
       }
       if (!loc->isInside(fileName)) {
         continue;
       }
 
-      const auto &relatedFunctions =
-          infos->getFileNameToFunctions().at(fileName);
+      const auto &relatedFunctions = fileNameToFunctions.at(fileName);
 
       for (const auto func : relatedFunctions) {
         const auto kfunc = kmodule->functionMap[func];
-        const auto &fi = infos->getFunctionInfo(*kfunc->function);
-        const auto &origInstsInFile = kmodule->origInfos.at(fi.file);
 
         for (const auto &kblock : kfunc->blocks) {
           auto b = kblock.get();
@@ -524,7 +527,7 @@ TargetedExecutionManager::prepareTargets(KModule *kmodule, SarifReport paths) {
 void TargetedExecutionManager::reportFalseNegative(ExecutionState &state,
                                                    ReachWithError error) {
   klee_warning("100.00%% %s False Negative at: %s", getErrorString(error),
-               state.prevPC->getSourceLocation().c_str());
+               state.prevPC->getSourceLocationString().c_str());
 }
 
 bool TargetedExecutionManager::reportTruePositive(ExecutionState &state,
diff --git a/lib/Core/TargetedExecutionManager.h b/lib/Core/TargetedExecutionManager.h
index e5a66cbf32..93ea108a07 100644
--- a/lib/Core/TargetedExecutionManager.h
+++ b/lib/Core/TargetedExecutionManager.h
@@ -96,12 +96,6 @@ class TargetedExecutionManager {
   using StatesSet = std::unordered_set<ExecutionState *>;
   using TargetToStateUnorderedSetMap = TargetHashMap<StatesSet>;
 
-  using Instructions = std::unordered_map<
-      std::string,
-      std::unordered_map<
-          unsigned int,
-          std::unordered_map<unsigned int, std::unordered_set<unsigned int>>>>;
-
   std::unordered_set<std::string> brokenTraces;
   std::unordered_set<std::string> reportedTraces;
 
diff --git a/lib/Expr/ExprPPrinter.cpp b/lib/Expr/ExprPPrinter.cpp
index bde8d30d6d..165b438025 100644
--- a/lib/Expr/ExprPPrinter.cpp
+++ b/lib/Expr/ExprPPrinter.cpp
@@ -409,8 +409,8 @@ class PPrinter : public ExprPPrinter {
       auto kf = s->km->functionMap.at(s->allocSite.getFunction());
       auto ki = kf->instructionMap.at(&s->allocSite);
       auto kb = ki->parent;
-      PC << ki->index << " " << kb->getLabel() << " " << kf->getName().str()
-         << " " << s->index;
+      PC << ki->getIndex() << " " << kb->getLabel() << " "
+         << kf->getName().str() << " " << s->index;
     } else if (auto s = dyn_cast<IrreproducibleSource>(source)) {
       PC << s->name;
     } else {
diff --git a/lib/Expr/Path.cpp b/lib/Expr/Path.cpp
index 7b578aa30c..e67abd51b4 100644
--- a/lib/Expr/Path.cpp
+++ b/lib/Expr/Path.cpp
@@ -15,8 +15,8 @@ using namespace llvm;
 
 void Path::advance(KInstruction *ki) {
   if (KBlocks.empty()) {
-    firstInstruction = ki->index;
-    lastInstruction = ki->index;
+    firstInstruction = ki->getIndex();
+    lastInstruction = ki->getIndex();
     KBlocks.push_back(ki->parent);
     return;
   }
@@ -24,8 +24,7 @@ void Path::advance(KInstruction *ki) {
   if (ki->parent != lastBlock) {
     KBlocks.push_back(ki->parent);
   }
-  lastInstruction = ki->index;
-  return;
+  lastInstruction = ki->getIndex();
 }
 
 unsigned Path::KBlockSize() const { return KBlocks.size(); }
diff --git a/lib/Expr/SymbolicSource.cpp b/lib/Expr/SymbolicSource.cpp
index 0e7f8b1086..9d8d3b6e58 100644
--- a/lib/Expr/SymbolicSource.cpp
+++ b/lib/Expr/SymbolicSource.cpp
@@ -98,9 +98,8 @@ int ArgumentSource::internalCompare(const SymbolicSource &b) const {
   assert(km == ab.km);
   auto parent = allocSite.getParent();
   auto bParent = ab.allocSite.getParent();
-  if (km->functionIDMap.at(parent) != km->functionIDMap.at(bParent)) {
-    return km->functionIDMap.at(parent) < km->functionIDMap.at(bParent) ? -1
-                                                                        : 1;
+  if (km->getFunctionId(parent) != km->getFunctionId(bParent)) {
+    return km->getFunctionId(parent) < km->getFunctionId(bParent) ? -1 : 1;
   }
   if (allocSite.getArgNo() != ab.allocSite.getArgNo()) {
     return allocSite.getArgNo() < ab.allocSite.getArgNo() ? -1 : 1;
@@ -119,20 +118,20 @@ int InstructionSource::internalCompare(const SymbolicSource &b) const {
   assert(km == ib.km);
   auto function = allocSite.getParent()->getParent();
   auto bFunction = ib.allocSite.getParent()->getParent();
-  if (km->functionIDMap.at(function) != km->functionIDMap.at(bFunction)) {
-    return km->functionIDMap.at(function) < km->functionIDMap.at(bFunction) ? -1
-                                                                            : 1;
+  if (km->getFunctionId(function) != km->getFunctionId(bFunction)) {
+    return km->getFunctionId(function) < km->getFunctionId(bFunction) ? -1 : 1;
   }
   auto kf = km->functionMap.at(function);
   auto block = allocSite.getParent();
   auto bBlock = ib.allocSite.getParent();
-  if (kf->blockMap[block]->id != kf->blockMap[bBlock]->id) {
-    return kf->blockMap[block]->id < kf->blockMap[bBlock]->id ? -1 : 1;
+  if (kf->blockMap[block]->getId() != kf->blockMap[bBlock]->getId()) {
+    return kf->blockMap[block]->getId() < kf->blockMap[bBlock]->getId() ? -1
+                                                                        : 1;
   }
-  if (kf->instructionMap[&allocSite]->index !=
-      kf->instructionMap[&ib.allocSite]->index) {
-    return kf->instructionMap[&allocSite]->index <
-                   kf->instructionMap[&ib.allocSite]->index
+  if (kf->instructionMap[&allocSite]->getIndex() !=
+      kf->instructionMap[&ib.allocSite]->getIndex()) {
+    return kf->instructionMap[&allocSite]->getIndex() <
+                   kf->instructionMap[&ib.allocSite]->getIndex()
                ? -1
                : 1;
   }
@@ -142,8 +141,7 @@ int InstructionSource::internalCompare(const SymbolicSource &b) const {
 unsigned ArgumentSource::computeHash() {
   unsigned res = (getKind() * SymbolicSource::MAGIC_HASH_CONSTANT) + index;
   auto parent = allocSite.getParent();
-  res = (res * SymbolicSource::MAGIC_HASH_CONSTANT) +
-        km->functionIDMap.at(parent);
+  res = (res * SymbolicSource::MAGIC_HASH_CONSTANT) + km->getFunctionId(parent);
   res = (res * SymbolicSource::MAGIC_HASH_CONSTANT) + allocSite.getArgNo();
   hashValue = res;
   return hashValue;
@@ -154,11 +152,12 @@ unsigned InstructionSource::computeHash() {
   auto function = allocSite.getParent()->getParent();
   auto kf = km->functionMap.at(function);
   auto block = allocSite.getParent();
+  res =
+      (res * SymbolicSource::MAGIC_HASH_CONSTANT) + km->getFunctionId(function);
   res = (res * SymbolicSource::MAGIC_HASH_CONSTANT) +
-        km->functionIDMap.at(function);
-  res = (res * SymbolicSource::MAGIC_HASH_CONSTANT) + kf->blockMap[block]->id;
+        kf->blockMap[block]->getId();
   res = (res * SymbolicSource::MAGIC_HASH_CONSTANT) +
-        kf->instructionMap[&allocSite]->index;
+        kf->instructionMap[&allocSite]->getIndex();
   hashValue = res;
   return hashValue;
 }
diff --git a/lib/Module/CMakeLists.txt b/lib/Module/CMakeLists.txt
index 81112acbe0..42ef35556b 100644
--- a/lib/Module/CMakeLists.txt
+++ b/lib/Module/CMakeLists.txt
@@ -11,7 +11,7 @@ set(KLEE_MODULE_COMPONENT_SRCS
   Checks.cpp
   CodeGraphInfo.cpp
   FunctionAlias.cpp
-  InstructionInfoTable.cpp
+  LocationInfo.cpp
   InstructionOperandTypeCheckPass.cpp
   IntrinsicCleaner.cpp
   KInstruction.cpp
diff --git a/lib/Module/InstructionInfoTable.cpp b/lib/Module/InstructionInfoTable.cpp
deleted file mode 100644
index ee66e91cbf..0000000000
--- a/lib/Module/InstructionInfoTable.cpp
+++ /dev/null
@@ -1,230 +0,0 @@
-//===-- InstructionInfoTable.cpp ------------------------------------------===//
-//
-//                     The KLEE Symbolic Virtual Machine
-//
-// This file is distributed under the University of Illinois Open Source
-// License. See LICENSE.TXT for details.
-//
-//===----------------------------------------------------------------------===//
-
-#include "klee/Module/InstructionInfoTable.h"
-#include "klee/Config/Version.h"
-
-#include "klee/Support/CompilerWarning.h"
-DISABLE_WARNING_PUSH
-DISABLE_WARNING_DEPRECATED_DECLARATIONS
-#include "llvm/Analysis/ValueTracking.h"
-#include "llvm/IR/AssemblyAnnotationWriter.h"
-#include "llvm/IR/DebugInfo.h"
-#include "llvm/IR/DebugInfoMetadata.h"
-#include "llvm/IR/Function.h"
-#include "llvm/IR/InstIterator.h"
-#include "llvm/IR/Instructions.h"
-#include "llvm/IR/IntrinsicInst.h"
-#include "llvm/IR/LLVMContext.h"
-#include "llvm/IR/Module.h"
-#include "llvm/Linker/Linker.h"
-#include "llvm/Support/ErrorHandling.h"
-#include "llvm/Support/FormattedStream.h"
-#include "llvm/Support/Path.h"
-#include "llvm/Support/raw_ostream.h"
-DISABLE_WARNING_POP
-
-#include <cstdint>
-#include <map>
-#include <string>
-
-using namespace klee;
-
-class InstructionToLineAnnotator : public llvm::AssemblyAnnotationWriter {
-private:
-  std::unordered_map<uintptr_t, uint64_t> mapping = {};
-
-public:
-  void emitInstructionAnnot(const llvm::Instruction *i,
-                            llvm::formatted_raw_ostream &os) override {
-    os.flush();
-    mapping.emplace(reinterpret_cast<std::uintptr_t>(i), os.getLine() + 1);
-  }
-
-  void emitFunctionAnnot(const llvm::Function *f,
-                         llvm::formatted_raw_ostream &os) override {
-    os.flush();
-    mapping.emplace(reinterpret_cast<std::uintptr_t>(f), os.getLine() + 1);
-  }
-
-  std::unordered_map<uintptr_t, uint64_t> getMapping() const { return mapping; }
-};
-
-static std::unordered_map<uintptr_t, uint64_t>
-buildInstructionToLineMap(const llvm::Module &m,
-                          std::unique_ptr<llvm::raw_fd_ostream> assemblyFS) {
-
-  InstructionToLineAnnotator a;
-
-  m.print(*assemblyFS, &a);
-  assemblyFS->flush();
-
-  return a.getMapping();
-}
-
-class DebugInfoExtractor {
-  std::vector<std::unique_ptr<std::string>> &internedStrings;
-  std::unordered_map<uintptr_t, uint64_t> lineTable;
-
-  const llvm::Module &module;
-  bool withAsm = false;
-
-public:
-  DebugInfoExtractor(
-      std::vector<std::unique_ptr<std::string>> &_internedStrings,
-      const llvm::Module &_module,
-      std::unique_ptr<llvm::raw_fd_ostream> assemblyFS)
-      : internedStrings(_internedStrings), module(_module) {
-    if (assemblyFS) {
-      withAsm = true;
-      lineTable = buildInstructionToLineMap(module, std::move(assemblyFS));
-    }
-  }
-
-  std::string &getInternedString(const std::string &s) {
-    auto found = std::find_if(internedStrings.begin(), internedStrings.end(),
-                              [&s](const std::unique_ptr<std::string> &item) {
-                                return *item.get() == s;
-                              });
-    if (found != internedStrings.end())
-      return *found->get();
-
-    auto newItem = std::unique_ptr<std::string>(new std::string(s));
-    auto result = newItem.get();
-
-    internedStrings.emplace_back(std::move(newItem));
-    return *result;
-  }
-
-  std::unique_ptr<FunctionInfo> getFunctionInfo(const llvm::Function &Func) {
-    llvm::Optional<uint64_t> asmLine;
-    if (withAsm) {
-      asmLine = lineTable.at(reinterpret_cast<std::uintptr_t>(&Func));
-    }
-    auto dsub = Func.getSubprogram();
-
-    if (dsub != nullptr) {
-      auto path = dsub->getFilename();
-      return std::make_unique<FunctionInfo>(FunctionInfo(
-          0, getInternedString(path.str()), dsub->getLine(), asmLine));
-    }
-
-    // Fallback: Mark as unknown
-    return std::make_unique<FunctionInfo>(
-        FunctionInfo(0, getInternedString(""), 0, asmLine));
-  }
-
-  std::unique_ptr<InstructionInfo>
-  getInstructionInfo(const llvm::Instruction &Inst, const FunctionInfo *f) {
-    llvm::Optional<uint64_t> asmLine;
-    if (withAsm) {
-      asmLine = lineTable.at(reinterpret_cast<std::uintptr_t>(&Inst));
-    }
-
-    // Retrieve debug information associated with instruction
-    auto dl = Inst.getDebugLoc();
-
-    // Check if a valid debug location is assigned to the instruction.
-    if (dl.get() != nullptr) {
-      auto full_path = dl.get()->getFilename();
-      auto line = dl.getLine();
-      auto column = dl.getCol();
-
-      // Still, if the line is unknown, take the context of the instruction to
-      // narrow it down
-      if (line == 0) {
-        if (auto LexicalBlock =
-                llvm::dyn_cast<llvm::DILexicalBlock>(dl.getScope())) {
-          line = LexicalBlock->getLine();
-          column = LexicalBlock->getColumn();
-        }
-      }
-      return std::make_unique<InstructionInfo>(InstructionInfo(
-          0, getInternedString(full_path.str()), line, column, asmLine));
-    }
-
-    if (f != nullptr)
-      // If nothing found, use the surrounding function
-      return std::make_unique<InstructionInfo>(
-          InstructionInfo(0, f->file, f->line, 0, asmLine));
-    // If nothing found, use the surrounding function
-    return std::make_unique<InstructionInfo>(
-        InstructionInfo(0, getInternedString(""), 0, 0, asmLine));
-  }
-};
-
-InstructionInfoTable::InstructionInfoTable(
-    const llvm::Module &m, std::unique_ptr<llvm::raw_fd_ostream> assemblyFS,
-    bool withInstructions) {
-  // Generate all debug instruction information
-  DebugInfoExtractor DI(internedStrings, m, std::move(assemblyFS));
-
-  for (const auto &Func : m) {
-    auto F = DI.getFunctionInfo(Func);
-    auto FR = F.get();
-    functionInfos.emplace(&Func, std::move(F));
-
-    for (auto it = llvm::inst_begin(Func), ie = llvm::inst_end(Func); it != ie;
-         ++it) {
-      auto instr = &*it;
-      auto instInfo = DI.getInstructionInfo(*instr, FR);
-      if (withInstructions) {
-        insts[instInfo->file][instInfo->line][instInfo->column].insert(
-            instr->getOpcode());
-      }
-      filesNames.insert(instInfo->file);
-      fileNameToFunctions[instInfo->file].insert(&Func);
-      infos.emplace(instr, std::move(instInfo));
-    }
-  }
-
-  // Make sure that every item has a unique ID
-  size_t idCounter = 0;
-  for (auto &item : infos)
-    item.second->id = idCounter++;
-  for (auto &item : functionInfos)
-    item.second->id = idCounter++;
-}
-
-unsigned InstructionInfoTable::getMaxID() const {
-  return infos.size() + functionInfos.size();
-}
-
-const InstructionInfo &
-InstructionInfoTable::getInfo(const llvm::Instruction &inst) const {
-  auto it = infos.find(&inst);
-  if (it == infos.end())
-    llvm::report_fatal_error("invalid instruction, not present in "
-                             "initial module!");
-  return *it->second.get();
-}
-
-const FunctionInfo &
-InstructionInfoTable::getFunctionInfo(const llvm::Function &f) const {
-  auto found = functionInfos.find(&f);
-  if (found == functionInfos.end())
-    llvm::report_fatal_error("invalid instruction, not present in "
-                             "initial module!");
-
-  return *found->second.get();
-}
-
-const InstructionInfoTable::LocationToFunctionsMap &
-InstructionInfoTable::getFileNameToFunctions() const {
-  return fileNameToFunctions;
-}
-
-const std::unordered_set<std::string> &
-InstructionInfoTable::getFilesNames() const {
-  return filesNames;
-}
-
-InstructionInfoTable::Instructions InstructionInfoTable::getInstructions() {
-  return std::move(insts);
-}
diff --git a/lib/Module/KInstruction.cpp b/lib/Module/KInstruction.cpp
index f7159c4bd6..b5c33fe41d 100644
--- a/lib/Module/KInstruction.cpp
+++ b/lib/Module/KInstruction.cpp
@@ -9,11 +9,15 @@
 
 #include "klee/Module/KInstruction.h"
 #include "klee/Module/KModule.h"
+#include "klee/Module/LocationInfo.h"
 
 #include "klee/Support/CompilerWarning.h"
 DISABLE_WARNING_PUSH
 DISABLE_WARNING_DEPRECATED_DECLARATIONS
 #include "llvm/ADT/StringExtras.h"
+#include "llvm/IR/DebugInfoMetadata.h"
+#include <llvm/IR/InstrTypes.h>
+#include <llvm/IR/Instructions.h>
 DISABLE_WARNING_POP
 
 #include <string>
@@ -23,17 +27,91 @@ using namespace klee;
 
 /***/
 
+static int getOperandNum(
+    Value *v,
+    const std::unordered_map<Instruction *, unsigned> &instructionToRegisterMap,
+    KModule *km, KInstruction *ki) {
+  if (Instruction *inst = dyn_cast<Instruction>(v)) {
+    return instructionToRegisterMap.at(inst);
+  } else if (Argument *a = dyn_cast<Argument>(v)) {
+    return a->getArgNo();
+  } else if (isa<BasicBlock>(v) || isa<InlineAsm>(v) ||
+             isa<MetadataAsValue>(v)) {
+    return -1;
+  } else {
+    assert(isa<Constant>(v));
+    Constant *c = cast<Constant>(v);
+    return -(km->getConstantID(c, ki) + 2);
+  }
+}
+
+KInstruction::KInstruction(
+    const std::unordered_map<llvm::Instruction *, unsigned>
+        &_instructionToRegisterMap,
+    llvm::Instruction *_inst, KModule *_km, KBlock *_kb,
+    unsigned &_globalIndexInc)
+    : inst(_inst), parent(_kb), globalIndex(_globalIndexInc++) {
+  if (isa<llvm::CallInst>(inst) || isa<llvm::InvokeInst>(inst)) {
+    const llvm::CallBase &cs = cast<llvm::CallBase>(*inst);
+    Value *val = cs.getCalledOperand();
+    unsigned numArgs = cs.arg_size();
+    operands = new int[numArgs + 1];
+    operands[0] = getOperandNum(val, _instructionToRegisterMap, _km, this);
+    for (unsigned j = 0; j < numArgs; j++) {
+      Value *v = cs.getArgOperand(j);
+      operands[j + 1] = getOperandNum(v, _instructionToRegisterMap, _km, this);
+    }
+  } else {
+    unsigned numOperands = inst->getNumOperands();
+    operands = new int[numOperands];
+    for (unsigned j = 0; j < numOperands; j++) {
+      Value *v = inst->getOperand(j);
+      operands[j] = getOperandNum(v, _instructionToRegisterMap, _km, this);
+    }
+  }
+}
+
 KInstruction::~KInstruction() { delete[] operands; }
 
-std::string KInstruction::getSourceLocation() const {
-  if (!info->file.empty())
-    return info->file + ":" + std::to_string(info->line) + " " +
-           std::to_string(info->column);
-  else
+size_t KInstruction::getLine() const {
+  auto locationInfo = getLocationInfo(inst);
+  return locationInfo.line;
+}
+
+size_t KInstruction::getColumn() const {
+  auto locationInfo = getLocationInfo(inst);
+  return locationInfo.column;
+}
+
+std::string KInstruction::getSourceFilepath() const {
+  auto locationInfo = getLocationInfo(inst);
+  return locationInfo.file;
+}
+
+std::string KInstruction::getSourceLocationString() const {
+  std::string filePath = getSourceFilepath();
+  if (!filePath.empty()) {
+    // TODO change format to file:line:column
+    return filePath + ":" + std::to_string(getLine()) + " " +
+           std::to_string(getColumn());
+  } else {
     return "[no debug info]";
+  }
 }
 
 std::string KInstruction::toString() const {
-  return llvm::utostr(index) + " at " + parent->toString() + " (" +
+  return llvm::utostr(getIndex()) + " at " + parent->toString() + " (" +
          inst->getOpcodeName() + ")";
 }
+
+unsigned KInstruction::getGlobalIndex() const { return globalIndex; }
+
+unsigned KInstruction::getIndex() const {
+  return getGlobalIndex() - getKFunction()->getGlobalIndex() -
+         getKBlock()->getId() - 1;
+}
+
+unsigned KInstruction::getDest() const {
+  return parent->parent->getNumArgs() + getIndex() +
+         (parent->instructions - parent->parent->instructions);
+}
diff --git a/lib/Module/KModule.cpp b/lib/Module/KModule.cpp
index 2ab1059a8f..7bfb8433f3 100644
--- a/lib/Module/KModule.cpp
+++ b/lib/Module/KModule.cpp
@@ -14,9 +14,9 @@
 #include "klee/Config/Version.h"
 #include "klee/Core/Interpreter.h"
 #include "klee/Module/Cell.h"
-#include "klee/Module/InstructionInfoTable.h"
 #include "klee/Module/KInstruction.h"
 #include "klee/Module/KModule.h"
+#include "klee/Module/LocationInfo.h"
 #include "klee/Support/Debug.h"
 #include "klee/Support/ErrorHandling.h"
 #include "klee/Support/ModuleUtil.h"
@@ -26,6 +26,7 @@
 DISABLE_WARNING_PUSH
 DISABLE_WARNING_DEPRECATED_DECLARATIONS
 #include "llvm/Bitcode/BitcodeWriter.h"
+#include "llvm/IR/AssemblyAnnotationWriter.h"
 #include "llvm/IR/DataLayout.h"
 #include "llvm/IR/Function.h"
 #include "llvm/IR/IRBuilder.h"
@@ -37,6 +38,7 @@ DISABLE_WARNING_DEPRECATED_DECLARATIONS
 #include "llvm/IR/Verifier.h"
 #include "llvm/Linker/Linker.h"
 #include "llvm/Support/CommandLine.h"
+#include "llvm/Support/FormattedStream.h"
 #include "llvm/Support/Path.h"
 #include "llvm/Support/raw_os_ostream.h"
 #include "llvm/Support/raw_ostream.h"
@@ -46,7 +48,9 @@ DISABLE_WARNING_DEPRECATED_DECLARATIONS
 #include "llvm/Transforms/Utils/Cloning.h"
 DISABLE_WARNING_POP
 
+#include <memory>
 #include <sstream>
+#include <utility>
 
 using namespace llvm;
 using namespace klee;
@@ -337,6 +341,38 @@ void KModule::optimiseAndPrepare(
   pm3.run(*module);
 }
 
+class InstructionToLineAnnotator : public llvm::AssemblyAnnotationWriter {
+private:
+  std::unordered_map<uintptr_t, uint64_t> mapping = {};
+
+public:
+  void emitInstructionAnnot(const llvm::Instruction *i,
+                            llvm::formatted_raw_ostream &os) override {
+    os.flush();
+    mapping.emplace(reinterpret_cast<std::uintptr_t>(i), os.getLine() + 1);
+  }
+
+  void emitFunctionAnnot(const llvm::Function *f,
+                         llvm::formatted_raw_ostream &os) override {
+    os.flush();
+    mapping.emplace(reinterpret_cast<std::uintptr_t>(f), os.getLine() + 1);
+  }
+
+  std::unordered_map<uintptr_t, uint64_t> getMapping() const { return mapping; }
+};
+
+static std::unordered_map<uintptr_t, uint64_t>
+buildInstructionToLineMap(const llvm::Module &m,
+                          std::unique_ptr<llvm::raw_fd_ostream> assemblyFS) {
+
+  InstructionToLineAnnotator a;
+
+  m.print(*assemblyFS, &a);
+  assemblyFS->flush();
+
+  return a.getMapping();
+}
+
 void KModule::manifest(InterpreterHandler *ih,
                        Interpreter::GuidanceKind guidance,
                        bool forceSourceOutput) {
@@ -351,32 +387,21 @@ void KModule::manifest(InterpreterHandler *ih,
     std::unique_ptr<llvm::raw_fd_ostream> assemblyFS;
     if (OutputSource || forceSourceOutput) {
       assemblyFS = ih->openOutputFile("assembly.ll");
+      asmLineMap = buildInstructionToLineMap(*module, std::move(assemblyFS));
     }
-    infos =
-        std::make_unique<InstructionInfoTable>(*module, std::move(assemblyFS));
   }
 
   std::vector<Function *> declarations;
 
   unsigned functionID = 0;
+  maxGlobalIndex = 0;
   for (auto &Function : module->functions()) {
     if (Function.isDeclaration()) {
       declarations.push_back(&Function);
     }
 
-    auto kf = std::unique_ptr<KFunction>(new KFunction(&Function, this));
-
-    llvm::Function *function = &Function;
-    for (auto &BasicBlock : *function) {
-      unsigned numInstructions = kf->blockMap[&BasicBlock]->numInstructions;
-      KBlock *kb = kf->blockMap[&BasicBlock];
-      for (unsigned i = 0; i < numInstructions; ++i) {
-        KInstruction *ki = kb->instructions[i];
-        ki->info = &infos->getInfo(*ki->inst);
-      }
-    }
+    auto kf = std::make_unique<KFunction>(&Function, this, maxGlobalIndex);
 
-    functionIDMap.insert({&Function, functionID});
     kf->id = functionID;
     functionID++;
     functionNameMap.insert({kf->getName().str(), kf.get()});
@@ -426,6 +451,19 @@ void KModule::manifest(InterpreterHandler *ih,
   }
 }
 
+std::optional<size_t> KModule::getAsmLine(const uintptr_t ref) const {
+  if (!asmLineMap.empty()) {
+    return asmLineMap.at(ref);
+  }
+  return std::nullopt;
+}
+std::optional<size_t> KModule::getAsmLine(const llvm::Function *func) const {
+  return getAsmLine(reinterpret_cast<std::uintptr_t>(func));
+}
+std::optional<size_t> KModule::getAsmLine(const llvm::Instruction *inst) const {
+  return getAsmLine(reinterpret_cast<std::uintptr_t>(inst));
+}
+
 void KModule::checkModule() {
   InstructionOperandTypeCheckPass *operandTypeCheckPass =
       new InstructionOperandTypeCheckPass();
@@ -502,6 +540,18 @@ unsigned KModule::getConstantID(Constant *c, KInstruction *ki) {
   return id;
 }
 
+unsigned KModule::getFunctionId(const llvm::Function *func) const {
+  return functionMap.at(func)->id;
+}
+unsigned KModule::getGlobalIndex(const llvm::Function *func) const {
+  return functionMap.at(func)->getGlobalIndex();
+}
+unsigned KModule::getGlobalIndex(const llvm::Instruction *inst) const {
+  return functionMap.at(inst->getFunction())
+      ->instructionMap.at(inst)
+      ->getGlobalIndex();
+}
+
 /***/
 
 KConstant::KConstant(llvm::Constant *_ct, unsigned _id, KInstruction *_ki) {
@@ -510,76 +560,25 @@ KConstant::KConstant(llvm::Constant *_ct, unsigned _id, KInstruction *_ki) {
   ki = _ki;
 }
 
-/***/
-
-static int getOperandNum(
-    Value *v,
-    std::unordered_map<Instruction *, unsigned> &instructionToRegisterMap,
-    KModule *km, KInstruction *ki) {
-  if (Instruction *inst = dyn_cast<Instruction>(v)) {
-    return instructionToRegisterMap[inst];
-  } else if (Argument *a = dyn_cast<Argument>(v)) {
-    return a->getArgNo();
-  } else if (isa<BasicBlock>(v) || isa<InlineAsm>(v) ||
-             isa<MetadataAsValue>(v)) {
-    return -1;
-  } else {
-    assert(isa<Constant>(v));
-    Constant *c = cast<Constant>(v);
-    return -(km->getConstantID(c, ki) + 2);
-  }
-}
-
-void KBlock::handleKInstruction(
-    std::unordered_map<Instruction *, unsigned> &instructionToRegisterMap,
-    llvm::Instruction *inst, KModule *km, KInstruction *ki) {
-  ki->parent = this;
-  ki->inst = inst;
-  ki->dest = instructionToRegisterMap[inst];
-  if (isa<CallInst>(inst) || isa<InvokeInst>(inst)) {
-    const CallBase &cs = cast<CallBase>(*inst);
-    Value *val = cs.getCalledOperand();
-    unsigned numArgs = cs.arg_size();
-    ki->operands = new int[numArgs + 1];
-    ki->operands[0] = getOperandNum(val, instructionToRegisterMap, km, ki);
-    for (unsigned j = 0; j < numArgs; j++) {
-      Value *v = cs.getArgOperand(j);
-      ki->operands[j + 1] = getOperandNum(v, instructionToRegisterMap, km, ki);
-    }
-  } else {
-    unsigned numOperands = inst->getNumOperands();
-    ki->operands = new int[numOperands];
-    for (unsigned j = 0; j < numOperands; j++) {
-      Value *v = inst->getOperand(j);
-      ki->operands[j] = getOperandNum(v, instructionToRegisterMap, km, ki);
-    }
-  }
-}
-
-KFunction::KFunction(llvm::Function *_function, KModule *_km)
-    : KCallable(CK_Function), parent(_km), function(_function),
-      numArgs(function->arg_size()), numInstructions(0), numBlocks(0),
-      entryKBlock(nullptr), trackCoverage(true) {
+KFunction::KFunction(llvm::Function *_function, KModule *_km,
+                     unsigned &globalIndexInc)
+    : KCallable(CK_Function), globalIndex(globalIndexInc++), parent(_km),
+      function(_function), entryKBlock(nullptr), numInstructions(0) {
   for (auto &BasicBlock : *function) {
     numInstructions += BasicBlock.size();
-    numBlocks++;
   }
   instructions = new KInstruction *[numInstructions];
   std::unordered_map<Instruction *, unsigned> instructionToRegisterMap;
   // Assign unique instruction IDs to each basic block
   unsigned n = 0;
   // The first arg_size() registers are reserved for formals.
-  unsigned rnum = numArgs;
-  for (llvm::Function::iterator bbit = function->begin(),
-                                bbie = function->end();
-       bbit != bbie; ++bbit) {
-    for (llvm::BasicBlock::iterator it = bbit->begin(), ie = bbit->end();
-         it != ie; ++it)
-      instructionToRegisterMap[&*it] = rnum++;
+  unsigned rnum = getNumArgs();
+  for (auto &bb : *function) {
+    for (auto &instr : bb) {
+      instructionToRegisterMap[&instr] = rnum++;
+    }
   }
-  numRegisters = rnum;
 
-  unsigned blockID = 0;
   for (llvm::Function::iterator bbit = function->begin(),
                                 bbie = function->end();
        bbit != bbie; ++bbit) {
@@ -594,32 +593,42 @@ KFunction::KFunction(llvm::Function *_function, KModule *_km)
       if (f) {
         calledFunctions.insert(f);
       }
-      KCallBlock *ckb = new KCallBlock(
-          this, &*bbit, parent, instructionToRegisterMap,
-          registerToInstructionMap, calledFunctions, &instructions[n]);
+      auto *ckb =
+          new KCallBlock(this, &*bbit, parent, instructionToRegisterMap,
+                         calledFunctions, &instructions[n], globalIndexInc);
       kCallBlocks.push_back(ckb);
       kb = ckb;
     } else if (SplitReturns && isa<ReturnInst>(lit)) {
       kb = new KReturnBlock(this, &*bbit, parent, instructionToRegisterMap,
-                            registerToInstructionMap, &instructions[n]);
+                            &instructions[n], globalIndexInc);
       returnKBlocks.push_back(kb);
-    } else
+    } else {
       kb = new KBlock(this, &*bbit, parent, instructionToRegisterMap,
-                      registerToInstructionMap, &instructions[n]);
+                      &instructions[n], globalIndexInc);
+    }
     for (unsigned i = 0; i < kb->numInstructions; i++, n++) {
       instructionMap[instructions[n]->inst] = instructions[n];
     }
-    kb->id = blockID++;
     blockMap[&*bbit] = kb;
     blocks.push_back(std::unique_ptr<KBlock>(kb));
   }
 
-  if (numBlocks > 0) {
+  if (blocks.size() > 0) {
     assert(function->begin() != function->end());
     entryKBlock = blockMap[&*function->begin()];
   }
 }
 
+size_t KFunction::getLine() const {
+  auto locationInfo = getLocationInfo(function);
+  return locationInfo.line;
+}
+
+std::string KFunction::getSourceFilepath() const {
+  auto locationInfo = getLocationInfo(function);
+  return locationInfo.file;
+}
+
 KFunction::~KFunction() {
   for (unsigned i = 0; i < numInstructions; ++i)
     delete instructions[i];
@@ -628,47 +637,40 @@ KFunction::~KFunction() {
 
 KBlock::KBlock(
     KFunction *_kfunction, llvm::BasicBlock *block, KModule *km,
-    std::unordered_map<Instruction *, unsigned> &instructionToRegisterMap,
-    std::unordered_map<unsigned, KInstruction *> &registerToInstructionMap,
-    KInstruction **instructionsKF)
-    : parent(_kfunction), basicBlock(block), numInstructions(0),
-      trackCoverage(true) {
+    const std::unordered_map<Instruction *, unsigned> &instructionToRegisterMap,
+    KInstruction **instructionsKF, unsigned &globalIndexInc)
+    : parent(_kfunction), basicBlock(block), numInstructions(0) {
   numInstructions += block->size();
   instructions = instructionsKF;
 
-  unsigned i = 0;
-  for (llvm::BasicBlock::iterator it = block->begin(), ie = block->end();
-       it != ie; ++it) {
+  for (auto &it : *block) {
     KInstruction *ki;
 
-    switch (it->getOpcode()) {
+    switch (it.getOpcode()) {
     case Instruction::GetElementPtr:
     case Instruction::InsertValue:
     case Instruction::ExtractValue:
-      ki = new KGEPInstruction();
+      ki = new KGEPInstruction(instructionToRegisterMap, &it, km, this,
+                               globalIndexInc);
       break;
     default:
-      ki = new KInstruction();
+      ki = new KInstruction(instructionToRegisterMap, &it, km, this,
+                            globalIndexInc);
       break;
     }
-
-    Instruction *inst = &*it;
-    handleKInstruction(instructionToRegisterMap, inst, km, ki);
-    ki->index = i;
-    instructions[i++] = ki;
-    registerToInstructionMap[instructionToRegisterMap[&*it]] = ki;
+    instructions[ki->getIndex()] = ki;
   }
 }
 
 KCallBlock::KCallBlock(
     KFunction *_kfunction, llvm::BasicBlock *block, KModule *km,
-    std::unordered_map<Instruction *, unsigned> &instructionToRegisterMap,
-    std::unordered_map<unsigned, KInstruction *> &registerToInstructionMap,
-    std::set<llvm::Function *> _calledFunctions, KInstruction **instructionsKF)
+    const std::unordered_map<Instruction *, unsigned> &instructionToRegisterMap,
+    std::set<llvm::Function *> _calledFunctions, KInstruction **instructionsKF,
+    unsigned &globalIndexInc)
     : KBlock::KBlock(_kfunction, block, km, instructionToRegisterMap,
-                     registerToInstructionMap, instructionsKF),
+                     instructionsKF, globalIndexInc),
       kcallInstruction(this->instructions[0]),
-      calledFunctions(_calledFunctions) {}
+      calledFunctions(std::move(_calledFunctions)) {}
 
 bool KCallBlock::intrinsic() const {
   if (calledFunctions.size() != 1) {
@@ -695,11 +697,10 @@ KFunction *KCallBlock::getKFunction() const {
 
 KReturnBlock::KReturnBlock(
     KFunction *_kfunction, llvm::BasicBlock *block, KModule *km,
-    std::unordered_map<Instruction *, unsigned> &instructionToRegisterMap,
-    std::unordered_map<unsigned, KInstruction *> &registerToInstructionMap,
-    KInstruction **instructionsKF)
+    const std::unordered_map<Instruction *, unsigned> &instructionToRegisterMap,
+    KInstruction **instructionsKF, unsigned &globalIndexInc)
     : KBlock::KBlock(_kfunction, block, km, instructionToRegisterMap,
-                     registerToInstructionMap, instructionsKF) {}
+                     instructionsKF, globalIndexInc) {}
 
 std::string KBlock::getLabel() const {
   std::string _label;
@@ -712,3 +713,13 @@ std::string KBlock::getLabel() const {
 std::string KBlock::toString() const {
   return getLabel() + " in function " + parent->function->getName().str();
 }
+
+uintptr_t KBlock::getId() const { return instructions - parent->instructions; }
+
+KInstruction *KFunction::getInstructionByRegister(size_t reg) const {
+  return instructions[reg - function->arg_size()];
+}
+size_t KFunction::getNumArgs() const { return function->arg_size(); }
+size_t KFunction::getNumRegisters() const {
+  return function->arg_size() + numInstructions;
+}
diff --git a/lib/Module/LocationInfo.cpp b/lib/Module/LocationInfo.cpp
new file mode 100644
index 0000000000..274a55e25d
--- /dev/null
+++ b/lib/Module/LocationInfo.cpp
@@ -0,0 +1,63 @@
+//===-- LocationInfo.cpp ------------------------------------------===//
+//
+//                     The KLEE Symbolic Virtual Machine
+//
+// This file is distributed under the University of Illinois Open Source
+// License. See LICENSE.TXT for details.
+//
+//===----------------------------------------------------------------------===//
+
+#include "klee/Module/LocationInfo.h"
+#include "klee/Support/CompilerWarning.h"
+
+DISABLE_WARNING_PUSH
+DISABLE_WARNING_DEPRECATED_DECLARATIONS
+#include "llvm/Analysis/ValueTracking.h"
+#include "llvm/IR/AssemblyAnnotationWriter.h"
+#include "llvm/IR/DebugInfoMetadata.h"
+#include "llvm/IR/Function.h"
+#include "llvm/IR/Instructions.h"
+#include "llvm/IR/LLVMContext.h"
+#include "llvm/IR/Module.h"
+#include "llvm/Support/FormattedStream.h"
+DISABLE_WARNING_POP
+
+namespace klee {
+
+LocationInfo getLocationInfo(const llvm::Function *func) {
+  const auto dsub = func->getSubprogram();
+
+  if (dsub != nullptr) {
+    auto path = dsub->getFilename();
+    return {path.str(), dsub->getLine(), 0}; // TODO why not use column here?
+  }
+
+  return {"", 0, 0};
+}
+
+LocationInfo getLocationInfo(const llvm::Instruction *inst) {
+  // Retrieve debug information associated with instruction
+  const auto &dl = inst->getDebugLoc();
+
+  // Check if a valid debug location is assigned to the instruction.
+  if (dl.get() != nullptr) {
+    auto full_path = dl->getFilename();
+    auto line = dl.getLine();
+    auto column = dl.getCol();
+
+    // Still, if the line is unknown, take the context of the instruction to
+    // narrow it down
+    if (line == 0) {
+      if (auto LexicalBlock =
+              llvm::dyn_cast<llvm::DILexicalBlock>(dl.getScope())) {
+        line = LexicalBlock->getLine();
+        column = LexicalBlock->getColumn();
+      }
+    }
+    return {full_path.str(), line, column};
+  }
+
+  return getLocationInfo(inst->getParent()->getParent());
+}
+
+} // namespace klee
diff --git a/lib/Module/SarifReport.cpp b/lib/Module/SarifReport.cpp
index 075ce32417..3923d32ead 100644
--- a/lib/Module/SarifReport.cpp
+++ b/lib/Module/SarifReport.cpp
@@ -326,20 +326,22 @@ bool Location::isInside(const std::string &name) const {
 }
 
 bool Location::isInside(KBlock *block, const Instructions &origInsts) const {
-  auto first = block->getFirstInstruction()->info;
-  auto last = block->getLastInstruction()->info;
+  auto first = block->getFirstInstruction();
+  auto last = block->getLastInstruction();
   if (!startColumn.has_value()) {
-    if (first->line > endLine)
+    if (first->getLine() > endLine)
       return false;
-    return startLine <= last->line; // and `first <= line` from above
+    return startLine <= last->getLine(); // and `first <= line` from above
   } else {
     for (size_t i = 0; i < block->numInstructions; ++i) {
-      auto inst = block->instructions[i]->info;
+      auto inst = block->instructions[i];
       auto opCode = block->instructions[i]->inst->getOpcode();
       if (!isa<DbgInfoIntrinsic>(block->instructions[i]->inst) &&
-          inst->line <= endLine && inst->line >= startLine &&
-          inst->column <= *endColumn && inst->column >= *startColumn &&
-          origInsts.at(inst->line).at(inst->column).count(opCode) != 0) {
+          inst->getLine() <= endLine && inst->getLine() >= startLine &&
+          inst->getColumn() <= *endColumn &&
+          inst->getColumn() >= *startColumn &&
+          origInsts.at(inst->getLine()).at(inst->getColumn()).count(opCode) !=
+              0) {
         return true;
       }
     }
diff --git a/lib/Module/Target.cpp b/lib/Module/Target.cpp
index 7e6cfab36d..d2dde07919 100644
--- a/lib/Module/Target.cpp
+++ b/lib/Module/Target.cpp
@@ -31,8 +31,8 @@ ErrorLocation::ErrorLocation(const klee::ref<klee::Location> &loc)
       startColumn(loc->startColumn), endColumn(loc->endColumn) {}
 
 ErrorLocation::ErrorLocation(const KInstruction *ki) {
-  startLine = (endLine = ki->info->line);
-  startColumn = (endColumn = ki->info->line);
+  startLine = (endLine = ki->getLine());
+  startColumn = (endColumn = ki->getLine());
 }
 
 std::string ReproduceErrorTarget::toString() const {
@@ -102,11 +102,11 @@ ref<Target> CoverBranchTarget::create(KBlock *_block, unsigned _branchCase) {
 
 bool ReproduceErrorTarget::isTheSameAsIn(const KInstruction *instr) const {
   const auto &errLoc = loc;
-  return instr->info->line >= errLoc.startLine &&
-         instr->info->line <= errLoc.endLine &&
+  return instr->getLine() >= errLoc.startLine &&
+         instr->getLine() <= errLoc.endLine &&
          (!LocationAccuracy || !errLoc.startColumn.has_value() ||
-          (instr->info->column >= *errLoc.startColumn &&
-           instr->info->column <= *errLoc.endColumn));
+          (instr->getColumn() >= *errLoc.startColumn &&
+           instr->getColumn() <= *errLoc.endColumn));
 }
 
 int Target::compare(const Target &b) const { return internalCompare(b); }
@@ -126,8 +126,8 @@ int ReachBlockTarget::internalCompare(const Target &b) const {
   if (block->parent->id != other.block->parent->id) {
     return block->parent->id < other.block->parent->id ? -1 : 1;
   }
-  if (block->id != other.block->id) {
-    return block->id < other.block->id ? -1 : 1;
+  if (block->getId() != other.block->getId()) {
+    return block->getId() < other.block->getId() ? -1 : 1;
   }
 
   if (atEnd != other.atEnd) {
@@ -146,8 +146,8 @@ int CoverBranchTarget::internalCompare(const Target &b) const {
   if (block->parent->id != other.block->parent->id) {
     return block->parent->id < other.block->parent->id ? -1 : 1;
   }
-  if (block->id != other.block->id) {
-    return block->id < other.block->id ? -1 : 1;
+  if (block->getId() != other.block->getId()) {
+    return block->getId() < other.block->getId() ? -1 : 1;
   }
 
   if (branchCase != other.branchCase) {
@@ -170,8 +170,8 @@ int ReproduceErrorTarget::internalCompare(const Target &b) const {
   if (block->parent->id != other.block->parent->id) {
     return block->parent->id < other.block->parent->id ? -1 : 1;
   }
-  if (block->id != other.block->id) {
-    return block->id < other.block->id ? -1 : 1;
+  if (block->getId() != other.block->getId()) {
+    return block->getId() < other.block->getId() ? -1 : 1;
   }
 
   if (errors.size() != other.errors.size()) {
diff --git a/test/regression/2023-10-04-email_spec0_product16.cil.c b/test/regression/2023-10-04-email_spec0_product16.cil.c
new file mode 100644
index 0000000000..8a4acd5c58
--- /dev/null
+++ b/test/regression/2023-10-04-email_spec0_product16.cil.c
@@ -0,0 +1,2794 @@
+// REQUIRES: z3
+// 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 --use-forked-solver=false --solver-backend=z3 -max-memory=6008 --optimize --skip-not-lazy-initialized -istats-write-interval=90s -exit-on-error-type=Assert --search=dfs -max-time=10s %t1.bc 2>&1 | FileCheck -check-prefix=CHECK %s
+
+// RUN find %t.klee-out -type f -name "*.assert.err" | sed 's/assert\.err/ktest/' | xargs %ktest-tool | FileCheck -check-prefix=CHECK-TEST %s
+// CHECK-TEST-NOT: object 20
+
+#include "klee-test-comp.c"
+
+// This file is part of the SV-Benchmarks collection of verification tasks:
+// https://gitlab.com/sosy-lab/benchmarking/sv-benchmarks
+//
+// SPDX-FileCopyrightText: 2011-2013 Alexander von Rhein, University of Passau
+// SPDX-FileCopyrightText: 2011-2021 The SV-Benchmarks Community
+//
+// SPDX-License-Identifier: Apache-2.0
+
+extern void abort(void);
+extern void __assert_fail(const char *, const char *, unsigned int, const char *) __attribute__((__nothrow__, __leaf__)) __attribute__((__noreturn__));
+// CHECK: email_spec0_product16.cil.c:[[@LINE+1]]: ASSERTION FAIL: 0
+void reach_error() { __assert_fail("0", "email_spec0_product16.cil.c", 3, "reach_error"); }
+
+extern int __VERIFIER_nondet_int(void);
+/* Generated by CIL v. 1.3.7 */
+/* print_CIL_Input is true */
+
+struct JoinPoint {
+  void **(*fp)(struct JoinPoint *);
+  void **args;
+  int argsCount;
+  char const **argsType;
+  void *(*arg)(int, struct JoinPoint *);
+  char const *(*argType)(int, struct JoinPoint *);
+  void **retValue;
+  char const *retType;
+  char const *funcName;
+  char const *targetName;
+  char const *fileName;
+  char const *kind;
+  void *excep_return;
+};
+struct __UTAC__CFLOW_FUNC {
+  int (*func)(int, int);
+  int val;
+  struct __UTAC__CFLOW_FUNC *next;
+};
+struct __UTAC__EXCEPTION {
+  void *jumpbuf;
+  unsigned long long prtValue;
+  int pops;
+  struct __UTAC__CFLOW_FUNC *cflowfuncs;
+};
+typedef unsigned int size_t;
+struct __ACC__ERR {
+  void *v;
+  struct __ACC__ERR *next;
+};
+#pragma merger(0, "featureselect.i", "")
+int __SELECTED_FEATURE_Base;
+int __SELECTED_FEATURE_Keys;
+int __SELECTED_FEATURE_Encrypt;
+int __SELECTED_FEATURE_AutoResponder;
+int __SELECTED_FEATURE_AddressBook;
+int __SELECTED_FEATURE_Sign;
+int __SELECTED_FEATURE_Forward;
+int __SELECTED_FEATURE_Verify;
+int __SELECTED_FEATURE_Decrypt;
+int __GUIDSL_ROOT_PRODUCTION;
+int __GUIDSL_NON_TERMINAL_main;
+int select_one(void);
+void select_features(void);
+void select_helpers(void);
+int valid_product(void);
+int select_one(void) {
+  int retValue_acc;
+  int choice = __VERIFIER_nondet_int();
+
+  {
+    retValue_acc = choice;
+    return (retValue_acc);
+    return (retValue_acc);
+  }
+}
+void select_features(void) {
+
+  {
+    return;
+  }
+}
+void select_helpers(void) {
+
+  {
+    return;
+  }
+}
+int valid_product(void) {
+  int retValue_acc;
+
+  {
+    retValue_acc = 1;
+    return (retValue_acc);
+    return (retValue_acc);
+  }
+}
+#pragma merger(0, "Test.i", "")
+extern int printf(char const *__restrict __format, ...);
+extern int puts(char const *__s);
+void setClientPrivateKey(int handle, int value);
+int createClientKeyringEntry(int handle);
+int getClientKeyringUser(int handle, int index);
+void setClientKeyringUser(int handle, int index, int value);
+int getClientKeyringPublicKey(int handle, int index);
+void setClientKeyringPublicKey(int handle, int index, int value);
+void setClientForwardReceiver(int handle, int value);
+void setClientId(int handle, int value);
+int is_queue_empty(void);
+int get_queued_client(void);
+int get_queued_email(void);
+void outgoing(int client, int msg);
+void sendEmail(int sender, int receiver);
+void generateKeyPair(int client, int seed);
+int bob;
+int rjh;
+int chuck;
+void setup_bob(int bob___0);
+void setup_rjh(int rjh___0);
+void setup_chuck(int chuck___0);
+void bobToRjh(void);
+void rjhToBob(void);
+void test(void);
+void setup(void);
+int main(void);
+void bobKeyAdd(void);
+void bobKeyAddChuck(void);
+void rjhKeyAdd(void);
+void rjhKeyAddChuck(void);
+void chuckKeyAdd(void);
+void bobKeyChange(void);
+void rjhKeyChange(void);
+void rjhDeletePrivateKey(void);
+void chuckKeyAddRjh(void);
+void rjhEnableForwarding(void);
+void setup_bob__wrappee__Base(int bob___0) {
+
+  {
+    {
+      setClientId(bob___0, bob___0);
+    }
+    return;
+  }
+}
+void setup_bob(int bob___0) {
+
+  {
+    {
+      setup_bob__wrappee__Base(bob___0);
+      setClientPrivateKey(bob___0, 123);
+    }
+    return;
+  }
+}
+void setup_rjh__wrappee__Base(int rjh___0) {
+
+  {
+    {
+      setClientId(rjh___0, rjh___0);
+    }
+    return;
+  }
+}
+void setup_rjh(int rjh___0) {
+
+  {
+    {
+      setup_rjh__wrappee__Base(rjh___0);
+      setClientPrivateKey(rjh___0, 456);
+    }
+    return;
+  }
+}
+void setup_chuck__wrappee__Base(int chuck___0) {
+
+  {
+    {
+      setClientId(chuck___0, chuck___0);
+    }
+    return;
+  }
+}
+void setup_chuck(int chuck___0) {
+
+  {
+    {
+      setup_chuck__wrappee__Base(chuck___0);
+      setClientPrivateKey(chuck___0, 789);
+    }
+    return;
+  }
+}
+void bobToRjh(void) {
+  int tmp;
+  int tmp___0;
+  int tmp___1;
+
+  {
+    {
+      puts("Please enter a subject and a message body.\n");
+      sendEmail(bob, rjh);
+      tmp___1 = is_queue_empty();
+    }
+    if (tmp___1) {
+
+    } else {
+      {
+        tmp = get_queued_email();
+        tmp___0 = get_queued_client();
+        outgoing(tmp___0, tmp);
+      }
+    }
+    return;
+  }
+}
+void rjhToBob(void) {
+
+  {
+    {
+      puts("Please enter a subject and a message body.\n");
+      sendEmail(rjh, bob);
+    }
+    return;
+  }
+}
+void setup(void) {
+  char const *__restrict __cil_tmp1;
+  char const *__restrict __cil_tmp2;
+  char const *__restrict __cil_tmp3;
+
+  {
+    {
+      bob = 1;
+      setup_bob(bob);
+      __cil_tmp1 = (char const *__restrict)"bob: %d\n";
+      printf(__cil_tmp1, bob);
+      rjh = 2;
+      setup_rjh(rjh);
+      __cil_tmp2 = (char const *__restrict)"rjh: %d\n";
+      printf(__cil_tmp2, rjh);
+      chuck = 3;
+      setup_chuck(chuck);
+      __cil_tmp3 = (char const *__restrict)"chuck: %d\n";
+      printf(__cil_tmp3, chuck);
+    }
+    return;
+  }
+}
+int main(void) {
+  int retValue_acc;
+  int tmp;
+
+  {
+    {
+      select_helpers();
+      select_features();
+      tmp = valid_product();
+    }
+    if (tmp) {
+      {
+        setup();
+        test();
+      }
+    } else {
+    }
+    return (retValue_acc);
+  }
+}
+void bobKeyAdd(void) {
+  int tmp;
+  int tmp___0;
+  char const *__restrict __cil_tmp3;
+  char const *__restrict __cil_tmp4;
+
+  {
+    {
+      createClientKeyringEntry(bob);
+      setClientKeyringUser(bob, 0, 2);
+      setClientKeyringPublicKey(bob, 0, 456);
+      puts("bob added rjhs key");
+      tmp = getClientKeyringUser(bob, 0);
+      __cil_tmp3 = (char const *__restrict)"%d\n";
+      printf(__cil_tmp3, tmp);
+      tmp___0 = getClientKeyringPublicKey(bob, 0);
+      __cil_tmp4 = (char const *__restrict)"%d\n";
+      printf(__cil_tmp4, tmp___0);
+    }
+    return;
+  }
+}
+void rjhKeyAdd(void) {
+
+  {
+    {
+      createClientKeyringEntry(rjh);
+      setClientKeyringUser(rjh, 0, 1);
+      setClientKeyringPublicKey(rjh, 0, 123);
+    }
+    return;
+  }
+}
+void rjhKeyAddChuck(void) {
+
+  {
+    {
+      createClientKeyringEntry(rjh);
+      setClientKeyringUser(rjh, 0, 3);
+      setClientKeyringPublicKey(rjh, 0, 789);
+    }
+    return;
+  }
+}
+void bobKeyAddChuck(void) {
+
+  {
+    {
+      createClientKeyringEntry(bob);
+      setClientKeyringUser(bob, 1, 3);
+      setClientKeyringPublicKey(bob, 1, 789);
+    }
+    return;
+  }
+}
+void chuckKeyAdd(void) {
+
+  {
+    {
+      createClientKeyringEntry(chuck);
+      setClientKeyringUser(chuck, 0, 1);
+      setClientKeyringPublicKey(chuck, 0, 123);
+    }
+    return;
+  }
+}
+void chuckKeyAddRjh(void) {
+
+  {
+    {
+      createClientKeyringEntry(chuck);
+      setClientKeyringUser(chuck, 0, 2);
+      setClientKeyringPublicKey(chuck, 0, 456);
+    }
+    return;
+  }
+}
+void rjhDeletePrivateKey(void) {
+
+  {
+    {
+      setClientPrivateKey(rjh, 0);
+    }
+    return;
+  }
+}
+void bobKeyChange(void) {
+
+  {
+    {
+      generateKeyPair(bob, 777);
+    }
+    return;
+  }
+}
+void rjhKeyChange(void) {
+
+  {
+    {
+      generateKeyPair(rjh, 666);
+    }
+    return;
+  }
+}
+void rjhEnableForwarding(void) {
+
+  {
+    {
+      setClientForwardReceiver(rjh, chuck);
+    }
+    return;
+  }
+}
+#pragma merger(0, "wsllib_check.i", "")
+void __automaton_fail(void) {
+
+  {
+  ERROR : {
+    reach_error();
+    abort();
+  }
+    return;
+  }
+}
+#pragma merger(0, "Email.i", "")
+int getEmailId(int handle);
+int getEmailFrom(int handle);
+void setEmailFrom(int handle, int value);
+int getEmailTo(int handle);
+void setEmailTo(int handle, int value);
+int isEncrypted(int handle);
+int getEmailEncryptionKey(int handle);
+void printMail(int msg);
+int isReadable(int msg);
+int createEmail(int from, int to);
+int cloneEmail(int msg);
+void printMail__wrappee__Keys(int msg) {
+  int tmp;
+  int tmp___0;
+  int tmp___1;
+  int tmp___2;
+  char const *__restrict __cil_tmp6;
+  char const *__restrict __cil_tmp7;
+  char const *__restrict __cil_tmp8;
+  char const *__restrict __cil_tmp9;
+
+  {
+    {
+      tmp = getEmailId(msg);
+      __cil_tmp6 = (char const *__restrict)"ID:\n  %i\n";
+      printf(__cil_tmp6, tmp);
+      tmp___0 = getEmailFrom(msg);
+      __cil_tmp7 = (char const *__restrict)"FROM:\n  %i\n";
+      printf(__cil_tmp7, tmp___0);
+      tmp___1 = getEmailTo(msg);
+      __cil_tmp8 = (char const *__restrict)"TO:\n  %i\n";
+      printf(__cil_tmp8, tmp___1);
+      tmp___2 = isReadable(msg);
+      __cil_tmp9 = (char const *__restrict)"IS_READABLE\n  %i\n";
+      printf(__cil_tmp9, tmp___2);
+    }
+    return;
+  }
+}
+void printMail(int msg) {
+  int tmp;
+  int tmp___0;
+  char const *__restrict __cil_tmp4;
+  char const *__restrict __cil_tmp5;
+
+  {
+    {
+      printMail__wrappee__Keys(msg);
+      tmp = isEncrypted(msg);
+      __cil_tmp4 = (char const *__restrict)"ENCRYPTED\n  %d\n";
+      printf(__cil_tmp4, tmp);
+      tmp___0 = getEmailEncryptionKey(msg);
+      __cil_tmp5 = (char const *__restrict)"ENCRYPTION KEY\n  %d\n";
+      printf(__cil_tmp5, tmp___0);
+    }
+    return;
+  }
+}
+int isReadable__wrappee__Keys(int msg) {
+  int retValue_acc;
+
+  {
+    retValue_acc = 1;
+    return (retValue_acc);
+    return (retValue_acc);
+  }
+}
+int isReadable(int msg) {
+  int retValue_acc;
+  int tmp;
+
+  {
+    {
+      tmp = isEncrypted(msg);
+    }
+    if (tmp) {
+      retValue_acc = 0;
+      return (retValue_acc);
+    } else {
+      {
+        retValue_acc = isReadable__wrappee__Keys(msg);
+      }
+      return (retValue_acc);
+    }
+    return (retValue_acc);
+  }
+}
+int cloneEmail(int msg) {
+  int retValue_acc;
+
+  {
+    retValue_acc = msg;
+    return (retValue_acc);
+    return (retValue_acc);
+  }
+}
+int createEmail(int from, int to) {
+  int retValue_acc;
+  int msg;
+
+  {
+    {
+      msg = 1;
+      setEmailFrom(msg, from);
+      setEmailTo(msg, to);
+      retValue_acc = msg;
+    }
+    return (retValue_acc);
+    return (retValue_acc);
+  }
+}
+#pragma merger(0, "scenario.i", "")
+void test(void) {
+  int op1;
+  int op2;
+  int op3;
+  int op4;
+  int op5;
+  int op6;
+  int op7;
+  int op8;
+  int op9;
+  int op10;
+  int op11;
+  int splverifierCounter;
+  int tmp;
+  int tmp___0;
+  int tmp___1;
+  int tmp___2;
+  int tmp___3;
+  int tmp___4;
+  int tmp___5;
+  int tmp___6;
+  int tmp___7;
+  int tmp___8;
+  int tmp___9;
+
+  {
+    op1 = 0;
+    op2 = 0;
+    op3 = 0;
+    op4 = 0;
+    op5 = 0;
+    op6 = 0;
+    op7 = 0;
+    op8 = 0;
+    op9 = 0;
+    op10 = 0;
+    op11 = 0;
+    splverifierCounter = 0;
+    {
+      while (1) {
+      while_0_continue: /* CIL Label */;
+        if (splverifierCounter < 4) {
+
+        } else {
+          goto while_0_break;
+        }
+        splverifierCounter = splverifierCounter + 1;
+        if (!op1) {
+          {
+            tmp___9 = __VERIFIER_nondet_int();
+          }
+          if (tmp___9) {
+            {
+              bobKeyAdd();
+              op1 = 1;
+            }
+          } else {
+            goto _L___8;
+          }
+        } else {
+        _L___8: /* CIL Label */
+          if (!op2) {
+            {
+              tmp___8 = __VERIFIER_nondet_int();
+            }
+            if (tmp___8) {
+              op2 = 1;
+            } else {
+              goto _L___7;
+            }
+          } else {
+          _L___7: /* CIL Label */
+            if (!op3) {
+              {
+                tmp___7 = __VERIFIER_nondet_int();
+              }
+              if (tmp___7) {
+                {
+                  rjhDeletePrivateKey();
+                  op3 = 1;
+                }
+              } else {
+                goto _L___6;
+              }
+            } else {
+            _L___6: /* CIL Label */
+              if (!op4) {
+                {
+                  tmp___6 = __VERIFIER_nondet_int();
+                }
+                if (tmp___6) {
+                  {
+                    rjhKeyAdd();
+                    op4 = 1;
+                  }
+                } else {
+                  goto _L___5;
+                }
+              } else {
+              _L___5: /* CIL Label */
+                if (!op5) {
+                  {
+                    tmp___5 = __VERIFIER_nondet_int();
+                  }
+                  if (tmp___5) {
+                    {
+                      chuckKeyAddRjh();
+                      op5 = 1;
+                    }
+                  } else {
+                    goto _L___4;
+                  }
+                } else {
+                _L___4: /* CIL Label */
+                  if (!op6) {
+                    {
+                      tmp___4 = __VERIFIER_nondet_int();
+                    }
+                    if (tmp___4) {
+                      {
+                        rjhEnableForwarding();
+                        op6 = 1;
+                      }
+                    } else {
+                      goto _L___3;
+                    }
+                  } else {
+                  _L___3: /* CIL Label */
+                    if (!op7) {
+                      {
+                        tmp___3 = __VERIFIER_nondet_int();
+                      }
+                      if (tmp___3) {
+                        {
+                          rjhKeyChange();
+                          op7 = 1;
+                        }
+                      } else {
+                        goto _L___2;
+                      }
+                    } else {
+                    _L___2: /* CIL Label */
+                      if (!op8) {
+                        {
+                          tmp___2 = __VERIFIER_nondet_int();
+                        }
+                        if (tmp___2) {
+                          op8 = 1;
+                        } else {
+                          goto _L___1;
+                        }
+                      } else {
+                      _L___1: /* CIL Label */
+                        if (!op9) {
+                          {
+                            tmp___1 = __VERIFIER_nondet_int();
+                          }
+                          if (tmp___1) {
+                            {
+                              chuckKeyAdd();
+                              op9 = 1;
+                            }
+                          } else {
+                            goto _L___0;
+                          }
+                        } else {
+                        _L___0: /* CIL Label */
+                          if (!op10) {
+                            {
+                              tmp___0 = __VERIFIER_nondet_int();
+                            }
+                            if (tmp___0) {
+                              {
+                                bobKeyChange();
+                                op10 = 1;
+                              }
+                            } else {
+                              goto _L;
+                            }
+                          } else {
+                          _L: /* CIL Label */
+                            if (!op11) {
+                              {
+                                tmp = __VERIFIER_nondet_int();
+                              }
+                              if (tmp) {
+                                {
+                                  chuckKeyAdd();
+                                  op11 = 1;
+                                }
+                              } else {
+                                goto while_0_break;
+                              }
+                            } else {
+                              goto while_0_break;
+                            }
+                          }
+                        }
+                      }
+                    }
+                  }
+                }
+              }
+            }
+          }
+        }
+      }
+    while_0_break: /* CIL Label */;
+    }
+    {
+      bobToRjh();
+    }
+    return;
+  }
+}
+#pragma merger(0, "libacc.i", "")
+extern __attribute__((__nothrow__, __noreturn__)) void __assert_fail(char const *__assertion,
+                                                                     char const *__file,
+                                                                     unsigned int __line,
+                                                                     char const *__function);
+extern __attribute__((__nothrow__)) void *malloc(size_t __size) __attribute__((__malloc__));
+extern __attribute__((__nothrow__)) void free(void *__ptr);
+void __utac__exception__cf_handler_set(void *exception, int (*cflow_func)(int, int),
+                                       int val) {
+  struct __UTAC__EXCEPTION *excep;
+  struct __UTAC__CFLOW_FUNC *cf;
+  void *tmp;
+  unsigned long __cil_tmp7;
+  unsigned long __cil_tmp8;
+  unsigned long __cil_tmp9;
+  unsigned long __cil_tmp10;
+  unsigned long __cil_tmp11;
+  unsigned long __cil_tmp12;
+  unsigned long __cil_tmp13;
+  unsigned long __cil_tmp14;
+  int (**mem_15)(int, int);
+  int *mem_16;
+  struct __UTAC__CFLOW_FUNC **mem_17;
+  struct __UTAC__CFLOW_FUNC **mem_18;
+  struct __UTAC__CFLOW_FUNC **mem_19;
+
+  {
+    {
+      excep = (struct __UTAC__EXCEPTION *)exception;
+      tmp = malloc(24UL);
+      cf = (struct __UTAC__CFLOW_FUNC *)tmp;
+      mem_15 = (int (**)(int, int))cf;
+      *mem_15 = cflow_func;
+      __cil_tmp7 = (unsigned long)cf;
+      __cil_tmp8 = __cil_tmp7 + 8;
+      mem_16 = (int *)__cil_tmp8;
+      *mem_16 = val;
+      __cil_tmp9 = (unsigned long)cf;
+      __cil_tmp10 = __cil_tmp9 + 16;
+      __cil_tmp11 = (unsigned long)excep;
+      __cil_tmp12 = __cil_tmp11 + 24;
+      mem_17 = (struct __UTAC__CFLOW_FUNC **)__cil_tmp10;
+      mem_18 = (struct __UTAC__CFLOW_FUNC **)__cil_tmp12;
+      *mem_17 = *mem_18;
+      __cil_tmp13 = (unsigned long)excep;
+      __cil_tmp14 = __cil_tmp13 + 24;
+      mem_19 = (struct __UTAC__CFLOW_FUNC **)__cil_tmp14;
+      *mem_19 = cf;
+    }
+    return;
+  }
+}
+void __utac__exception__cf_handler_free(void *exception) {
+  struct __UTAC__EXCEPTION *excep;
+  struct __UTAC__CFLOW_FUNC *cf;
+  struct __UTAC__CFLOW_FUNC *tmp;
+  unsigned long __cil_tmp5;
+  unsigned long __cil_tmp6;
+  struct __UTAC__CFLOW_FUNC *__cil_tmp7;
+  unsigned long __cil_tmp8;
+  unsigned long __cil_tmp9;
+  unsigned long __cil_tmp10;
+  unsigned long __cil_tmp11;
+  void *__cil_tmp12;
+  unsigned long __cil_tmp13;
+  unsigned long __cil_tmp14;
+  struct __UTAC__CFLOW_FUNC **mem_15;
+  struct __UTAC__CFLOW_FUNC **mem_16;
+  struct __UTAC__CFLOW_FUNC **mem_17;
+
+  {
+    excep = (struct __UTAC__EXCEPTION *)exception;
+    __cil_tmp5 = (unsigned long)excep;
+    __cil_tmp6 = __cil_tmp5 + 24;
+    mem_15 = (struct __UTAC__CFLOW_FUNC **)__cil_tmp6;
+    cf = *mem_15;
+    {
+      while (1) {
+      while_1_continue: /* CIL Label */;
+        {
+          __cil_tmp7 = (struct __UTAC__CFLOW_FUNC *)0;
+          __cil_tmp8 = (unsigned long)__cil_tmp7;
+          __cil_tmp9 = (unsigned long)cf;
+          if (__cil_tmp9 != __cil_tmp8) {
+
+          } else {
+            goto while_1_break;
+          }
+        }
+        {
+          tmp = cf;
+          __cil_tmp10 = (unsigned long)cf;
+          __cil_tmp11 = __cil_tmp10 + 16;
+          mem_16 = (struct __UTAC__CFLOW_FUNC **)__cil_tmp11;
+          cf = *mem_16;
+          __cil_tmp12 = (void *)tmp;
+          free(__cil_tmp12);
+        }
+      }
+    while_1_break: /* CIL Label */;
+    }
+    __cil_tmp13 = (unsigned long)excep;
+    __cil_tmp14 = __cil_tmp13 + 24;
+    mem_17 = (struct __UTAC__CFLOW_FUNC **)__cil_tmp14;
+    *mem_17 = (struct __UTAC__CFLOW_FUNC *)0;
+    return;
+  }
+}
+void __utac__exception__cf_handler_reset(void *exception) {
+  struct __UTAC__EXCEPTION *excep;
+  struct __UTAC__CFLOW_FUNC *cf;
+  unsigned long __cil_tmp5;
+  unsigned long __cil_tmp6;
+  struct __UTAC__CFLOW_FUNC *__cil_tmp7;
+  unsigned long __cil_tmp8;
+  unsigned long __cil_tmp9;
+  int (*__cil_tmp10)(int, int);
+  unsigned long __cil_tmp11;
+  unsigned long __cil_tmp12;
+  int __cil_tmp13;
+  unsigned long __cil_tmp14;
+  unsigned long __cil_tmp15;
+  struct __UTAC__CFLOW_FUNC **mem_16;
+  int (**mem_17)(int, int);
+  int *mem_18;
+  struct __UTAC__CFLOW_FUNC **mem_19;
+
+  {
+    excep = (struct __UTAC__EXCEPTION *)exception;
+    __cil_tmp5 = (unsigned long)excep;
+    __cil_tmp6 = __cil_tmp5 + 24;
+    mem_16 = (struct __UTAC__CFLOW_FUNC **)__cil_tmp6;
+    cf = *mem_16;
+    {
+      while (1) {
+      while_2_continue: /* CIL Label */;
+        {
+          __cil_tmp7 = (struct __UTAC__CFLOW_FUNC *)0;
+          __cil_tmp8 = (unsigned long)__cil_tmp7;
+          __cil_tmp9 = (unsigned long)cf;
+          if (__cil_tmp9 != __cil_tmp8) {
+
+          } else {
+            goto while_2_break;
+          }
+        }
+        {
+          mem_17 = (int (**)(int, int))cf;
+          __cil_tmp10 = *mem_17;
+          __cil_tmp11 = (unsigned long)cf;
+          __cil_tmp12 = __cil_tmp11 + 8;
+          mem_18 = (int *)__cil_tmp12;
+          __cil_tmp13 = *mem_18;
+          (*__cil_tmp10)(4, __cil_tmp13);
+          __cil_tmp14 = (unsigned long)cf;
+          __cil_tmp15 = __cil_tmp14 + 16;
+          mem_19 = (struct __UTAC__CFLOW_FUNC **)__cil_tmp15;
+          cf = *mem_19;
+        }
+      }
+    while_2_break: /* CIL Label */;
+    }
+    {
+      __utac__exception__cf_handler_free(exception);
+    }
+    return;
+  }
+}
+void *__utac__error_stack_mgt(void *env, int mode, int count);
+static struct __ACC__ERR *head = (struct __ACC__ERR *)0;
+void *__utac__error_stack_mgt(void *env, int mode, int count) {
+  void *retValue_acc;
+  struct __ACC__ERR *new;
+  void *tmp;
+  struct __ACC__ERR *temp;
+  struct __ACC__ERR *next;
+  void *excep;
+  unsigned long __cil_tmp10;
+  unsigned long __cil_tmp11;
+  unsigned long __cil_tmp12;
+  unsigned long __cil_tmp13;
+  void *__cil_tmp14;
+  unsigned long __cil_tmp15;
+  unsigned long __cil_tmp16;
+  void *__cil_tmp17;
+  void **mem_18;
+  struct __ACC__ERR **mem_19;
+  struct __ACC__ERR **mem_20;
+  void **mem_21;
+  struct __ACC__ERR **mem_22;
+  void **mem_23;
+  void **mem_24;
+
+  {
+    if (count == 0) {
+      return (retValue_acc);
+    } else {
+    }
+    if (mode == 0) {
+      {
+        tmp = malloc(16UL);
+        new = (struct __ACC__ERR *)tmp;
+        mem_18 = (void **)new;
+        *mem_18 = env;
+        __cil_tmp10 = (unsigned long)new;
+        __cil_tmp11 = __cil_tmp10 + 8;
+        mem_19 = (struct __ACC__ERR **)__cil_tmp11;
+        *mem_19 = head;
+        head = new;
+        retValue_acc = (void *)new;
+      }
+      return (retValue_acc);
+    } else {
+    }
+    if (mode == 1) {
+      temp = head;
+      {
+        while (1) {
+        while_3_continue: /* CIL Label */;
+          if (count > 1) {
+
+          } else {
+            goto while_3_break;
+          }
+          {
+            __cil_tmp12 = (unsigned long)temp;
+            __cil_tmp13 = __cil_tmp12 + 8;
+            mem_20 = (struct __ACC__ERR **)__cil_tmp13;
+            next = *mem_20;
+            mem_21 = (void **)temp;
+            excep = *mem_21;
+            __cil_tmp14 = (void *)temp;
+            free(__cil_tmp14);
+            __utac__exception__cf_handler_reset(excep);
+            temp = next;
+            count = count - 1;
+          }
+        }
+      while_3_break: /* CIL Label */;
+      }
+      {
+        __cil_tmp15 = (unsigned long)temp;
+        __cil_tmp16 = __cil_tmp15 + 8;
+        mem_22 = (struct __ACC__ERR **)__cil_tmp16;
+        head = *mem_22;
+        mem_23 = (void **)temp;
+        excep = *mem_23;
+        __cil_tmp17 = (void *)temp;
+        free(__cil_tmp17);
+        __utac__exception__cf_handler_reset(excep);
+        retValue_acc = excep;
+      }
+      return (retValue_acc);
+    } else {
+    }
+    if (mode == 2) {
+      if (head) {
+        mem_24 = (void **)head;
+        retValue_acc = *mem_24;
+        return (retValue_acc);
+      } else {
+        retValue_acc = (void *)0;
+        return (retValue_acc);
+      }
+    } else {
+    }
+    return (retValue_acc);
+  }
+}
+void *__utac__get_this_arg(int i, struct JoinPoint *this) {
+  void *retValue_acc;
+  unsigned long __cil_tmp4;
+  unsigned long __cil_tmp5;
+  int __cil_tmp6;
+  int __cil_tmp7;
+  unsigned long __cil_tmp8;
+  unsigned long __cil_tmp9;
+  void **__cil_tmp10;
+  void **__cil_tmp11;
+  int *mem_12;
+  void ***mem_13;
+
+  {
+    if (i > 0) {
+      {
+        __cil_tmp4 = (unsigned long)this;
+        __cil_tmp5 = __cil_tmp4 + 16;
+        mem_12 = (int *)__cil_tmp5;
+        __cil_tmp6 = *mem_12;
+        if (i <= __cil_tmp6) {
+
+        } else {
+          {
+            __assert_fail("i > 0 && i <= this->argsCount", "libacc.c",
+                          123U, "__utac__get_this_arg");
+          }
+        }
+      }
+    } else {
+      {
+        __assert_fail("i > 0 && i <= this->argsCount", "libacc.c",
+                      123U, "__utac__get_this_arg");
+      }
+    }
+    __cil_tmp7 = i - 1;
+    __cil_tmp8 = (unsigned long)this;
+    __cil_tmp9 = __cil_tmp8 + 8;
+    mem_13 = (void ***)__cil_tmp9;
+    __cil_tmp10 = *mem_13;
+    __cil_tmp11 = __cil_tmp10 + __cil_tmp7;
+    retValue_acc = *__cil_tmp11;
+    return (retValue_acc);
+    return (retValue_acc);
+  }
+}
+char const *__utac__get_this_argtype(int i, struct JoinPoint *this) {
+  char const *retValue_acc;
+  unsigned long __cil_tmp4;
+  unsigned long __cil_tmp5;
+  int __cil_tmp6;
+  int __cil_tmp7;
+  unsigned long __cil_tmp8;
+  unsigned long __cil_tmp9;
+  char const **__cil_tmp10;
+  char const **__cil_tmp11;
+  int *mem_12;
+  char const ***mem_13;
+
+  {
+    if (i > 0) {
+      {
+        __cil_tmp4 = (unsigned long)this;
+        __cil_tmp5 = __cil_tmp4 + 16;
+        mem_12 = (int *)__cil_tmp5;
+        __cil_tmp6 = *mem_12;
+        if (i <= __cil_tmp6) {
+
+        } else {
+          {
+            __assert_fail("i > 0 && i <= this->argsCount", "libacc.c",
+                          131U, "__utac__get_this_argtype");
+          }
+        }
+      }
+    } else {
+      {
+        __assert_fail("i > 0 && i <= this->argsCount", "libacc.c",
+                      131U, "__utac__get_this_argtype");
+      }
+    }
+    __cil_tmp7 = i - 1;
+    __cil_tmp8 = (unsigned long)this;
+    __cil_tmp9 = __cil_tmp8 + 24;
+    mem_13 = (char const ***)__cil_tmp9;
+    __cil_tmp10 = *mem_13;
+    __cil_tmp11 = __cil_tmp10 + __cil_tmp7;
+    retValue_acc = *__cil_tmp11;
+    return (retValue_acc);
+    return (retValue_acc);
+  }
+}
+#pragma merger(0, "ClientLib.i", "")
+int initClient(void);
+char *getClientName(int handle);
+void setClientName(int handle, char *value);
+int getClientOutbuffer(int handle);
+void setClientOutbuffer(int handle, int value);
+int getClientAddressBookSize(int handle);
+void setClientAddressBookSize(int handle, int value);
+int createClientAddressBookEntry(int handle);
+int getClientAddressBookAlias(int handle, int index);
+void setClientAddressBookAlias(int handle, int index, int value);
+int getClientAddressBookAddress(int handle, int index);
+void setClientAddressBookAddress(int handle, int index, int value);
+int getClientAutoResponse(int handle);
+void setClientAutoResponse(int handle, int value);
+int getClientPrivateKey(int handle);
+int getClientKeyringSize(int handle);
+int getClientForwardReceiver(int handle);
+int getClientId(int handle);
+int findPublicKey(int handle, int userid);
+int findClientAddressBookAlias(int handle, int userid);
+int __ste_Client_counter = 0;
+int initClient(void) {
+  int retValue_acc;
+
+  {
+    if (__ste_Client_counter < 3) {
+      __ste_Client_counter = __ste_Client_counter + 1;
+      retValue_acc = __ste_Client_counter;
+      return (retValue_acc);
+    } else {
+      retValue_acc = -1;
+      return (retValue_acc);
+    }
+    return (retValue_acc);
+  }
+}
+char *__ste_client_name0 = (char *)0;
+char *__ste_client_name1 = (char *)0;
+char *__ste_client_name2 = (char *)0;
+char *getClientName(int handle) {
+  char *retValue_acc;
+  void *__cil_tmp3;
+
+  {
+    if (handle == 1) {
+      retValue_acc = __ste_client_name0;
+      return (retValue_acc);
+    } else {
+      if (handle == 2) {
+        retValue_acc = __ste_client_name1;
+        return (retValue_acc);
+      } else {
+        if (handle == 3) {
+          retValue_acc = __ste_client_name2;
+          return (retValue_acc);
+        } else {
+          __cil_tmp3 = (void *)0;
+          retValue_acc = (char *)__cil_tmp3;
+          return (retValue_acc);
+        }
+      }
+    }
+    return (retValue_acc);
+  }
+}
+void setClientName(int handle, char *value) {
+
+  {
+    if (handle == 1) {
+      __ste_client_name0 = value;
+    } else {
+      if (handle == 2) {
+        __ste_client_name1 = value;
+      } else {
+        if (handle == 3) {
+          __ste_client_name2 = value;
+        } else {
+        }
+      }
+    }
+    return;
+  }
+}
+int __ste_client_outbuffer0 = 0;
+int __ste_client_outbuffer1 = 0;
+int __ste_client_outbuffer2 = 0;
+int __ste_client_outbuffer3 = 0;
+int getClientOutbuffer(int handle) {
+  int retValue_acc;
+
+  {
+    if (handle == 1) {
+      retValue_acc = __ste_client_outbuffer0;
+      return (retValue_acc);
+    } else {
+      if (handle == 2) {
+        retValue_acc = __ste_client_outbuffer1;
+        return (retValue_acc);
+      } else {
+        if (handle == 3) {
+          retValue_acc = __ste_client_outbuffer2;
+          return (retValue_acc);
+        } else {
+          retValue_acc = 0;
+          return (retValue_acc);
+        }
+      }
+    }
+    return (retValue_acc);
+  }
+}
+void setClientOutbuffer(int handle, int value) {
+
+  {
+    if (handle == 1) {
+      __ste_client_outbuffer0 = value;
+    } else {
+      if (handle == 2) {
+        __ste_client_outbuffer1 = value;
+      } else {
+        if (handle == 3) {
+          __ste_client_outbuffer2 = value;
+        } else {
+        }
+      }
+    }
+    return;
+  }
+}
+int __ste_ClientAddressBook_size0 = 0;
+int __ste_ClientAddressBook_size1 = 0;
+int __ste_ClientAddressBook_size2 = 0;
+int getClientAddressBookSize(int handle) {
+  int retValue_acc;
+
+  {
+    if (handle == 1) {
+      retValue_acc = __ste_ClientAddressBook_size0;
+      return (retValue_acc);
+    } else {
+      if (handle == 2) {
+        retValue_acc = __ste_ClientAddressBook_size1;
+        return (retValue_acc);
+      } else {
+        if (handle == 3) {
+          retValue_acc = __ste_ClientAddressBook_size2;
+          return (retValue_acc);
+        } else {
+          retValue_acc = 0;
+          return (retValue_acc);
+        }
+      }
+    }
+    return (retValue_acc);
+  }
+}
+void setClientAddressBookSize(int handle, int value) {
+
+  {
+    if (handle == 1) {
+      __ste_ClientAddressBook_size0 = value;
+    } else {
+      if (handle == 2) {
+        __ste_ClientAddressBook_size1 = value;
+      } else {
+        if (handle == 3) {
+          __ste_ClientAddressBook_size2 = value;
+        } else {
+        }
+      }
+    }
+    return;
+  }
+}
+int createClientAddressBookEntry(int handle) {
+  int retValue_acc;
+  int size;
+  int tmp;
+  int __cil_tmp5;
+
+  {
+    {
+      tmp = getClientAddressBookSize(handle);
+      size = tmp;
+    }
+    if (size < 3) {
+      {
+        __cil_tmp5 = size + 1;
+        setClientAddressBookSize(handle, __cil_tmp5);
+        retValue_acc = size + 1;
+      }
+      return (retValue_acc);
+    } else {
+      retValue_acc = -1;
+      return (retValue_acc);
+    }
+    return (retValue_acc);
+  }
+}
+int __ste_Client_AddressBook0_Alias0 = 0;
+int __ste_Client_AddressBook0_Alias1 = 0;
+int __ste_Client_AddressBook0_Alias2 = 0;
+int __ste_Client_AddressBook1_Alias0 = 0;
+int __ste_Client_AddressBook1_Alias1 = 0;
+int __ste_Client_AddressBook1_Alias2 = 0;
+int __ste_Client_AddressBook2_Alias0 = 0;
+int __ste_Client_AddressBook2_Alias1 = 0;
+int __ste_Client_AddressBook2_Alias2 = 0;
+int getClientAddressBookAlias(int handle, int index) {
+  int retValue_acc;
+
+  {
+    if (handle == 1) {
+      if (index == 0) {
+        retValue_acc = __ste_Client_AddressBook0_Alias0;
+        return (retValue_acc);
+      } else {
+        if (index == 1) {
+          retValue_acc = __ste_Client_AddressBook0_Alias1;
+          return (retValue_acc);
+        } else {
+          if (index == 2) {
+            retValue_acc = __ste_Client_AddressBook0_Alias2;
+            return (retValue_acc);
+          } else {
+            retValue_acc = 0;
+            return (retValue_acc);
+          }
+        }
+      }
+    } else {
+      if (handle == 2) {
+        if (index == 0) {
+          retValue_acc = __ste_Client_AddressBook1_Alias0;
+          return (retValue_acc);
+        } else {
+          if (index == 1) {
+            retValue_acc = __ste_Client_AddressBook1_Alias1;
+            return (retValue_acc);
+          } else {
+            if (index == 2) {
+              retValue_acc = __ste_Client_AddressBook1_Alias2;
+              return (retValue_acc);
+            } else {
+              retValue_acc = 0;
+              return (retValue_acc);
+            }
+          }
+        }
+      } else {
+        if (handle == 3) {
+          if (index == 0) {
+            retValue_acc = __ste_Client_AddressBook2_Alias0;
+            return (retValue_acc);
+          } else {
+            if (index == 1) {
+              retValue_acc = __ste_Client_AddressBook2_Alias1;
+              return (retValue_acc);
+            } else {
+              if (index == 2) {
+                retValue_acc = __ste_Client_AddressBook2_Alias2;
+                return (retValue_acc);
+              } else {
+                retValue_acc = 0;
+                return (retValue_acc);
+              }
+            }
+          }
+        } else {
+          retValue_acc = 0;
+          return (retValue_acc);
+        }
+      }
+    }
+    return (retValue_acc);
+  }
+}
+int findClientAddressBookAlias(int handle, int userid) {
+  int retValue_acc;
+
+  {
+    if (handle == 1) {
+      if (userid == __ste_Client_AddressBook0_Alias0) {
+        retValue_acc = 0;
+        return (retValue_acc);
+      } else {
+        if (userid == __ste_Client_AddressBook0_Alias1) {
+          retValue_acc = 1;
+          return (retValue_acc);
+        } else {
+          if (userid == __ste_Client_AddressBook0_Alias2) {
+            retValue_acc = 2;
+            return (retValue_acc);
+          } else {
+            retValue_acc = -1;
+            return (retValue_acc);
+          }
+        }
+      }
+    } else {
+      if (handle == 2) {
+        if (userid == __ste_Client_AddressBook1_Alias0) {
+          retValue_acc = 0;
+          return (retValue_acc);
+        } else {
+          if (userid == __ste_Client_AddressBook1_Alias1) {
+            retValue_acc = 1;
+            return (retValue_acc);
+          } else {
+            if (userid == __ste_Client_AddressBook1_Alias2) {
+              retValue_acc = 2;
+              return (retValue_acc);
+            } else {
+              retValue_acc = -1;
+              return (retValue_acc);
+            }
+          }
+        }
+      } else {
+        if (handle == 3) {
+          if (userid == __ste_Client_AddressBook2_Alias0) {
+            retValue_acc = 0;
+            return (retValue_acc);
+          } else {
+            if (userid == __ste_Client_AddressBook2_Alias1) {
+              retValue_acc = 1;
+              return (retValue_acc);
+            } else {
+              if (userid == __ste_Client_AddressBook2_Alias2) {
+                retValue_acc = 2;
+                return (retValue_acc);
+              } else {
+                retValue_acc = -1;
+                return (retValue_acc);
+              }
+            }
+          }
+        } else {
+          retValue_acc = -1;
+          return (retValue_acc);
+        }
+      }
+    }
+    return (retValue_acc);
+  }
+}
+void setClientAddressBookAlias(int handle, int index, int value) {
+
+  {
+    if (handle == 1) {
+      if (index == 0) {
+        __ste_Client_AddressBook0_Alias0 = value;
+      } else {
+        if (index == 1) {
+          __ste_Client_AddressBook0_Alias1 = value;
+        } else {
+          if (index == 2) {
+            __ste_Client_AddressBook0_Alias2 = value;
+          } else {
+          }
+        }
+      }
+    } else {
+      if (handle == 2) {
+        if (index == 0) {
+          __ste_Client_AddressBook1_Alias0 = value;
+        } else {
+          if (index == 1) {
+            __ste_Client_AddressBook1_Alias1 = value;
+          } else {
+            if (index == 2) {
+              __ste_Client_AddressBook1_Alias2 = value;
+            } else {
+            }
+          }
+        }
+      } else {
+        if (handle == 3) {
+          if (index == 0) {
+            __ste_Client_AddressBook2_Alias0 = value;
+          } else {
+            if (index == 1) {
+              __ste_Client_AddressBook2_Alias1 = value;
+            } else {
+              if (index == 2) {
+                __ste_Client_AddressBook2_Alias2 = value;
+              } else {
+              }
+            }
+          }
+        } else {
+        }
+      }
+    }
+    return;
+  }
+}
+int __ste_Client_AddressBook0_Address0 = 0;
+int __ste_Client_AddressBook0_Address1 = 0;
+int __ste_Client_AddressBook0_Address2 = 0;
+int __ste_Client_AddressBook1_Address0 = 0;
+int __ste_Client_AddressBook1_Address1 = 0;
+int __ste_Client_AddressBook1_Address2 = 0;
+int __ste_Client_AddressBook2_Address0 = 0;
+int __ste_Client_AddressBook2_Address1 = 0;
+int __ste_Client_AddressBook2_Address2 = 0;
+int getClientAddressBookAddress(int handle, int index) {
+  int retValue_acc;
+
+  {
+    if (handle == 1) {
+      if (index == 0) {
+        retValue_acc = __ste_Client_AddressBook0_Address0;
+        return (retValue_acc);
+      } else {
+        if (index == 1) {
+          retValue_acc = __ste_Client_AddressBook0_Address1;
+          return (retValue_acc);
+        } else {
+          if (index == 2) {
+            retValue_acc = __ste_Client_AddressBook0_Address2;
+            return (retValue_acc);
+          } else {
+            retValue_acc = 0;
+            return (retValue_acc);
+          }
+        }
+      }
+    } else {
+      if (handle == 2) {
+        if (index == 0) {
+          retValue_acc = __ste_Client_AddressBook1_Address0;
+          return (retValue_acc);
+        } else {
+          if (index == 1) {
+            retValue_acc = __ste_Client_AddressBook1_Address1;
+            return (retValue_acc);
+          } else {
+            if (index == 2) {
+              retValue_acc = __ste_Client_AddressBook1_Address2;
+              return (retValue_acc);
+            } else {
+              retValue_acc = 0;
+              return (retValue_acc);
+            }
+          }
+        }
+      } else {
+        if (handle == 3) {
+          if (index == 0) {
+            retValue_acc = __ste_Client_AddressBook2_Address0;
+            return (retValue_acc);
+          } else {
+            if (index == 1) {
+              retValue_acc = __ste_Client_AddressBook2_Address1;
+              return (retValue_acc);
+            } else {
+              if (index == 2) {
+                retValue_acc = __ste_Client_AddressBook2_Address2;
+                return (retValue_acc);
+              } else {
+                retValue_acc = 0;
+                return (retValue_acc);
+              }
+            }
+          }
+        } else {
+          retValue_acc = 0;
+          return (retValue_acc);
+        }
+      }
+    }
+    return (retValue_acc);
+  }
+}
+void setClientAddressBookAddress(int handle, int index, int value) {
+
+  {
+    if (handle == 1) {
+      if (index == 0) {
+        __ste_Client_AddressBook0_Address0 = value;
+      } else {
+        if (index == 1) {
+          __ste_Client_AddressBook0_Address1 = value;
+        } else {
+          if (index == 2) {
+            __ste_Client_AddressBook0_Address2 = value;
+          } else {
+          }
+        }
+      }
+    } else {
+      if (handle == 2) {
+        if (index == 0) {
+          __ste_Client_AddressBook1_Address0 = value;
+        } else {
+          if (index == 1) {
+            __ste_Client_AddressBook1_Address1 = value;
+          } else {
+            if (index == 2) {
+              __ste_Client_AddressBook1_Address2 = value;
+            } else {
+            }
+          }
+        }
+      } else {
+        if (handle == 3) {
+          if (index == 0) {
+            __ste_Client_AddressBook2_Address0 = value;
+          } else {
+            if (index == 1) {
+              __ste_Client_AddressBook2_Address1 = value;
+            } else {
+              if (index == 2) {
+                __ste_Client_AddressBook2_Address2 = value;
+              } else {
+              }
+            }
+          }
+        } else {
+        }
+      }
+    }
+    return;
+  }
+}
+int __ste_client_autoResponse0 = 0;
+int __ste_client_autoResponse1 = 0;
+int __ste_client_autoResponse2 = 0;
+int getClientAutoResponse(int handle) {
+  int retValue_acc;
+
+  {
+    if (handle == 1) {
+      retValue_acc = __ste_client_autoResponse0;
+      return (retValue_acc);
+    } else {
+      if (handle == 2) {
+        retValue_acc = __ste_client_autoResponse1;
+        return (retValue_acc);
+      } else {
+        if (handle == 3) {
+          retValue_acc = __ste_client_autoResponse2;
+          return (retValue_acc);
+        } else {
+          retValue_acc = -1;
+          return (retValue_acc);
+        }
+      }
+    }
+    return (retValue_acc);
+  }
+}
+void setClientAutoResponse(int handle, int value) {
+
+  {
+    if (handle == 1) {
+      __ste_client_autoResponse0 = value;
+    } else {
+      if (handle == 2) {
+        __ste_client_autoResponse1 = value;
+      } else {
+        if (handle == 3) {
+          __ste_client_autoResponse2 = value;
+        } else {
+        }
+      }
+    }
+    return;
+  }
+}
+int __ste_client_privateKey0 = 0;
+int __ste_client_privateKey1 = 0;
+int __ste_client_privateKey2 = 0;
+int getClientPrivateKey(int handle) {
+  int retValue_acc;
+
+  {
+    if (handle == 1) {
+      retValue_acc = __ste_client_privateKey0;
+      return (retValue_acc);
+    } else {
+      if (handle == 2) {
+        retValue_acc = __ste_client_privateKey1;
+        return (retValue_acc);
+      } else {
+        if (handle == 3) {
+          retValue_acc = __ste_client_privateKey2;
+          return (retValue_acc);
+        } else {
+          retValue_acc = 0;
+          return (retValue_acc);
+        }
+      }
+    }
+    return (retValue_acc);
+  }
+}
+void setClientPrivateKey(int handle, int value) {
+
+  {
+    if (handle == 1) {
+      __ste_client_privateKey0 = value;
+    } else {
+      if (handle == 2) {
+        __ste_client_privateKey1 = value;
+      } else {
+        if (handle == 3) {
+          __ste_client_privateKey2 = value;
+        } else {
+        }
+      }
+    }
+    return;
+  }
+}
+int __ste_ClientKeyring_size0 = 0;
+int __ste_ClientKeyring_size1 = 0;
+int __ste_ClientKeyring_size2 = 0;
+int getClientKeyringSize(int handle) {
+  int retValue_acc;
+
+  {
+    if (handle == 1) {
+      retValue_acc = __ste_ClientKeyring_size0;
+      return (retValue_acc);
+    } else {
+      if (handle == 2) {
+        retValue_acc = __ste_ClientKeyring_size1;
+        return (retValue_acc);
+      } else {
+        if (handle == 3) {
+          retValue_acc = __ste_ClientKeyring_size2;
+          return (retValue_acc);
+        } else {
+          retValue_acc = 0;
+          return (retValue_acc);
+        }
+      }
+    }
+    return (retValue_acc);
+  }
+}
+void setClientKeyringSize(int handle, int value) {
+
+  {
+    if (handle == 1) {
+      __ste_ClientKeyring_size0 = value;
+    } else {
+      if (handle == 2) {
+        __ste_ClientKeyring_size1 = value;
+      } else {
+        if (handle == 3) {
+          __ste_ClientKeyring_size2 = value;
+        } else {
+        }
+      }
+    }
+    return;
+  }
+}
+int createClientKeyringEntry(int handle) {
+  int retValue_acc;
+  int size;
+  int tmp;
+  int __cil_tmp5;
+
+  {
+    {
+      tmp = getClientKeyringSize(handle);
+      size = tmp;
+    }
+    if (size < 2) {
+      {
+        __cil_tmp5 = size + 1;
+        setClientKeyringSize(handle, __cil_tmp5);
+        retValue_acc = size + 1;
+      }
+      return (retValue_acc);
+    } else {
+      retValue_acc = -1;
+      return (retValue_acc);
+    }
+    return (retValue_acc);
+  }
+}
+int __ste_Client_Keyring0_User0 = 0;
+int __ste_Client_Keyring0_User1 = 0;
+int __ste_Client_Keyring0_User2 = 0;
+int __ste_Client_Keyring1_User0 = 0;
+int __ste_Client_Keyring1_User1 = 0;
+int __ste_Client_Keyring1_User2 = 0;
+int __ste_Client_Keyring2_User0 = 0;
+int __ste_Client_Keyring2_User1 = 0;
+int __ste_Client_Keyring2_User2 = 0;
+int getClientKeyringUser(int handle, int index) {
+  int retValue_acc;
+
+  {
+    if (handle == 1) {
+      if (index == 0) {
+        retValue_acc = __ste_Client_Keyring0_User0;
+        return (retValue_acc);
+      } else {
+        if (index == 1) {
+          retValue_acc = __ste_Client_Keyring0_User1;
+          return (retValue_acc);
+        } else {
+          retValue_acc = 0;
+          return (retValue_acc);
+        }
+      }
+    } else {
+      if (handle == 2) {
+        if (index == 0) {
+          retValue_acc = __ste_Client_Keyring1_User0;
+          return (retValue_acc);
+        } else {
+          if (index == 1) {
+            retValue_acc = __ste_Client_Keyring1_User1;
+            return (retValue_acc);
+          } else {
+            retValue_acc = 0;
+            return (retValue_acc);
+          }
+        }
+      } else {
+        if (handle == 3) {
+          if (index == 0) {
+            retValue_acc = __ste_Client_Keyring2_User0;
+            return (retValue_acc);
+          } else {
+            if (index == 1) {
+              retValue_acc = __ste_Client_Keyring2_User1;
+              return (retValue_acc);
+            } else {
+              retValue_acc = 0;
+              return (retValue_acc);
+            }
+          }
+        } else {
+          retValue_acc = 0;
+          return (retValue_acc);
+        }
+      }
+    }
+    return (retValue_acc);
+  }
+}
+void setClientKeyringUser(int handle, int index, int value) {
+
+  {
+    if (handle == 1) {
+      if (index == 0) {
+        __ste_Client_Keyring0_User0 = value;
+      } else {
+        if (index == 1) {
+          __ste_Client_Keyring0_User1 = value;
+        } else {
+        }
+      }
+    } else {
+      if (handle == 2) {
+        if (index == 0) {
+          __ste_Client_Keyring1_User0 = value;
+        } else {
+          if (index == 1) {
+            __ste_Client_Keyring1_User1 = value;
+          } else {
+          }
+        }
+      } else {
+        if (handle == 3) {
+          if (index == 0) {
+            __ste_Client_Keyring2_User0 = value;
+          } else {
+            if (index == 1) {
+              __ste_Client_Keyring2_User1 = value;
+            } else {
+            }
+          }
+        } else {
+        }
+      }
+    }
+    return;
+  }
+}
+int __ste_Client_Keyring0_PublicKey0 = 0;
+int __ste_Client_Keyring0_PublicKey1 = 0;
+int __ste_Client_Keyring0_PublicKey2 = 0;
+int __ste_Client_Keyring1_PublicKey0 = 0;
+int __ste_Client_Keyring1_PublicKey1 = 0;
+int __ste_Client_Keyring1_PublicKey2 = 0;
+int __ste_Client_Keyring2_PublicKey0 = 0;
+int __ste_Client_Keyring2_PublicKey1 = 0;
+int __ste_Client_Keyring2_PublicKey2 = 0;
+int getClientKeyringPublicKey(int handle, int index) {
+  int retValue_acc;
+
+  {
+    if (handle == 1) {
+      if (index == 0) {
+        retValue_acc = __ste_Client_Keyring0_PublicKey0;
+        return (retValue_acc);
+      } else {
+        if (index == 1) {
+          retValue_acc = __ste_Client_Keyring0_PublicKey1;
+          return (retValue_acc);
+        } else {
+          retValue_acc = 0;
+          return (retValue_acc);
+        }
+      }
+    } else {
+      if (handle == 2) {
+        if (index == 0) {
+          retValue_acc = __ste_Client_Keyring1_PublicKey0;
+          return (retValue_acc);
+        } else {
+          if (index == 1) {
+            retValue_acc = __ste_Client_Keyring1_PublicKey1;
+            return (retValue_acc);
+          } else {
+            retValue_acc = 0;
+            return (retValue_acc);
+          }
+        }
+      } else {
+        if (handle == 3) {
+          if (index == 0) {
+            retValue_acc = __ste_Client_Keyring2_PublicKey0;
+            return (retValue_acc);
+          } else {
+            if (index == 1) {
+              retValue_acc = __ste_Client_Keyring2_PublicKey1;
+              return (retValue_acc);
+            } else {
+              retValue_acc = 0;
+              return (retValue_acc);
+            }
+          }
+        } else {
+          retValue_acc = 0;
+          return (retValue_acc);
+        }
+      }
+    }
+    return (retValue_acc);
+  }
+}
+int findPublicKey(int handle, int userid) {
+  int retValue_acc;
+
+  {
+    if (handle == 1) {
+      if (userid == __ste_Client_Keyring0_User0) {
+        retValue_acc = __ste_Client_Keyring0_PublicKey0;
+        return (retValue_acc);
+      } else {
+        if (userid == __ste_Client_Keyring0_User1) {
+          retValue_acc = __ste_Client_Keyring0_PublicKey1;
+          return (retValue_acc);
+        } else {
+          retValue_acc = 0;
+          return (retValue_acc);
+        }
+      }
+    } else {
+      if (handle == 2) {
+        if (userid == __ste_Client_Keyring1_User0) {
+          retValue_acc = __ste_Client_Keyring1_PublicKey0;
+          return (retValue_acc);
+        } else {
+          if (userid == __ste_Client_Keyring1_User1) {
+            retValue_acc = __ste_Client_Keyring1_PublicKey1;
+            return (retValue_acc);
+          } else {
+            retValue_acc = 0;
+            return (retValue_acc);
+          }
+        }
+      } else {
+        if (handle == 3) {
+          if (userid == __ste_Client_Keyring2_User0) {
+            retValue_acc = __ste_Client_Keyring2_PublicKey0;
+            return (retValue_acc);
+          } else {
+            if (userid == __ste_Client_Keyring2_User1) {
+              retValue_acc = __ste_Client_Keyring2_PublicKey1;
+              return (retValue_acc);
+            } else {
+              retValue_acc = 0;
+              return (retValue_acc);
+            }
+          }
+        } else {
+          retValue_acc = 0;
+          return (retValue_acc);
+        }
+      }
+    }
+    return (retValue_acc);
+  }
+}
+void setClientKeyringPublicKey(int handle, int index, int value) {
+
+  {
+    if (handle == 1) {
+      if (index == 0) {
+        __ste_Client_Keyring0_PublicKey0 = value;
+      } else {
+        if (index == 1) {
+          __ste_Client_Keyring0_PublicKey1 = value;
+        } else {
+        }
+      }
+    } else {
+      if (handle == 2) {
+        if (index == 0) {
+          __ste_Client_Keyring1_PublicKey0 = value;
+        } else {
+          if (index == 1) {
+            __ste_Client_Keyring1_PublicKey1 = value;
+          } else {
+          }
+        }
+      } else {
+        if (handle == 3) {
+          if (index == 0) {
+            __ste_Client_Keyring2_PublicKey0 = value;
+          } else {
+            if (index == 1) {
+              __ste_Client_Keyring2_PublicKey1 = value;
+            } else {
+            }
+          }
+        } else {
+        }
+      }
+    }
+    return;
+  }
+}
+int __ste_client_forwardReceiver0 = 0;
+int __ste_client_forwardReceiver1 = 0;
+int __ste_client_forwardReceiver2 = 0;
+int __ste_client_forwardReceiver3 = 0;
+int getClientForwardReceiver(int handle) {
+  int retValue_acc;
+
+  {
+    if (handle == 1) {
+      retValue_acc = __ste_client_forwardReceiver0;
+      return (retValue_acc);
+    } else {
+      if (handle == 2) {
+        retValue_acc = __ste_client_forwardReceiver1;
+        return (retValue_acc);
+      } else {
+        if (handle == 3) {
+          retValue_acc = __ste_client_forwardReceiver2;
+          return (retValue_acc);
+        } else {
+          retValue_acc = 0;
+          return (retValue_acc);
+        }
+      }
+    }
+    return (retValue_acc);
+  }
+}
+void setClientForwardReceiver(int handle, int value) {
+
+  {
+    if (handle == 1) {
+      __ste_client_forwardReceiver0 = value;
+    } else {
+      if (handle == 2) {
+        __ste_client_forwardReceiver1 = value;
+      } else {
+        if (handle == 3) {
+          __ste_client_forwardReceiver2 = value;
+        } else {
+        }
+      }
+    }
+    return;
+  }
+}
+int __ste_client_idCounter0 = 0;
+int __ste_client_idCounter1 = 0;
+int __ste_client_idCounter2 = 0;
+int getClientId(int handle) {
+  int retValue_acc;
+
+  {
+    if (handle == 1) {
+      retValue_acc = __ste_client_idCounter0;
+      return (retValue_acc);
+    } else {
+      if (handle == 2) {
+        retValue_acc = __ste_client_idCounter1;
+        return (retValue_acc);
+      } else {
+        if (handle == 3) {
+          retValue_acc = __ste_client_idCounter2;
+          return (retValue_acc);
+        } else {
+          retValue_acc = 0;
+          return (retValue_acc);
+        }
+      }
+    }
+    return (retValue_acc);
+  }
+}
+void setClientId(int handle, int value) {
+
+  {
+    if (handle == 1) {
+      __ste_client_idCounter0 = value;
+    } else {
+      if (handle == 2) {
+        __ste_client_idCounter1 = value;
+      } else {
+        if (handle == 3) {
+          __ste_client_idCounter2 = value;
+        } else {
+        }
+      }
+    }
+    return;
+  }
+}
+#pragma merger(0, "EmailLib.i", "")
+int initEmail(void);
+void setEmailId(int handle, int value);
+char *getEmailSubject(int handle);
+void setEmailSubject(int handle, char *value);
+char *getEmailBody(int handle);
+void setEmailBody(int handle, char *value);
+void setEmailIsEncrypted(int handle, int value);
+void setEmailEncryptionKey(int handle, int value);
+int isSigned(int handle);
+void setEmailIsSigned(int handle, int value);
+int getEmailSignKey(int handle);
+void setEmailSignKey(int handle, int value);
+int isVerified(int handle);
+void setEmailIsSignatureVerified(int handle, int value);
+int __ste_Email_counter = 0;
+int initEmail(void) {
+  int retValue_acc;
+
+  {
+    if (__ste_Email_counter < 2) {
+      __ste_Email_counter = __ste_Email_counter + 1;
+      retValue_acc = __ste_Email_counter;
+      return (retValue_acc);
+    } else {
+      retValue_acc = -1;
+      return (retValue_acc);
+    }
+    return (retValue_acc);
+  }
+}
+int __ste_email_id0 = 0;
+int __ste_email_id1 = 0;
+int getEmailId(int handle) {
+  int retValue_acc;
+
+  {
+    if (handle == 1) {
+      retValue_acc = __ste_email_id0;
+      return (retValue_acc);
+    } else {
+      if (handle == 2) {
+        retValue_acc = __ste_email_id1;
+        return (retValue_acc);
+      } else {
+        retValue_acc = 0;
+        return (retValue_acc);
+      }
+    }
+    return (retValue_acc);
+  }
+}
+void setEmailId(int handle, int value) {
+
+  {
+    if (handle == 1) {
+      __ste_email_id0 = value;
+    } else {
+      if (handle == 2) {
+        __ste_email_id1 = value;
+      } else {
+      }
+    }
+    return;
+  }
+}
+int __ste_email_from0 = 0;
+int __ste_email_from1 = 0;
+int getEmailFrom(int handle) {
+  int retValue_acc;
+
+  {
+    if (handle == 1) {
+      retValue_acc = __ste_email_from0;
+      return (retValue_acc);
+    } else {
+      if (handle == 2) {
+        retValue_acc = __ste_email_from1;
+        return (retValue_acc);
+      } else {
+        retValue_acc = 0;
+        return (retValue_acc);
+      }
+    }
+    return (retValue_acc);
+  }
+}
+void setEmailFrom(int handle, int value) {
+
+  {
+    if (handle == 1) {
+      __ste_email_from0 = value;
+    } else {
+      if (handle == 2) {
+        __ste_email_from1 = value;
+      } else {
+      }
+    }
+    return;
+  }
+}
+int __ste_email_to0 = 0;
+int __ste_email_to1 = 0;
+int getEmailTo(int handle) {
+  int retValue_acc;
+
+  {
+    if (handle == 1) {
+      retValue_acc = __ste_email_to0;
+      return (retValue_acc);
+    } else {
+      if (handle == 2) {
+        retValue_acc = __ste_email_to1;
+        return (retValue_acc);
+      } else {
+        retValue_acc = 0;
+        return (retValue_acc);
+      }
+    }
+    return (retValue_acc);
+  }
+}
+void setEmailTo(int handle, int value) {
+
+  {
+    if (handle == 1) {
+      __ste_email_to0 = value;
+    } else {
+      if (handle == 2) {
+        __ste_email_to1 = value;
+      } else {
+      }
+    }
+    return;
+  }
+}
+char *__ste_email_subject0;
+char *__ste_email_subject1;
+char *getEmailSubject(int handle) {
+  char *retValue_acc;
+  void *__cil_tmp3;
+
+  {
+    if (handle == 1) {
+      retValue_acc = __ste_email_subject0;
+      return (retValue_acc);
+    } else {
+      if (handle == 2) {
+        retValue_acc = __ste_email_subject1;
+        return (retValue_acc);
+      } else {
+        __cil_tmp3 = (void *)0;
+        retValue_acc = (char *)__cil_tmp3;
+        return (retValue_acc);
+      }
+    }
+    return (retValue_acc);
+  }
+}
+void setEmailSubject(int handle, char *value) {
+
+  {
+    if (handle == 1) {
+      __ste_email_subject0 = value;
+    } else {
+      if (handle == 2) {
+        __ste_email_subject1 = value;
+      } else {
+      }
+    }
+    return;
+  }
+}
+char *__ste_email_body0 = (char *)0;
+char *__ste_email_body1 = (char *)0;
+char *getEmailBody(int handle) {
+  char *retValue_acc;
+  void *__cil_tmp3;
+
+  {
+    if (handle == 1) {
+      retValue_acc = __ste_email_body0;
+      return (retValue_acc);
+    } else {
+      if (handle == 2) {
+        retValue_acc = __ste_email_body1;
+        return (retValue_acc);
+      } else {
+        __cil_tmp3 = (void *)0;
+        retValue_acc = (char *)__cil_tmp3;
+        return (retValue_acc);
+      }
+    }
+    return (retValue_acc);
+  }
+}
+void setEmailBody(int handle, char *value) {
+
+  {
+    if (handle == 1) {
+      __ste_email_body0 = value;
+    } else {
+      if (handle == 2) {
+        __ste_email_body1 = value;
+      } else {
+      }
+    }
+    return;
+  }
+}
+int __ste_email_isEncrypted0 = 0;
+int __ste_email_isEncrypted1 = 0;
+int isEncrypted(int handle) {
+  int retValue_acc;
+
+  {
+    if (handle == 1) {
+      retValue_acc = __ste_email_isEncrypted0;
+      return (retValue_acc);
+    } else {
+      if (handle == 2) {
+        retValue_acc = __ste_email_isEncrypted1;
+        return (retValue_acc);
+      } else {
+        retValue_acc = 0;
+        return (retValue_acc);
+      }
+    }
+    return (retValue_acc);
+  }
+}
+void setEmailIsEncrypted(int handle, int value) {
+
+  {
+    if (handle == 1) {
+      __ste_email_isEncrypted0 = value;
+    } else {
+      if (handle == 2) {
+        __ste_email_isEncrypted1 = value;
+      } else {
+      }
+    }
+    return;
+  }
+}
+int __ste_email_encryptionKey0 = 0;
+int __ste_email_encryptionKey1 = 0;
+int getEmailEncryptionKey(int handle) {
+  int retValue_acc;
+
+  {
+    if (handle == 1) {
+      retValue_acc = __ste_email_encryptionKey0;
+      return (retValue_acc);
+    } else {
+      if (handle == 2) {
+        retValue_acc = __ste_email_encryptionKey1;
+        return (retValue_acc);
+      } else {
+        retValue_acc = 0;
+        return (retValue_acc);
+      }
+    }
+    return (retValue_acc);
+  }
+}
+void setEmailEncryptionKey(int handle, int value) {
+
+  {
+    if (handle == 1) {
+      __ste_email_encryptionKey0 = value;
+    } else {
+      if (handle == 2) {
+        __ste_email_encryptionKey1 = value;
+      } else {
+      }
+    }
+    return;
+  }
+}
+int __ste_email_isSigned0 = 0;
+int __ste_email_isSigned1 = 0;
+int isSigned(int handle) {
+  int retValue_acc;
+
+  {
+    if (handle == 1) {
+      retValue_acc = __ste_email_isSigned0;
+      return (retValue_acc);
+    } else {
+      if (handle == 2) {
+        retValue_acc = __ste_email_isSigned1;
+        return (retValue_acc);
+      } else {
+        retValue_acc = 0;
+        return (retValue_acc);
+      }
+    }
+    return (retValue_acc);
+  }
+}
+void setEmailIsSigned(int handle, int value) {
+
+  {
+    if (handle == 1) {
+      __ste_email_isSigned0 = value;
+    } else {
+      if (handle == 2) {
+        __ste_email_isSigned1 = value;
+      } else {
+      }
+    }
+    return;
+  }
+}
+int __ste_email_signKey0 = 0;
+int __ste_email_signKey1 = 0;
+int getEmailSignKey(int handle) {
+  int retValue_acc;
+
+  {
+    if (handle == 1) {
+      retValue_acc = __ste_email_signKey0;
+      return (retValue_acc);
+    } else {
+      if (handle == 2) {
+        retValue_acc = __ste_email_signKey1;
+        return (retValue_acc);
+      } else {
+        retValue_acc = 0;
+        return (retValue_acc);
+      }
+    }
+    return (retValue_acc);
+  }
+}
+void setEmailSignKey(int handle, int value) {
+
+  {
+    if (handle == 1) {
+      __ste_email_signKey0 = value;
+    } else {
+      if (handle == 2) {
+        __ste_email_signKey1 = value;
+      } else {
+      }
+    }
+    return;
+  }
+}
+int __ste_email_isSignatureVerified0;
+int __ste_email_isSignatureVerified1;
+int isVerified(int handle) {
+  int retValue_acc;
+
+  {
+    if (handle == 1) {
+      retValue_acc = __ste_email_isSignatureVerified0;
+      return (retValue_acc);
+    } else {
+      if (handle == 2) {
+        retValue_acc = __ste_email_isSignatureVerified1;
+        return (retValue_acc);
+      } else {
+        retValue_acc = 0;
+        return (retValue_acc);
+      }
+    }
+    return (retValue_acc);
+  }
+}
+void setEmailIsSignatureVerified(int handle, int value) {
+
+  {
+    if (handle == 1) {
+      __ste_email_isSignatureVerified0 = value;
+    } else {
+      if (handle == 2) {
+        __ste_email_isSignatureVerified1 = value;
+      } else {
+      }
+    }
+    return;
+  }
+}
+#pragma merger(0, "DecryptForward_spec.i", "")
+inline static void __utac_acc__DecryptForward_spec__1(int msg) {
+  int tmp;
+
+  {
+    {
+      puts("before forward\n");
+      tmp = isReadable(msg);
+    }
+    if (tmp) {
+
+    } else {
+      {
+        __automaton_fail();
+      }
+    }
+    return;
+  }
+}
+#pragma merger(0, "Util.i", "")
+int prompt(char *msg);
+int prompt(char *msg) {
+  int retValue_acc;
+  int retval;
+  char const *__restrict __cil_tmp4;
+
+  {
+    {
+      __cil_tmp4 = (char const *__restrict)"%s\n";
+      printf(__cil_tmp4, msg);
+      retValue_acc = retval;
+    }
+    return (retValue_acc);
+    return (retValue_acc);
+  }
+}
+#pragma merger(0, "Client.i", "")
+void queue(int client, int msg);
+void mail(int client, int msg);
+void deliver(int client, int msg);
+void incoming(int client, int msg);
+int createClient(char *name);
+int isKeyPairValid(int publicKey, int privateKey);
+void forward(int client, int msg);
+int queue_empty = 1;
+int queued_message;
+int queued_client;
+void mail(int client, int msg) {
+  int tmp;
+
+  {
+    {
+      puts("mail sent");
+      tmp = getEmailTo(msg);
+      incoming(tmp, msg);
+    }
+    return;
+  }
+}
+void outgoing__wrappee__Keys(int client, int msg) {
+  int tmp;
+
+  {
+    {
+      tmp = getClientId(client);
+      setEmailFrom(msg, tmp);
+      mail(client, msg);
+    }
+    return;
+  }
+}
+void outgoing(int client, int msg) {
+  int receiver;
+  int tmp;
+  int pubkey;
+  int tmp___0;
+
+  {
+    {
+      tmp = getEmailTo(msg);
+      receiver = tmp;
+      tmp___0 = findPublicKey(client, receiver);
+      pubkey = tmp___0;
+    }
+    if (pubkey) {
+      {
+        setEmailEncryptionKey(msg, pubkey);
+        setEmailIsEncrypted(msg, 1);
+      }
+    } else {
+    }
+    {
+      outgoing__wrappee__Keys(client, msg);
+    }
+    return;
+  }
+}
+void deliver(int client, int msg) {
+
+  {
+    {
+      puts("mail delivered\n");
+    }
+    return;
+  }
+}
+void incoming__wrappee__Encrypt(int client, int msg) {
+
+  {
+    {
+      deliver(client, msg);
+    }
+    return;
+  }
+}
+void incoming__wrappee__Forward(int client, int msg) {
+  int fwreceiver;
+  int tmp;
+
+  {
+    {
+      incoming__wrappee__Encrypt(client, msg);
+      tmp = getClientForwardReceiver(client);
+      fwreceiver = tmp;
+    }
+    if (fwreceiver) {
+      {
+        setEmailTo(msg, fwreceiver);
+        forward(client, msg);
+      }
+    } else {
+    }
+    return;
+  }
+}
+void incoming(int client, int msg) {
+  int privkey;
+  int tmp;
+  int tmp___0;
+  int tmp___1;
+  int tmp___2;
+
+  {
+    {
+      tmp = getClientPrivateKey(client);
+      privkey = tmp;
+    }
+    if (privkey) {
+      {
+        tmp___0 = isEncrypted(msg);
+      }
+      if (tmp___0) {
+        {
+          tmp___1 = getEmailEncryptionKey(msg);
+          tmp___2 = isKeyPairValid(tmp___1, privkey);
+        }
+        if (tmp___2) {
+          {
+            setEmailIsEncrypted(msg, 0);
+            setEmailEncryptionKey(msg, 0);
+          }
+        } else {
+        }
+      } else {
+      }
+    } else {
+    }
+    {
+      incoming__wrappee__Forward(client, msg);
+    }
+    return;
+  }
+}
+int createClient(char *name) {
+  int retValue_acc;
+  int client;
+  int tmp;
+
+  {
+    {
+      tmp = initClient();
+      client = tmp;
+      retValue_acc = client;
+    }
+    return (retValue_acc);
+    return (retValue_acc);
+  }
+}
+void sendEmail(int sender, int receiver) {
+  int email;
+  int tmp;
+
+  {
+    {
+      tmp = createEmail(0, receiver);
+      email = tmp;
+      outgoing(sender, email);
+    }
+    return;
+  }
+}
+void queue(int client, int msg) {
+
+  {
+    queue_empty = 0;
+    queued_message = msg;
+    queued_client = client;
+    return;
+  }
+}
+int is_queue_empty(void) {
+  int retValue_acc;
+
+  {
+    retValue_acc = queue_empty;
+    return (retValue_acc);
+    return (retValue_acc);
+  }
+}
+int get_queued_client(void) {
+  int retValue_acc;
+
+  {
+    retValue_acc = queued_client;
+    return (retValue_acc);
+    return (retValue_acc);
+  }
+}
+int get_queued_email(void) {
+  int retValue_acc;
+
+  {
+    retValue_acc = queued_message;
+    return (retValue_acc);
+    return (retValue_acc);
+  }
+}
+int isKeyPairValid(int publicKey, int privateKey) {
+  int retValue_acc;
+  char const *__restrict __cil_tmp4;
+
+  {
+    {
+      __cil_tmp4 = (char const *__restrict)"keypair valid %d %d";
+      printf(__cil_tmp4, publicKey, privateKey);
+    }
+    if (!publicKey) {
+      retValue_acc = 0;
+      return (retValue_acc);
+    } else {
+      if (!privateKey) {
+        retValue_acc = 0;
+        return (retValue_acc);
+      } else {
+      }
+    }
+    retValue_acc = privateKey == publicKey;
+    return (retValue_acc);
+    return (retValue_acc);
+  }
+}
+void generateKeyPair(int client, int seed) {
+
+  {
+    {
+      setClientPrivateKey(client, seed);
+    }
+    return;
+  }
+}
+void forward(int client, int msg) {
+  int __utac__ad__arg1;
+
+  {
+    {
+      __utac__ad__arg1 = msg;
+      __utac_acc__DecryptForward_spec__1(__utac__ad__arg1);
+      puts("Forwarding message.\n");
+      printMail(msg);
+      queue(client, msg);
+    }
+    return;
+  }
+}
diff --git a/tools/klee/main.cpp b/tools/klee/main.cpp
index e3e87da330..364254f278 100644
--- a/tools/klee/main.cpp
+++ b/tools/klee/main.cpp
@@ -15,7 +15,7 @@
 #include "klee/Core/Context.h"
 #include "klee/Core/Interpreter.h"
 #include "klee/Core/TargetedExecutionReporter.h"
-#include "klee/Expr/Expr.h"
+#include "klee/Module/LocationInfo.h"
 #include "klee/Module/SarifReport.h"
 #include "klee/Module/TargetForest.h"
 #include "klee/Solver/SolverCmdLine.h"
@@ -34,9 +34,7 @@ DISABLE_WARNING_DEPRECATED_DECLARATIONS
 #include "llvm/Bitcode/BitcodeReader.h"
 #include "llvm/IR/Constants.h"
 #include "llvm/IR/IRBuilder.h"
-#include "llvm/IR/InstrTypes.h"
 #include "llvm/IR/Instruction.h"
-#include "llvm/IR/Instructions.h"
 #include "llvm/IR/LLVMContext.h"
 #include "llvm/IR/Type.h"
 #include "llvm/Support/CommandLine.h"
@@ -52,8 +50,8 @@ DISABLE_WARNING_DEPRECATED_DECLARATIONS
 #include "llvm/Support/TargetSelect.h"
 DISABLE_WARNING_POP
 
+#include <csignal>
 #include <dirent.h>
-#include <signal.h>
 #include <sys/stat.h>
 #include <sys/wait.h>
 #include <thread>
@@ -64,6 +62,7 @@ DISABLE_WARNING_POP
 #include <fstream>
 #include <iomanip>
 #include <iterator>
+#include <llvm/IR/InstIterator.h>
 #include <sstream>
 
 using json = nlohmann::json;
@@ -678,13 +677,13 @@ void KleeHandler::processTestCase(const ExecutionState &state,
     }
 
     if (WriteCov) {
-      std::map<const std::string *, std::set<unsigned>> cov;
+      std::map<std::string, std::set<unsigned>> cov;
       m_interpreter->getCoveredLines(state, cov);
       auto f = openTestFile("cov", id);
       if (f) {
         for (const auto &entry : cov) {
           for (const auto &line : entry.second) {
-            *f << *entry.first << ':' << line << '\n';
+            *f << entry.first << ':' << line << '\n';
           }
         }
       }
@@ -1691,13 +1690,19 @@ int main(int argc, char **argv, char **envp) {
   }
 
   llvm::Module *mainModule = loadedUserModules.front().get();
-  std::unique_ptr<InstructionInfoTable> origInfos;
-  std::unique_ptr<llvm::raw_fd_ostream> assemblyFS;
+  FLCtoOpcode origInstructions;
 
   if (UseGuidedSearch == Interpreter::GuidanceKind::ErrorGuidance) {
+    for (const auto &Func : *mainModule) {
+      for (const auto &instr : llvm::instructions(Func)) {
+        auto locationInfo = getLocationInfo(&instr);
+        origInstructions[locationInfo.file][locationInfo.line]
+                        [locationInfo.column]
+                            .insert(instr.getOpcode());
+      }
+    }
+
     std::vector<llvm::Type *> args;
-    origInfos = std::make_unique<InstructionInfoTable>(
-        *mainModule, std::move(assemblyFS), true);
     args.push_back(llvm::Type::getInt32Ty(ctx)); // argc
     args.push_back(llvm::PointerType::get(
         Type::getInt8PtrTy(ctx),
@@ -1716,15 +1721,16 @@ int main(int argc, char **argv, char **envp) {
     EntryPoint = stubEntryPoint;
   }
 
-  std::unordered_set<std::string> mainModuleFunctions;
+  std::set<std::string> mainModuleFunctions;
   for (auto &Function : *mainModule) {
     if (!Function.isDeclaration()) {
       mainModuleFunctions.insert(Function.getName().str());
     }
   }
-  std::unordered_set<std::string> mainModuleGlobals;
-  for (const auto &gv : mainModule->globals())
+  std::set<std::string> mainModuleGlobals;
+  for (const auto &gv : mainModule->globals()) {
     mainModuleGlobals.insert(gv.getName().str());
+  }
 
   const std::string &module_triple = mainModule->getTargetTriple();
   std::string host_triple = llvm::sys::getDefaultTargetTriple();
@@ -1962,8 +1968,9 @@ int main(int argc, char **argv, char **envp) {
   // locale and other data and then calls main.
 
   auto finalModule = interpreter->setModule(
-      loadedUserModules, loadedLibsModules, Opts, mainModuleFunctions,
-      mainModuleGlobals, std::move(origInfos));
+      loadedUserModules, loadedLibsModules, Opts,
+      std::move(mainModuleFunctions), std::move(mainModuleGlobals),
+      std::move(origInstructions));
 
   externalsAndGlobalsCheck(finalModule);
   if (InteractiveMode) {