diff --git a/.clang-tidy b/.clang-tidy
index 73854bf49..a66d8d18b 100644
--- a/.clang-tidy
+++ b/.clang-tidy
@@ -21,6 +21,7 @@ Checks:
   -bugprone-exception-escape
   -bugprone-implicit-widening-of-multiplication-result
   -bugprone-unchecked-optional-access
+  -bugprone-lambda-function-name
   cppcoreguidelines-*
   -cppcoreguidelines-avoid-magic-numbers
   -cppcoreguidelines-avoid-non-const-global-variables
@@ -43,3 +44,5 @@ CheckOptions:
     value: true
   - key: 'cppcoreguidelines-macro-usage.CheckCapsOnly'
     value: true
+  - key: 'cppcoreguidelines-special-member-functions.AllowSoleDefaultDtor'
+    value: true
diff --git a/include/kllvm/ast/AST.h b/include/kllvm/ast/AST.h
index 1fa3896da..f3fd29c3a 100644
--- a/include/kllvm/ast/AST.h
+++ b/include/kllvm/ast/AST.h
@@ -103,22 +103,22 @@ class KORESortVariable : public KORESort {
     return sptr<KORESortVariable>(new KORESortVariable(Name));
   }
 
-  virtual bool isConcrete() const override { return false; }
-  virtual sptr<KORESort> substitute(substitution const &subst) override {
+  bool isConcrete() const override { return false; }
+  sptr<KORESort> substitute(substitution const &subst) override {
     return subst.at(*this);
   }
 
-  virtual void print(std::ostream &Out, unsigned indent = 0) const override;
-  virtual void prettyPrint(std::ostream &Out) const override;
-  virtual void serialize_to(serializer &s) const override;
+  void print(std::ostream &Out, unsigned indent = 0) const override;
+  void prettyPrint(std::ostream &Out) const override;
+  void serialize_to(serializer &s) const override;
 
-  virtual bool operator==(KORESort const &other) const override;
+  bool operator==(KORESort const &other) const override;
 
   std::string const &getName() const { return name; }
 
 private:
-  KORESortVariable(std::string const &Name)
-      : name(Name) { }
+  KORESortVariable(std::string Name)
+      : name(std::move(Name)) { }
 };
 
 enum class SortCategory {
@@ -163,25 +163,25 @@ class KORECompositeSort : public KORESort {
     return sptr<KORECompositeSort>(new KORECompositeSort(Name, Cat));
   }
 
-  std::string const getName() const { return name; }
+  std::string getName() const { return name; }
   ValueType getCategory(KOREDefinition *definition);
   std::string getHook(KOREDefinition *definition) const;
   static ValueType getCategory(std::string const &hookName);
 
-  virtual bool isConcrete() const override;
-  virtual sptr<KORESort> substitute(substitution const &subst) override;
+  bool isConcrete() const override;
+  sptr<KORESort> substitute(substitution const &subst) override;
 
   void addArgument(sptr<KORESort> const &Argument);
-  virtual void print(std::ostream &Out, unsigned indent = 0) const override;
-  virtual void prettyPrint(std::ostream &out) const override;
-  virtual void serialize_to(serializer &s) const override;
-  virtual bool operator==(KORESort const &other) const override;
+  void print(std::ostream &Out, unsigned indent = 0) const override;
+  void prettyPrint(std::ostream &out) const override;
+  void serialize_to(serializer &s) const override;
+  bool operator==(KORESort const &other) const override;
 
   std::vector<sptr<KORESort>> const &getArguments() const { return arguments; }
 
 private:
-  KORECompositeSort(std::string const &Name, ValueType category)
-      : name(Name)
+  KORECompositeSort(std::string Name, ValueType category)
+      : name(std::move(Name))
       , category(category) { }
 };
 
@@ -211,14 +211,14 @@ class KORESymbol {
   /* the first integer in a continuous range representing the tags of all the
      polymorphic instantiations of this symbol. If the symbol has no parameters
      or its parameters are fully specified, firstTag == lastTag. */
-  uint32_t firstTag;
+  uint32_t firstTag{};
   /* the last integer in a continuous range representing the tags of all the
      polymorphic instantiations of this symbol. If the symbol has no parameters
      or its parameters are fully specified, firstTag == lastTag. */
-  uint32_t lastTag;
+  uint32_t lastTag{};
   /* A unique integer representing the layout of the symbol in memory.
      See CreateTerm.cpp for more information about the layout of K terms. */
-  uint16_t layout;
+  uint16_t layout{};
 
 public:
   static ptr<KORESymbol> Create(std::string const &Name) {
@@ -228,23 +228,25 @@ class KORESymbol {
   void addArgument(sptr<KORESort> const &Argument);
   void addFormalArgument(sptr<KORESort> const &Argument);
   void addSort(sptr<KORESort> Sort);
-  void initPatternArguments(void) { arguments.swap(formalArguments); }
+  void initPatternArguments() { arguments.swap(formalArguments); }
 
-  std::string const &getName() const { return name; }
-  std::vector<sptr<KORESort>> const &getArguments() const { return arguments; }
-  std::vector<sptr<KORESort>> const &getFormalArguments() const {
+  [[nodiscard]] std::string const &getName() const { return name; }
+  [[nodiscard]] std::vector<sptr<KORESort>> const &getArguments() const {
+    return arguments;
+  }
+  [[nodiscard]] std::vector<sptr<KORESort>> const &getFormalArguments() const {
     return formalArguments;
   }
-  sptr<KORESort> const getSort() const { return sort; }
+  [[nodiscard]] sptr<KORESort> getSort() const { return sort; }
   sptr<KORESort> getSort() { return sort; }
-  uint32_t getTag() const {
+  [[nodiscard]] uint32_t getTag() const {
     assert(firstTag == lastTag);
     return firstTag;
   }
-  uint32_t getFirstTag() const { return firstTag; }
-  uint32_t getLastTag() const { return lastTag; }
+  [[nodiscard]] uint32_t getFirstTag() const { return firstTag; }
+  [[nodiscard]] uint32_t getLastTag() const { return lastTag; }
   void setTag(uint32_t val) { firstTag = lastTag = val; }
-  uint16_t getLayout() const { return layout; }
+  [[nodiscard]] uint16_t getLayout() const { return layout; }
 
   void print(std::ostream &Out, unsigned indent = 0) const;
   void print(std::ostream &Out, unsigned indent, bool formal) const;
@@ -255,9 +257,9 @@ class KORESymbol {
 
   std::string layoutString(KOREDefinition *) const;
 
-  bool isConcrete() const;
-  bool isPolymorphic() const;
-  bool isBuiltin() const;
+  [[nodiscard]] bool isConcrete() const;
+  [[nodiscard]] bool isPolymorphic() const;
+  [[nodiscard]] bool isBuiltin() const;
 
   /* instantiates this symbol (which should be parsed from a pattern in an
      axiom) with the sorts corresponding to its actual sort parameters after
@@ -273,8 +275,8 @@ class KORESymbol {
   friend KOREDefinition;
 
 private:
-  KORESymbol(std::string const &Name)
-      : name(Name)
+  KORESymbol(std::string Name)
+      : name(std::move(Name))
       , sort(nullptr) { }
 };
 
@@ -282,7 +284,7 @@ struct HashSymbol {
   size_t operator()(kllvm::KORESymbol const &s) const noexcept {
     size_t hash = 0;
     boost::hash_combine(hash, s.name);
-    for (auto &arg : s.arguments) {
+    for (auto const &arg : s.arguments) {
       boost::hash_combine(hash, *arg);
     }
     return hash;
@@ -311,7 +313,7 @@ class KOREVariable {
     return ptr<KOREVariable>(new KOREVariable(Name));
   }
 
-  std::string getName() const;
+  [[nodiscard]] std::string getName() const;
 
   virtual void print(std::ostream &Out, unsigned indent = 0) const;
   virtual void serialize_to(serializer &s) const;
@@ -319,8 +321,8 @@ class KOREVariable {
   virtual ~KOREVariable() = default;
 
 private:
-  KOREVariable(std::string const &Name)
-      : name(Name) { }
+  KOREVariable(std::string Name)
+      : name(std::move(Name)) { }
 };
 
 class KOREVariablePattern;
@@ -356,7 +358,7 @@ struct PrettyPrintData {
   std::set<std::string> comm;
   SubsortMap subsorts;
   // enable coloring
-  bool hasColor;
+  bool hasColor{};
 };
 
 class KOREDeclaration;
@@ -388,7 +390,7 @@ class KOREPattern : public std::enable_shared_from_this<KOREPattern> {
   virtual void markVariables(std::map<std::string, KOREVariablePattern *> &)
       = 0;
 
-  virtual sptr<KORESort> getSort(void) const = 0;
+  virtual sptr<KORESort> getSort() const = 0;
 
   using substitution = std::unordered_map<std::string, sptr<KOREPattern>>;
 
@@ -398,12 +400,12 @@ class KOREPattern : public std::enable_shared_from_this<KOREPattern> {
   virtual void prettyPrint(std::ostream &, PrettyPrintData const &data) const
       = 0;
   virtual sptr<KOREPattern> sortCollections(PrettyPrintData const &data) = 0;
-  std::set<std::string> gatherSingletonVars(void);
-  virtual std::map<std::string, int> gatherVarCounts(void) = 0;
+  std::set<std::string> gatherSingletonVars();
+  virtual std::map<std::string, int> gatherVarCounts() = 0;
   virtual sptr<KOREPattern> filterSubstitution(
       PrettyPrintData const &data, std::set<std::string> const &vars)
       = 0;
-  virtual sptr<KOREPattern> dedupeDisjuncts(void) = 0;
+  virtual sptr<KOREPattern> dedupeDisjuncts() = 0;
   virtual bool matches(
       substitution &subst, SubsortMap const &subsorts,
       SymbolMap const &overloads, sptr<KOREPattern> subject)
@@ -411,7 +413,7 @@ class KOREPattern : public std::enable_shared_from_this<KOREPattern> {
   sptr<KOREPattern> expandMacros(
       SubsortMap const &subsorts, SymbolMap const &overloads,
       std::vector<ptr<KOREDeclaration>> const &axioms, bool reverse);
-  virtual sptr<KOREPattern> unflattenAndOr(void) = 0;
+  virtual sptr<KOREPattern> unflattenAndOr() = 0;
 
   /*
    * Recursively expands productions of the form:
@@ -454,62 +456,55 @@ class KOREVariablePattern : public KOREPattern {
   Create(std::string const &Name, sptr<KORESort> sort) {
     ptr<KOREVariable> Var = KOREVariable::Create(Name);
     return ptr<KOREVariablePattern>(
-        new KOREVariablePattern(std::move(Var), sort));
+        new KOREVariablePattern(std::move(Var), std::move(sort)));
   }
 
   std::string getName() const;
-  virtual sptr<KORESort> getSort() const override { return sort; }
+  sptr<KORESort> getSort() const override { return sort; }
 
-  virtual void print(std::ostream &Out, unsigned indent = 0) const override;
-  virtual void serialize_to(serializer &s) const override;
+  void print(std::ostream &Out, unsigned indent = 0) const override;
+  void serialize_to(serializer &s) const override;
 
-  virtual void
+  void
   markSymbols(std::map<std::string, std::vector<KORESymbol *>> &) override { }
-  virtual void
+  void
   markVariables(std::map<std::string, KOREVariablePattern *> &map) override {
     map.insert({name->getName(), this});
   }
-  virtual sptr<KOREPattern> substitute(substitution const &subst) override {
+  sptr<KOREPattern> substitute(substitution const &subst) override {
     auto val = subst.find(name->getName());
     if (val == subst.end()) {
       return shared_from_this();
     }
     return val->second;
   }
-  virtual sptr<KOREPattern> expandAliases(KOREDefinition *) override {
-    return shared_from_this();
-  }
-  virtual sptr<KOREPattern>
-  sortCollections(PrettyPrintData const &data) override {
+  sptr<KOREPattern> expandAliases(KOREDefinition *) override {
     return shared_from_this();
   }
-  virtual sptr<KOREPattern> dedupeDisjuncts(void) override {
+  sptr<KOREPattern> sortCollections(PrettyPrintData const &data) override {
     return shared_from_this();
   }
-  virtual std::map<std::string, int> gatherVarCounts(void) override {
+  sptr<KOREPattern> dedupeDisjuncts() override { return shared_from_this(); }
+  std::map<std::string, int> gatherVarCounts() override {
     return std::map<std::string, int>{{name->getName(), 1}};
   }
-  virtual sptr<KOREPattern> filterSubstitution(
+  sptr<KOREPattern> filterSubstitution(
       PrettyPrintData const &data, std::set<std::string> const &vars) override {
     return shared_from_this();
   }
 
-  virtual sptr<KOREPattern> desugarAssociative() override {
-    return shared_from_this();
-  }
+  sptr<KOREPattern> desugarAssociative() override { return shared_from_this(); }
 
-  virtual sptr<KOREPattern> unflattenAndOr() override {
-    return shared_from_this();
-  }
+  sptr<KOREPattern> unflattenAndOr() override { return shared_from_this(); }
 
-  virtual bool matches(
+  bool matches(
       substitution &subst, SubsortMap const &, SymbolMap const &,
       sptr<KOREPattern> subject) override;
-  virtual void
+  void
   prettyPrint(std::ostream &out, PrettyPrintData const &data) const override;
 
 private:
-  virtual sptr<KOREPattern> expandMacros(
+  sptr<KOREPattern> expandMacros(
       SubsortMap const &, SymbolMap const &,
       std::vector<ptr<KOREDeclaration>> const &macros, bool reverse,
       std::set<size_t> &appliedRules,
@@ -517,10 +512,9 @@ class KOREVariablePattern : public KOREPattern {
     return shared_from_this();
   }
 
-private:
   KOREVariablePattern(ptr<KOREVariable> Name, sptr<KORESort> Sort)
       : name(std::move(Name))
-      , sort(Sort) { }
+      , sort(std::move(std::move(Sort))) { }
 };
 
 void deallocateSPtrKorePattern(sptr<KOREPattern> pattern);
@@ -563,31 +557,28 @@ class KORECompositePattern : public KOREPattern {
 
   void addArgument(sptr<KOREPattern> const &Argument);
 
-  virtual void print(std::ostream &Out, unsigned indent = 0) const override;
-  virtual void serialize_to(serializer &s) const override;
+  void print(std::ostream &Out, unsigned indent = 0) const override;
+  void serialize_to(serializer &s) const override;
 
-  virtual void
+  void
   prettyPrint(std::ostream &out, PrettyPrintData const &data) const override;
-  virtual void
-  markSymbols(std::map<std::string, std::vector<KORESymbol *>> &) override;
-  virtual void
-  markVariables(std::map<std::string, KOREVariablePattern *> &) override;
-  virtual sptr<KOREPattern> substitute(substitution const &) override;
-  virtual sptr<KOREPattern> expandAliases(KOREDefinition *) override;
-  virtual sptr<KOREPattern>
-  sortCollections(PrettyPrintData const &data) override;
-  virtual sptr<KOREPattern> dedupeDisjuncts(void) override;
-  virtual std::map<std::string, int> gatherVarCounts(void) override;
-  virtual sptr<KOREPattern> desugarAssociative() override;
-  virtual sptr<KOREPattern> unflattenAndOr() override;
-  virtual sptr<KOREPattern> filterSubstitution(
+  void markSymbols(std::map<std::string, std::vector<KORESymbol *>> &) override;
+  void markVariables(std::map<std::string, KOREVariablePattern *> &) override;
+  sptr<KOREPattern> substitute(substitution const &) override;
+  sptr<KOREPattern> expandAliases(KOREDefinition *) override;
+  sptr<KOREPattern> sortCollections(PrettyPrintData const &data) override;
+  sptr<KOREPattern> dedupeDisjuncts() override;
+  std::map<std::string, int> gatherVarCounts() override;
+  sptr<KOREPattern> desugarAssociative() override;
+  sptr<KOREPattern> unflattenAndOr() override;
+  sptr<KOREPattern> filterSubstitution(
       PrettyPrintData const &data, std::set<std::string> const &vars) override;
-  virtual bool matches(
+  bool matches(
       substitution &, SubsortMap const &, SymbolMap const &,
       sptr<KOREPattern>) override;
 
 private:
-  virtual sptr<KOREPattern> expandMacros(
+  sptr<KOREPattern> expandMacros(
       SubsortMap const &, SymbolMap const &,
       std::vector<ptr<KOREDeclaration>> const &macros, bool reverse,
       std::set<size_t> &appliedRules,
@@ -595,7 +586,6 @@ class KORECompositePattern : public KOREPattern {
 
   friend void ::kllvm::deallocateSPtrKorePattern(sptr<KOREPattern> pattern);
 
-private:
   KORECompositePattern(ptr<KORESymbol> Constructor)
       : constructor(std::move(Constructor)) { }
 };
@@ -611,53 +601,46 @@ class KOREStringPattern : public KOREPattern {
 
   std::string getContents() { return contents; }
 
-  virtual void print(std::ostream &Out, unsigned indent = 0) const override;
-  virtual void serialize_to(serializer &s) const override;
-  virtual void
+  void print(std::ostream &Out, unsigned indent = 0) const override;
+  void serialize_to(serializer &s) const override;
+  void
   prettyPrint(std::ostream &out, PrettyPrintData const &data) const override {
     abort();
   }
 
-  virtual void
+  void
   markSymbols(std::map<std::string, std::vector<KORESymbol *>> &) override { }
-  virtual void
-  markVariables(std::map<std::string, KOREVariablePattern *> &) override { }
-  virtual sptr<KORESort> getSort(void) const override { abort(); }
-  virtual sptr<KOREPattern> substitute(substitution const &) override {
-    return shared_from_this();
+  void markVariables(std::map<std::string, KOREVariablePattern *> &) override {
   }
-  virtual sptr<KOREPattern> expandAliases(KOREDefinition *) override {
+  sptr<KORESort> getSort() const override { abort(); }
+  sptr<KOREPattern> substitute(substitution const &) override {
     return shared_from_this();
   }
-  virtual sptr<KOREPattern>
-  sortCollections(PrettyPrintData const &data) override {
+  sptr<KOREPattern> expandAliases(KOREDefinition *) override {
     return shared_from_this();
   }
-  virtual sptr<KOREPattern> dedupeDisjuncts(void) override {
+  sptr<KOREPattern> sortCollections(PrettyPrintData const &data) override {
     return shared_from_this();
   }
-  virtual std::map<std::string, int> gatherVarCounts(void) override {
+  sptr<KOREPattern> dedupeDisjuncts() override { return shared_from_this(); }
+  std::map<std::string, int> gatherVarCounts() override {
     return std::map<std::string, int>{};
   }
 
-  virtual sptr<KOREPattern> desugarAssociative() override {
-    return shared_from_this();
-  }
+  sptr<KOREPattern> desugarAssociative() override { return shared_from_this(); }
 
-  virtual sptr<KOREPattern> unflattenAndOr() override {
-    return shared_from_this();
-  }
+  sptr<KOREPattern> unflattenAndOr() override { return shared_from_this(); }
 
-  virtual sptr<KOREPattern> filterSubstitution(
+  sptr<KOREPattern> filterSubstitution(
       PrettyPrintData const &data, std::set<std::string> const &var) override {
     return shared_from_this();
   }
-  virtual bool matches(
+  bool matches(
       substitution &, SubsortMap const &, SymbolMap const &,
       sptr<KOREPattern> subject) override;
 
 private:
-  virtual sptr<KOREPattern> expandMacros(
+  sptr<KOREPattern> expandMacros(
       SubsortMap const &, SymbolMap const &,
       std::vector<ptr<KOREDeclaration>> const &macros, bool reverse,
       std::set<size_t> &appliedRules,
@@ -665,25 +648,25 @@ class KOREStringPattern : public KOREPattern {
     return shared_from_this();
   }
 
-private:
-  KOREStringPattern(std::string const &Contents)
-      : contents(Contents) { }
+  KOREStringPattern(std::string Contents)
+      : contents(std::move(Contents)) { }
 };
 
 // KOREDeclaration
 class KOREDeclaration {
-protected:
+private:
   attribute_set attributes_;
   std::vector<sptr<KORESortVariable>> objectSortVariables;
 
 public:
   attribute_set &attributes() { return attributes_; }
-  attribute_set const &attributes() const { return attributes_; }
+  [[nodiscard]] attribute_set const &attributes() const { return attributes_; }
 
   void addObjectSortVariable(sptr<KORESortVariable> const &SortVariable);
   virtual void print(std::ostream &Out, unsigned indent = 0) const = 0;
 
-  std::vector<sptr<KORESortVariable>> const &getObjectSortVariables() const {
+  [[nodiscard]] std::vector<sptr<KORESortVariable>> const &
+  getObjectSortVariables() const {
     return objectSortVariables;
   }
   virtual ~KOREDeclaration() = default;
@@ -704,26 +687,27 @@ class KORECompositeSortDeclaration : public KOREDeclaration {
         new KORECompositeSortDeclaration(Name, isHooked));
   }
 
-  std::string getName() const { return sortName; }
-  bool isHooked() const { return _isHooked; }
+  [[nodiscard]] std::string getName() const { return sortName; }
+  [[nodiscard]] bool isHooked() const { return _isHooked; }
 
-  virtual void print(std::ostream &Out, unsigned indent = 0) const override;
+  void print(std::ostream &Out, unsigned indent = 0) const override;
 
 private:
-  KORECompositeSortDeclaration(std::string const &Name, bool _isHooked)
+  KORECompositeSortDeclaration(std::string Name, bool _isHooked)
       : _isHooked(_isHooked)
-      , sortName(Name) { }
+      , sortName(std::move(Name)) { }
 };
 
 class KORESymbolAliasDeclaration : public KOREDeclaration {
-protected:
+private:
   ptr<KORESymbol> symbol;
 
+protected:
   KORESymbolAliasDeclaration(ptr<KORESymbol> Symbol)
       : symbol(std::move(Symbol)) { }
 
 public:
-  KORESymbol *getSymbol() const { return symbol.get(); }
+  [[nodiscard]] KORESymbol *getSymbol() const { return symbol.get(); }
 };
 
 class KORESymbolDeclaration : public KORESymbolAliasDeclaration {
@@ -738,11 +722,11 @@ class KORESymbolDeclaration : public KORESymbolAliasDeclaration {
         new KORESymbolDeclaration(std::move(Sym), isHooked));
   }
 
-  bool isHooked() const { return _isHooked; }
+  [[nodiscard]] bool isHooked() const { return _isHooked; }
 
-  bool isAnywhere() const;
+  [[nodiscard]] bool isAnywhere() const;
 
-  virtual void print(std::ostream &Out, unsigned indent = 0) const override;
+  void print(std::ostream &Out, unsigned indent = 0) const override;
 
 private:
   KORESymbolDeclaration(ptr<KORESymbol> Symbol, bool _isHooked)
@@ -764,11 +748,11 @@ class KOREAliasDeclaration : public KORESymbolAliasDeclaration {
   void addVariables(sptr<KORECompositePattern> variables);
   void addPattern(sptr<KOREPattern> Pattern);
   KOREPattern::substitution getSubstitution(KORECompositePattern *subject);
-  KORECompositePattern *getBoundVariables() const {
+  [[nodiscard]] KORECompositePattern *getBoundVariables() const {
     return boundVariables.get();
   }
   sptr<KOREPattern> &getPattern() { return pattern; }
-  virtual void print(std::ostream &Out, unsigned indent = 0) const override;
+  void print(std::ostream &Out, unsigned indent = 0) const override;
 
 private:
   KOREAliasDeclaration(ptr<KORESymbol> Symbol)
@@ -778,7 +762,7 @@ class KOREAliasDeclaration : public KORESymbolAliasDeclaration {
 class KOREAxiomDeclaration : public KOREDeclaration {
 private:
   sptr<KOREPattern> pattern;
-  unsigned ordinal;
+  unsigned ordinal{};
   bool _isClaim;
 
   KOREAxiomDeclaration(bool isClaim)
@@ -790,20 +774,20 @@ class KOREAxiomDeclaration : public KOREDeclaration {
   }
 
   void addPattern(sptr<KOREPattern> Pattern);
-  virtual void print(std::ostream &Out, unsigned indent = 0) const override;
+  void print(std::ostream &Out, unsigned indent = 0) const override;
 
   /* returns true if the axiom is actually required to be translated to llvm
      and false if it is an axiom pertaining to symbolic execution which is not
      required for concrete execution. Axioms that are not required are elided
      from the definition by KOREDefinition::preprocess. */
-  bool isRequired() const;
-  bool isTopAxiom() const;
-  bool isClaim() const { return _isClaim; }
-  KOREPattern *getRightHandSide() const;
-  std::vector<KOREPattern *> getLeftHandSide() const;
-  KOREPattern *getRequires() const;
-  sptr<KOREPattern> getPattern() const { return pattern; }
-  unsigned getOrdinal() const { return ordinal; }
+  [[nodiscard]] bool isRequired() const;
+  [[nodiscard]] bool isTopAxiom() const;
+  [[nodiscard]] bool isClaim() const { return _isClaim; }
+  [[nodiscard]] KOREPattern *getRightHandSide() const;
+  [[nodiscard]] std::vector<KOREPattern *> getLeftHandSide() const;
+  [[nodiscard]] KOREPattern *getRequires() const;
+  [[nodiscard]] sptr<KOREPattern> getPattern() const { return pattern; }
+  [[nodiscard]] unsigned getOrdinal() const { return ordinal; }
 
   friend KOREDefinition;
 };
@@ -818,13 +802,13 @@ class KOREModuleImportDeclaration : public KOREDeclaration {
         new KOREModuleImportDeclaration(Name));
   }
 
-  std::string const &getModuleName() const { return moduleName; }
+  [[nodiscard]] std::string const &getModuleName() const { return moduleName; }
 
-  virtual void print(std::ostream &Out, unsigned indent = 0) const override;
+  void print(std::ostream &Out, unsigned indent = 0) const override;
 
 private:
-  KOREModuleImportDeclaration(std::string const &Name)
-      : moduleName(Name) { }
+  KOREModuleImportDeclaration(std::string Name)
+      : moduleName(std::move(Name)) { }
 };
 
 // KOREModule
@@ -840,19 +824,20 @@ class KOREModule {
   }
 
   attribute_set &attributes() { return attributes_; }
-  attribute_set const &attributes() const { return attributes_; }
+  [[nodiscard]] attribute_set const &attributes() const { return attributes_; }
 
   void addDeclaration(sptr<KOREDeclaration> Declaration);
   void print(std::ostream &Out, unsigned indent = 0) const;
 
-  std::string const &getName() const { return name; }
-  std::vector<sptr<KOREDeclaration>> const &getDeclarations() const {
+  [[nodiscard]] std::string const &getName() const { return name; }
+  [[nodiscard]] std::vector<sptr<KOREDeclaration>> const &
+  getDeclarations() const {
     return declarations;
   }
 
 private:
-  KOREModule(std::string const &Name)
-      : name(Name) { }
+  KOREModule(std::string Name)
+      : name(std::move(Name)) { }
 };
 
 // KOREDefinition
@@ -903,7 +888,7 @@ class KOREDefinition {
   /* an automatically computed list of all the axioms in the definition */
   std::list<KOREAxiomDeclaration *> axioms;
 
-  KORESymbol *injSymbol;
+  KORESymbol *injSymbol{};
 
   /*
    * Insert symbols into this definition that have knowable labels, but cannot
@@ -914,7 +899,7 @@ class KOREDefinition {
 
 public:
   static ptr<KOREDefinition> Create() {
-    return ptr<KOREDefinition>(new KOREDefinition());
+    return std::make_unique<KOREDefinition>();
   }
 
   /* Preprocesses the definition and prepares it for translation to llvm.
@@ -928,7 +913,7 @@ class KOREDefinition {
   void preprocess();
 
   attribute_set &attributes() { return attributes_; }
-  attribute_set const &attributes() const { return attributes_; }
+  [[nodiscard]] attribute_set const &attributes() const { return attributes_; }
 
   void addModule(sptr<KOREModule> Module);
   void print(std::ostream &Out, unsigned indent = 0) const;
@@ -943,7 +928,7 @@ class KOREDefinition {
    * implement type-safe collections), those user sorts will be returned as
    * well.
    */
-  std::unordered_set<std::string>
+  [[nodiscard]] std::unordered_set<std::string>
   getSortsHookedTo(std::string const &hookName) const;
 
   /*
@@ -954,7 +939,7 @@ class KOREDefinition {
    *
    *   S |-> {T . S is a subsort of T}
    */
-  SubsortMap getSubsorts() const;
+  [[nodiscard]] SubsortMap getSubsorts() const;
 
   /*
    * Build this definition's overload relation from axioms that have the
@@ -964,28 +949,39 @@ class KOREDefinition {
    *
    *  P |-> {Q . P is a more specific overload of Q}
    */
-  SymbolMap getOverloads() const;
+  [[nodiscard]] SymbolMap getOverloads() const;
 
-  std::vector<sptr<KOREModule>> const &getModules() const { return modules; }
-  KORECompositeSortDeclarationMapType const &getSortDeclarations() const {
+  [[nodiscard]] std::vector<sptr<KOREModule>> const &getModules() const {
+    return modules;
+  }
+  [[nodiscard]] KORECompositeSortDeclarationMapType const &
+  getSortDeclarations() const {
     return sortDeclarations;
   }
-  KORESymbolDeclarationMapType const &getSymbolDeclarations() const {
+  [[nodiscard]] KORESymbolDeclarationMapType const &
+  getSymbolDeclarations() const {
     return symbolDeclarations;
   }
-  KOREAliasDeclarationMapType const &getAliasDeclarations() const {
+  [[nodiscard]] KOREAliasDeclarationMapType const &
+  getAliasDeclarations() const {
     return aliasDeclarations;
   }
-  KORESymbolMapType const &getSymbols() const { return objectSymbols; }
-  KORESymbolStringMapType const &getAllSymbols() const {
+  [[nodiscard]] KORESymbolMapType const &getSymbols() const {
+    return objectSymbols;
+  }
+  [[nodiscard]] KORESymbolStringMapType const &getAllSymbols() const {
     return allObjectSymbols;
   }
-  KORECompositeSortMapType const getHookedSorts() const { return hookedSorts; }
-  std::list<KOREAxiomDeclaration *> const &getAxioms() const { return axioms; }
-  KOREAxiomDeclaration *getAxiomByOrdinal(size_t ordinal) const {
+  [[nodiscard]] KORECompositeSortMapType getHookedSorts() const {
+    return hookedSorts;
+  }
+  [[nodiscard]] std::list<KOREAxiomDeclaration *> const &getAxioms() const {
+    return axioms;
+  }
+  [[nodiscard]] KOREAxiomDeclaration *getAxiomByOrdinal(size_t ordinal) const {
     return ordinals.at(ordinal);
   }
-  KORESymbolStringMapType const &getFreshFunctions() const {
+  [[nodiscard]] KORESymbolStringMapType const &getFreshFunctions() const {
     return freshFunctions;
   }
   KORESymbol *getInjSymbol() { return injSymbol; }
diff --git a/include/kllvm/ast/attribute_set.h b/include/kllvm/ast/attribute_set.h
index d8a1f9da9..5421c2a77 100644
--- a/include/kllvm/ast/attribute_set.h
+++ b/include/kllvm/ast/attribute_set.h
@@ -89,7 +89,7 @@ class attribute_set {
    * Returns true if there is any attribute with the given key; the arguments of
    * that attribute are not considered.
    */
-  bool contains(key k) const;
+  [[nodiscard]] bool contains(key k) const;
 
   /**
    * Look up the attribute pattern with the specified key.
@@ -97,7 +97,7 @@ class attribute_set {
    * This lookup is unchecked; use `.contains(k)` first if the attribute may not
    * be present.
    */
-  std::shared_ptr<KORECompositePattern> const &get(key k) const;
+  [[nodiscard]] std::shared_ptr<KORECompositePattern> const &get(key k) const;
 
   /**
    * Look up an attribute with the specified key that has the form:
@@ -106,14 +106,14 @@ class attribute_set {
    *
    * and extract the string data in the pattern's argument.
    */
-  std::string get_string(key k) const;
+  [[nodiscard]] std::string get_string(key k) const;
 
   /**
    * Get the underlying attribute table; this table will allow access to
    * attributes that are not statically whitelisted by the backend, and so
    * should only be used at library boundaries (e.g. in bindings code).
    */
-  storage_t const &underlying() const;
+  [[nodiscard]] storage_t const &underlying() const;
 
   /**
    * Support for iterating over the stored attributes.
@@ -121,8 +121,8 @@ class attribute_set {
    * Code that uses this feature should not dispatch on specific attribute names
    * when iterating; the type-safe interface should be used to do so instead.
    */
-  storage_t::const_iterator begin() const;
-  storage_t::const_iterator end() const;
+  [[nodiscard]] storage_t::const_iterator begin() const;
+  [[nodiscard]] storage_t::const_iterator end() const;
 
 private:
   storage_t attribute_map_ = {};
diff --git a/include/kllvm/ast/pattern_matching.h b/include/kllvm/ast/pattern_matching.h
index c325958e0..133159613 100644
--- a/include/kllvm/ast/pattern_matching.h
+++ b/include/kllvm/ast/pattern_matching.h
@@ -170,7 +170,8 @@ struct match_result {
  */
 class any_ {
 public:
-  match_result match(std::shared_ptr<KOREPattern> const &term) const {
+  [[nodiscard]] static match_result
+  match(std::shared_ptr<KOREPattern> const &term) {
     return {true, nullptr};
   }
 };
@@ -188,20 +189,20 @@ template <typename Inner>
 class subject {
 public:
   subject(Inner inner)
-      : inner_(inner) {
+      : inner_(std::move(inner)) {
     static_assert(
         detail::subject_count_v<Inner> == 0,
         "Cannot construct a subject expression with nested subject terms");
   }
 
-  match_result match(std::shared_ptr<KOREPattern> const &term) const {
+  [[nodiscard]] match_result
+  match(std::shared_ptr<KOREPattern> const &term) const {
     auto inner_result = inner_.match(term);
 
     if (inner_result.matches) {
       return {true, term};
-    } else {
-      return {false, nullptr};
     }
+    return {false, nullptr};
   }
 
 private:
@@ -217,7 +218,7 @@ template <typename... Ts>
 class pattern {
 public:
   pattern(std::string ctor, Ts... children)
-      : constructor_(ctor)
+      : constructor_(std::move(std::move(ctor)))
       , children_(children...) {
     static_assert(
         detail::subject_count_v<std::decay_t<decltype(*this)>> <= 1,
@@ -236,7 +237,8 @@ class pattern {
    * assume that the first child lens to match with a returned subject pattern
    * is the only such lens.
    */
-  match_result match(std::shared_ptr<KOREPattern> const &term) const {
+  [[nodiscard]] match_result
+  match(std::shared_ptr<KOREPattern> const &term) const {
     if (auto composite = std::dynamic_pointer_cast<KORECompositePattern>(term);
         composite && composite->getArguments().size() == arity()
         && composite->getConstructor()->getName() == constructor_) {
@@ -267,7 +269,7 @@ class pattern {
   }
 
 private:
-  constexpr size_t arity() const { return sizeof...(Ts); }
+  [[nodiscard]] constexpr size_t arity() const { return sizeof...(Ts); }
 
   std::string constructor_;
   std::tuple<Ts...> children_;
@@ -293,7 +295,7 @@ class map {
 
   template <typename Func>
   map(Pattern p, Func f)
-      : pattern_(p)
+      : pattern_(std::move(p))
       , func_(f) { }
 
   map(Pattern p)
@@ -303,7 +305,7 @@ class map {
    * Analogous to `match` on a lens type, but with the subject result being a
    * transformed value of type Result rather than a pattern.
    */
-  std::pair<bool, Result>
+  [[nodiscard]] std::pair<bool, Result>
   match(std::shared_ptr<KOREPattern> const &term) const {
     auto [match, subject] = pattern_.match(term);
 
@@ -358,7 +360,7 @@ class match_first {
   match_first(Lens first, Lenses... rest)
       : maps_(make_map(first), make_map(rest)...) { }
 
-  std::pair<bool, result_t>
+  [[nodiscard]] std::pair<bool, result_t>
   match(std::shared_ptr<KOREPattern> const &term) const {
     result_t result = std::nullopt;
     bool any = false;
diff --git a/include/kllvm/binary/ProofTraceParser.h b/include/kllvm/binary/ProofTraceParser.h
index b45508e8b..7d46998e4 100644
--- a/include/kllvm/binary/ProofTraceParser.h
+++ b/include/kllvm/binary/ProofTraceParser.h
@@ -6,6 +6,7 @@
 
 #include <iostream>
 #include <string>
+#include <utility>
 
 namespace kllvm {
 
@@ -13,7 +14,7 @@ namespace detail {
 
 constexpr uint64_t word(uint8_t byte) {
   auto ret = uint64_t{0};
-  for (auto i = 0u; i < sizeof(ret); ++i) {
+  for (auto i = 0U; i < sizeof(ret); ++i) {
     ret <<= 8;
     ret |= byte;
   }
@@ -36,7 +37,7 @@ constexpr uint64_t side_condition_end_sentinel = detail::word(0x33);
 
 class LLVMStepEvent : public std::enable_shared_from_this<LLVMStepEvent> {
 public:
-  virtual void print(std::ostream &Out, unsigned indent = 0u) const = 0;
+  virtual void print(std::ostream &Out, unsigned indent = 0U) const = 0;
   virtual ~LLVMStepEvent() = default;
 };
 
@@ -45,27 +46,30 @@ class LLVMRewriteEvent : public LLVMStepEvent {
   using substitution_t
       = std::map<std::string, std::pair<sptr<KOREPattern>, uint64_t>>;
 
-protected:
+private:
   uint64_t ruleOrdinal;
-  substitution_t substitution;
+  substitution_t substitution{};
 
-  void printSubstitution(std::ostream &Out, unsigned indent = 0u) const;
+protected:
+  void printSubstitution(std::ostream &Out, unsigned indent = 0U) const;
 
 public:
   LLVMRewriteEvent(uint64_t _ruleOrdinal)
-      : ruleOrdinal(_ruleOrdinal)
-      , substitution() { }
+      : ruleOrdinal(_ruleOrdinal) { }
 
-  uint64_t getRuleOrdinal() const { return ruleOrdinal; }
-  substitution_t const &getSubstitution() const { return substitution; }
+  [[nodiscard]] uint64_t getRuleOrdinal() const { return ruleOrdinal; }
+  [[nodiscard]] substitution_t const &getSubstitution() const {
+    return substitution;
+  }
 
   void addSubstitution(
-      std::string const &name, sptr<KOREPattern> term, uint64_t pattern_len) {
+      std::string const &name, sptr<KOREPattern> const &term,
+      uint64_t pattern_len) {
     substitution.insert(
         std::make_pair(name, std::make_pair(term, pattern_len)));
   }
 
-  virtual ~LLVMRewriteEvent() = default;
+  ~LLVMRewriteEvent() override = default;
 };
 
 class LLVMRuleEvent : public LLVMRewriteEvent {
@@ -78,7 +82,7 @@ class LLVMRuleEvent : public LLVMRewriteEvent {
     return sptr<LLVMRuleEvent>(new LLVMRuleEvent(_ruleOrdinal));
   }
 
-  virtual void print(std::ostream &Out, unsigned indent = 0u) const override;
+  void print(std::ostream &Out, unsigned indent = 0U) const override;
 };
 
 class LLVMSideConditionEvent : public LLVMRewriteEvent {
@@ -92,19 +96,18 @@ class LLVMSideConditionEvent : public LLVMRewriteEvent {
         new LLVMSideConditionEvent(_ruleOrdinal));
   }
 
-  virtual void print(std::ostream &Out, unsigned indent = 0u) const override;
+  void print(std::ostream &Out, unsigned indent = 0U) const override;
 };
 
 class LLVMSideConditionEndEvent : public LLVMStepEvent {
 private:
   uint64_t ruleOrdinal;
-  sptr<KOREPattern> korePattern;
-  uint64_t patternLength;
+  sptr<KOREPattern> korePattern{};
+  uint64_t patternLength{0U};
 
   LLVMSideConditionEndEvent(uint64_t _ruleOrdinal)
       : ruleOrdinal(_ruleOrdinal)
-      , korePattern(nullptr)
-      , patternLength(0u) { }
+      , korePattern(nullptr) { }
 
 public:
   static sptr<LLVMSideConditionEndEvent> Create(uint64_t _ruleOrdinal) {
@@ -112,15 +115,15 @@ class LLVMSideConditionEndEvent : public LLVMStepEvent {
         new LLVMSideConditionEndEvent(_ruleOrdinal));
   }
 
-  uint64_t getRuleOrdinal() const { return ruleOrdinal; }
-  sptr<KOREPattern> getKOREPattern() const { return korePattern; }
-  uint64_t getPatternLength() const { return patternLength; }
+  [[nodiscard]] uint64_t getRuleOrdinal() const { return ruleOrdinal; }
+  [[nodiscard]] sptr<KOREPattern> getKOREPattern() const { return korePattern; }
+  [[nodiscard]] uint64_t getPatternLength() const { return patternLength; }
   void setKOREPattern(sptr<KOREPattern> _korePattern, uint64_t _patternLength) {
-    korePattern = _korePattern;
+    korePattern = std::move(_korePattern);
     patternLength = _patternLength;
   }
 
-  virtual void print(std::ostream &Out, unsigned indent = 0u) const override;
+  void print(std::ostream &Out, unsigned indent = 0U) const override;
 };
 
 class LLVMEvent;
@@ -140,13 +143,15 @@ class LLVMFunctionEvent : public LLVMStepEvent {
         new LLVMFunctionEvent(_name, _relativePosition));
   }
 
-  std::string const &getName() const { return name; }
-  std::string const &getRelativePosition() const { return relativePosition; }
-  std::vector<LLVMEvent> const &getArguments() const;
+  [[nodiscard]] std::string const &getName() const { return name; }
+  [[nodiscard]] std::string const &getRelativePosition() const {
+    return relativePosition;
+  }
+  [[nodiscard]] std::vector<LLVMEvent> const &getArguments() const;
 
   void addArgument(LLVMEvent const &argument);
 
-  virtual void print(std::ostream &Out, unsigned indent = 0u) const override;
+  void print(std::ostream &Out, unsigned indent = 0U) const override;
 };
 
 class LLVMHookEvent : public LLVMStepEvent {
@@ -155,7 +160,7 @@ class LLVMHookEvent : public LLVMStepEvent {
   std::string relativePosition;
   std::vector<LLVMEvent> arguments;
   sptr<KOREPattern> korePattern;
-  uint64_t patternLength;
+  uint64_t patternLength{0U};
 
   LLVMHookEvent(std::string _name, std::string _relativePosition);
 
@@ -165,72 +170,78 @@ class LLVMHookEvent : public LLVMStepEvent {
     return sptr<LLVMHookEvent>(new LLVMHookEvent(_name, _relativePosition));
   }
 
-  std::string const &getName() const { return name; }
-  std::string const &getRelativePosition() const { return relativePosition; }
-  std::vector<LLVMEvent> const &getArguments() const { return arguments; }
-  sptr<KOREPattern> getKOREPattern() const { return korePattern; }
-  uint64_t getPatternLength() const { return patternLength; }
+  [[nodiscard]] std::string const &getName() const { return name; }
+  [[nodiscard]] std::string const &getRelativePosition() const {
+    return relativePosition;
+  }
+  [[nodiscard]] std::vector<LLVMEvent> const &getArguments() const {
+    return arguments;
+  }
+  [[nodiscard]] sptr<KOREPattern> getKOREPattern() const { return korePattern; }
+  [[nodiscard]] uint64_t getPatternLength() const { return patternLength; }
   void setKOREPattern(sptr<KOREPattern> _korePattern, uint64_t _patternLength) {
-    korePattern = _korePattern;
+    korePattern = std::move(_korePattern);
     patternLength = _patternLength;
   }
 
   void addArgument(LLVMEvent const &argument);
 
-  virtual void print(std::ostream &Out, unsigned indent = 0u) const override;
+  void print(std::ostream &Out, unsigned indent = 0U) const override;
 };
 
 class LLVMEvent {
 private:
-  bool isStepEvent;
-  sptr<LLVMStepEvent> stepEvent;
-  sptr<KOREPattern> korePattern;
-  uint64_t patternLength;
+  bool isStepEvent{};
+  sptr<LLVMStepEvent> stepEvent{};
+  sptr<KOREPattern> korePattern{};
+  uint64_t patternLength{};
 
 public:
-  bool isStep() const { return isStepEvent; }
-  bool isPattern() const { return !isStep(); }
-  sptr<LLVMStepEvent> getStepEvent() const { return stepEvent; }
-  sptr<KOREPattern> getKOREPattern() const { return korePattern; }
-  uint64_t getPatternLength() const { return patternLength; }
+  [[nodiscard]] bool isStep() const { return isStepEvent; }
+  [[nodiscard]] bool isPattern() const { return !isStep(); }
+  [[nodiscard]] sptr<LLVMStepEvent> getStepEvent() const { return stepEvent; }
+  [[nodiscard]] sptr<KOREPattern> getKOREPattern() const { return korePattern; }
+  [[nodiscard]] uint64_t getPatternLength() const { return patternLength; }
   void setStepEvent(sptr<LLVMStepEvent> _stepEvent) {
     isStepEvent = true;
-    stepEvent = _stepEvent;
+    stepEvent = std::move(_stepEvent);
   }
   void setKOREPattern(sptr<KOREPattern> _korePattern, uint64_t _patternLength) {
     isStepEvent = false;
-    korePattern = _korePattern;
+    korePattern = std::move(_korePattern);
     patternLength = _patternLength;
   }
-  void print(std::ostream &Out, bool isArg, unsigned indent = 0u) const;
+  void print(std::ostream &Out, bool isArg, unsigned indent = 0U) const;
 };
 
 class LLVMRewriteTrace {
 private:
-  uint32_t version;
-  std::vector<LLVMEvent> preTrace;
+  uint32_t version{};
+  std::vector<LLVMEvent> preTrace{};
   LLVMEvent initialConfig;
-  std::vector<LLVMEvent> trace;
+  std::vector<LLVMEvent> trace{};
 
 public:
-  uint32_t getVersion() const { return version; }
-  std::vector<LLVMEvent> const &getPreTrace() const { return preTrace; }
-  LLVMEvent getInitialConfig() const { return initialConfig; }
-  std::vector<LLVMEvent> const &getTrace() const { return trace; }
+  [[nodiscard]] uint32_t getVersion() const { return version; }
+  [[nodiscard]] std::vector<LLVMEvent> const &getPreTrace() const {
+    return preTrace;
+  }
+  [[nodiscard]] LLVMEvent getInitialConfig() const { return initialConfig; }
+  [[nodiscard]] std::vector<LLVMEvent> const &getTrace() const { return trace; }
   void setVersion(uint32_t _version) { version = _version; }
   void setInitialConfig(LLVMEvent _initialConfig) {
-    initialConfig = _initialConfig;
+    initialConfig = std::move(_initialConfig);
   }
 
   void addPreTraceEvent(LLVMEvent const &event) { preTrace.push_back(event); }
   void addTraceEvent(LLVMEvent const &event) { trace.push_back(event); }
 
-  void print(std::ostream &Out, unsigned indent = 0u) const;
+  void print(std::ostream &Out, unsigned indent = 0U) const;
 };
 
 class ProofTraceParser {
 public:
-  static constexpr uint32_t expectedVersion = 5u;
+  static constexpr uint32_t expectedVersion = 5U;
 
 private:
   bool verbose;
@@ -296,7 +307,7 @@ class ProofTraceParser {
 
   template <typename It>
   sptr<KOREPattern> parse_kore_term(It &ptr, It end, uint64_t &pattern_len) {
-    if (std::distance(ptr, end) < 11u) {
+    if (std::distance(ptr, end) < 11U) {
       return nullptr;
     }
     if (detail::read<char>(ptr, end) != '\x7F'
@@ -314,7 +325,8 @@ class ProofTraceParser {
 
     if (std::distance(ptr, end) < pattern_len) {
       return nullptr;
-    } else if (pattern_len > 0 && std::distance(ptr, end) > pattern_len) {
+    }
+    if (pattern_len > 0 && std::distance(ptr, end) > pattern_len) {
       end = std::next(ptr, pattern_len);
     }
 
@@ -333,7 +345,7 @@ class ProofTraceParser {
 
   template <typename It>
   bool parse_header(It &ptr, It end, uint32_t &version) {
-    if (std::distance(ptr, end) < 4u) {
+    if (std::distance(ptr, end) < 4U) {
       return false;
     }
     if (detail::read<char>(ptr, end) != 'H'
@@ -355,13 +367,13 @@ class ProofTraceParser {
   }
 
   template <typename It>
-  bool parse_variable(It &ptr, It end, sptr<LLVMRewriteEvent> event) {
+  bool parse_variable(It &ptr, It end, sptr<LLVMRewriteEvent> const &event) {
     std::string name;
     if (!parse_name(ptr, end, name)) {
       return false;
     }
 
-    uint64_t pattern_len;
+    uint64_t pattern_len = 0;
     auto kore_term = parse_kore_term(ptr, end, pattern_len);
     if (!kore_term) {
       return false;
@@ -390,7 +402,7 @@ class ProofTraceParser {
 
     auto event = LLVMHookEvent::Create(name, location);
 
-    while (std::distance(ptr, end) < 8u
+    while (std::distance(ptr, end) < 8U
            || peek_word(ptr) != hook_result_sentinel) {
       LLVMEvent argument;
       if (!parse_argument(ptr, end, argument)) {
@@ -403,7 +415,7 @@ class ProofTraceParser {
       return nullptr;
     }
 
-    uint64_t pattern_len;
+    uint64_t pattern_len = 0;
     auto kore_term = parse_kore_term(ptr, end, pattern_len);
     if (!kore_term) {
       return nullptr;
@@ -431,7 +443,7 @@ class ProofTraceParser {
 
     auto event = LLVMFunctionEvent::Create(name, location);
 
-    while (std::distance(ptr, end) < 8u
+    while (std::distance(ptr, end) < 8U
            || peek_word(ptr) != function_end_sentinel) {
       LLVMEvent argument;
       if (!parse_argument(ptr, end, argument)) {
@@ -471,12 +483,12 @@ class ProofTraceParser {
       return nullptr;
     }
 
-    uint64_t ordinal;
+    uint64_t ordinal = 0;
     if (!parse_ordinal(ptr, end, ordinal)) {
       return nullptr;
     }
 
-    uint64_t arity;
+    uint64_t arity = 0;
     if (!parse_arity(ptr, end, arity)) {
       return nullptr;
     }
@@ -498,12 +510,12 @@ class ProofTraceParser {
       return nullptr;
     }
 
-    uint64_t ordinal;
+    uint64_t ordinal = 0;
     if (!parse_ordinal(ptr, end, ordinal)) {
       return nullptr;
     }
 
-    uint64_t arity;
+    uint64_t arity = 0;
     if (!parse_arity(ptr, end, arity)) {
       return nullptr;
     }
@@ -525,14 +537,14 @@ class ProofTraceParser {
       return nullptr;
     }
 
-    uint64_t ordinal;
+    uint64_t ordinal = 0;
     if (!parse_ordinal(ptr, end, ordinal)) {
       return nullptr;
     }
 
     auto event = LLVMSideConditionEndEvent::Create(ordinal);
 
-    uint64_t pattern_len;
+    uint64_t pattern_len = 0;
     auto kore_term = parse_kore_term(ptr, end, pattern_len);
     if (!kore_term) {
       return nullptr;
@@ -548,8 +560,8 @@ class ProofTraceParser {
 
   template <typename It>
   bool parse_argument(It &ptr, It end, LLVMEvent &event) {
-    if (std::distance(ptr, end) >= 1u && detail::peek(ptr) == '\x7F') {
-      uint64_t pattern_len;
+    if (std::distance(ptr, end) >= 1U && detail::peek(ptr) == '\x7F') {
+      uint64_t pattern_len = 0;
       auto kore_term = parse_kore_term(ptr, end, pattern_len);
       if (!kore_term) {
         return false;
@@ -559,7 +571,7 @@ class ProofTraceParser {
       return true;
     }
 
-    if (std::distance(ptr, end) < 8u) {
+    if (std::distance(ptr, end) < 8U) {
       return false;
     }
 
@@ -598,7 +610,7 @@ class ProofTraceParser {
 
   template <typename It>
   sptr<LLVMStepEvent> parse_step_event(It &ptr, It end) {
-    if (std::distance(ptr, end) < 8u) {
+    if (std::distance(ptr, end) < 8U) {
       return nullptr;
     }
 
@@ -620,12 +632,12 @@ class ProofTraceParser {
 
   template <typename It>
   bool parse_event(It &ptr, It end, LLVMEvent &event) {
-    if (std::distance(ptr, end) < 8u) {
+    if (std::distance(ptr, end) < 8U) {
       return false;
     }
 
     if (peek_word(ptr) == config_sentinel) {
-      uint64_t pattern_len;
+      uint64_t pattern_len = 0;
       auto config = parse_config(ptr, end, pattern_len);
       if (!config) {
         return false;
@@ -644,13 +656,13 @@ class ProofTraceParser {
 
   template <typename It>
   bool parse_trace(It &ptr, It end, LLVMRewriteTrace &trace) {
-    uint32_t version;
+    uint32_t version = 0;
     if (!parse_header(ptr, end, version)) {
       return false;
     }
     trace.setVersion(version);
 
-    while (std::distance(ptr, end) >= 8u && peek_word(ptr) != config_sentinel) {
+    while (std::distance(ptr, end) >= 8U && peek_word(ptr) != config_sentinel) {
       LLVMEvent event;
       if (!parse_event(ptr, end, event)) {
         return false;
@@ -658,7 +670,7 @@ class ProofTraceParser {
       trace.addPreTraceEvent(event);
     }
 
-    uint64_t pattern_len;
+    uint64_t pattern_len = 0;
     auto config = parse_config(ptr, end, pattern_len);
     if (!config) {
       return false;
diff --git a/include/kllvm/binary/deserializer.h b/include/kllvm/binary/deserializer.h
index d038a5a48..aebece8ad 100644
--- a/include/kllvm/binary/deserializer.h
+++ b/include/kllvm/binary/deserializer.h
@@ -63,7 +63,7 @@ uint64_t read_pattern_size(It &ptr, It end, binary_version version) {
     return read_pattern_size_unchecked(ptr, end);
   }
 
-  return 0u;
+  return 0U;
 }
 
 template <typename It>
@@ -77,28 +77,27 @@ uint64_t read_length(It &ptr, It end, binary_version version, int v1_bytes) {
     }
 
     return ret;
-  } else {
-    uint64_t ret = 0;
-    auto should_continue = true;
-    auto steps = 0;
-
-    while (should_continue) {
-      assert(ptr != end && "Invalid variable-length field");
-      assert(steps < 9 && "No terminating byte in variable-length field");
+  }
+  uint64_t ret = 0;
+  auto should_continue = true;
+  auto steps = 0;
 
-      auto chunk = peek(ptr);
-      auto cont_bit = uint8_t{0x80};
-      should_continue = static_cast<bool>(chunk & cont_bit);
+  while (should_continue) {
+    assert(ptr != end && "Invalid variable-length field");
+    assert(steps < 9 && "No terminating byte in variable-length field");
 
-      chunk = chunk & ~cont_bit;
-      ret = ret | (uint64_t(chunk) << (7 * steps));
+    auto chunk = peek(ptr);
+    auto cont_bit = uint8_t{0x80};
+    should_continue = static_cast<bool>(chunk & cont_bit);
 
-      ++steps;
-      ++ptr;
-    }
+    chunk = chunk & ~cont_bit;
+    ret = ret | (uint64_t(chunk) << (7 * steps));
 
-    return ret;
+    ++steps;
+    ++ptr;
   }
+
+  return ret;
 }
 
 template <typename It>
@@ -120,7 +119,7 @@ std::string read_string(It &ptr, It end, binary_version version) {
     auto begin = ptr - backref;
     auto len = read_length(begin, end, version, 4);
 
-    return std::string((char *)&*begin, (char *)(&*begin + len));
+    return {(char *)&*begin, (char *)(&*begin + len)};
   }
 
   default: throw std::runtime_error("Internal parsing exception");
diff --git a/include/kllvm/binary/serializer.h b/include/kllvm/binary/serializer.h
index e976dbd14..b367aa2fa 100644
--- a/include/kllvm/binary/serializer.h
+++ b/include/kllvm/binary/serializer.h
@@ -52,7 +52,7 @@ class serializer {
   template <
       typename T,
       typename = std::enable_if_t<std::is_fundamental_v<std::decay_t<T>>>>
-  void emit(T t);
+  void emit(T val);
 
   /**
    * Emit a string to the output buffer, using the interning table to either
@@ -81,7 +81,7 @@ class serializer {
    * Return a copy of the bytes currently stored by this serializer as a string,
    * for compatibility with interfaces that don't deal with vectors of bytes.
    */
-  std::string byte_string() const;
+  [[nodiscard]] std::string byte_string() const;
 
   /**
    * Reset the state of the serializer back to its newly-constructed state, with
@@ -94,7 +94,7 @@ class serializer {
    * the topmost arity is dropped.
    */
   void reset_arity_flag();
-  bool use_arity() const { return use_arity_; }
+  [[nodiscard]] bool use_arity() const { return use_arity_; }
 
 private:
   bool use_header_;
diff --git a/include/kllvm/binary/version.h b/include/kllvm/binary/version.h
index ac068ab99..bc8d1055c 100644
--- a/include/kllvm/binary/version.h
+++ b/include/kllvm/binary/version.h
@@ -20,7 +20,7 @@ struct binary_version {
    * Two versions are compatible if they have identical v_major and v_minor
    * components; they may differ in the v_patch component.
    */
-  constexpr bool compatible(binary_version other) const {
+  [[nodiscard]] constexpr bool compatible(binary_version other) const {
     return std::tie(v_major, v_minor) == std::tie(other.v_major, other.v_minor);
   }
 
diff --git a/include/kllvm/codegen/CreateTerm.h b/include/kllvm/codegen/CreateTerm.h
index dfd7cccd1..182127a24 100644
--- a/include/kllvm/codegen/CreateTerm.h
+++ b/include/kllvm/codegen/CreateTerm.h
@@ -20,8 +20,8 @@ class CreateTerm {
   bool isAnywhereOwise;
   std::set<KOREPattern *> staticTerms;
 
-  llvm::Value *
-  alloc_arg(KORECompositePattern *pattern, int idx, std::string locationStack);
+  llvm::Value *alloc_arg(
+      KORECompositePattern *pattern, int idx, std::string const &locationStack);
   llvm::Value *createHook(
       KORECompositePattern *hookAtt, KORECompositePattern *pattern,
       std::string const &locationStack = "0");
@@ -30,7 +30,7 @@ class CreateTerm {
       bool tailcc, std::string const &locationStack = "0");
   llvm::Value *notInjectionCase(
       KORECompositePattern *constructor, llvm::Value *val,
-      std::string locationStack = "0");
+      std::string const &locationStack = "0");
   bool populateStaticSet(KOREPattern *pattern);
   std::pair<llvm::Value *, bool> createAllocation(
       KOREPattern *pattern, std::string const &locationStack = "0");
@@ -44,8 +44,7 @@ class CreateTerm {
       , CurrentBlock(EntryBlock)
       , Module(Module)
       , Ctx(Module->getContext())
-      , isAnywhereOwise(isAnywhereOwise)
-      , staticTerms(std::set<KOREPattern *>()) { }
+      , isAnywhereOwise(isAnywhereOwise) { }
 
   /* adds code to the specified basic block in the specified module which
      constructs an llvm value corresponding to the specified KORE RHS pattern
@@ -73,7 +72,9 @@ class CreateTerm {
       std::vector<llvm::Value *> const &args, bool sret, bool tailcc,
       std::string const &locationStack = "0");
 
-  llvm::BasicBlock *getCurrentBlock() const { return CurrentBlock; }
+  [[nodiscard]] llvm::BasicBlock *getCurrentBlock() const {
+    return CurrentBlock;
+  }
 };
 
 std::string escape(std::string const &str);
diff --git a/include/kllvm/codegen/Debug.h b/include/kllvm/codegen/Debug.h
index dfe501685..1969de6b0 100644
--- a/include/kllvm/codegen/Debug.h
+++ b/include/kllvm/codegen/Debug.h
@@ -18,7 +18,7 @@
 namespace kllvm {
 
 void initDebugInfo(llvm::Module *module, std::string const &filename);
-void finalizeDebugInfo(void);
+void finalizeDebugInfo();
 
 void initDebugFunction(
     std::string const &name, std::string const &linkageName,
@@ -33,23 +33,23 @@ void initDebugGlobal(
     std::string const &name, llvm::DIType *type, llvm::GlobalVariable *var);
 
 llvm::DIType *getDebugType(ValueType type, std::string const &typeName);
-llvm::DIType *getIntDebugType(void);
-llvm::DIType *getLongDebugType(void);
-llvm::DIType *getVoidDebugType(void);
-llvm::DIType *getBoolDebugType(void);
-llvm::DIType *getShortDebugType(void);
+llvm::DIType *getIntDebugType();
+llvm::DIType *getLongDebugType();
+llvm::DIType *getVoidDebugType();
+llvm::DIType *getBoolDebugType();
+llvm::DIType *getShortDebugType();
 llvm::DIType *getPointerDebugType(llvm::DIType *, std::string const &typeName);
 llvm::DIType *
 getArrayDebugType(llvm::DIType *ty, size_t len, llvm::Align align);
-llvm::DIType *getCharPtrDebugType(void);
-llvm::DIType *getCharDebugType(void);
+llvm::DIType *getCharPtrDebugType();
+llvm::DIType *getCharDebugType();
 llvm::DIType *getForwardDecl(std::string const &name);
 
 llvm::DISubroutineType *
 getDebugFunctionType(llvm::Metadata *, std::vector<llvm::Metadata *>);
 
 void setDebugLoc(llvm::Instruction *instr);
-void resetDebugLoc(void);
+void resetDebugLoc();
 
 } // namespace kllvm
 #endif
diff --git a/include/kllvm/codegen/Decision.h b/include/kllvm/codegen/Decision.h
index e09a1df83..33c295909 100644
--- a/include/kllvm/codegen/Decision.h
+++ b/include/kllvm/codegen/Decision.h
@@ -43,18 +43,21 @@ using var_set_type
     = std::unordered_map<var_type, std::unordered_set<IterNextNode *>, HashVar>;
 
 class DecisionNode {
-public:
+private:
   llvm::BasicBlock *cachedCode = nullptr;
   /* completed tracks whether codegen for this DecisionNode has concluded */
   bool completed = false;
 
+public:
+  virtual ~DecisionNode() = default;
+
   virtual void codegen(Decision *d) = 0;
   virtual void preprocess(std::unordered_set<LeafNode *> &) = 0;
   bool beginNode(Decision *d, std::string const &name);
 
   void setCompleted() { completed = true; }
-  bool isCompleted() const { return completed; }
-  uint64_t getChoiceDepth() const { return choiceDepth; }
+  [[nodiscard]] bool isCompleted() const { return completed; }
+  [[nodiscard]] uint64_t getChoiceDepth() const { return choiceDepth; }
 
 private:
   bool preprocessed = false, containsFailNode = false;
@@ -71,15 +74,16 @@ class DecisionNode {
 
 class FailNode : public DecisionNode {
 private:
-  FailNode() { }
+  FailNode() = default;
 
   static FailNode instance;
 
 public:
+  ~FailNode() override = default;
   static FailNode *get() { return &instance; }
 
-  virtual void codegen(Decision *d) { abort(); }
-  virtual void preprocess(std::unordered_set<LeafNode *> &) {
+  void codegen(Decision *d) override { abort(); }
+  void preprocess(std::unordered_set<LeafNode *> &) override {
     containsFailNode = true;
   }
 };
@@ -102,20 +106,22 @@ class DecisionCase {
       KORESymbol *constructor, std::vector<var_type> bindings,
       DecisionNode *child)
       : constructor(constructor)
-      , bindings(bindings)
+      , bindings(std::move(std::move(bindings)))
       , child(child) { }
   DecisionCase(KORESymbol *dv, llvm::APInt literal, DecisionNode *child)
       : constructor(dv)
-      , literal(literal)
+      , literal(std::move(std::move(literal)))
       , child(child) { }
 
-  KORESymbol *getConstructor() const { return constructor; }
-  std::vector<var_type> const &getBindings() const { return bindings; }
-  void addBinding(std::string name, ValueType type, llvm::Module *mod) {
-    bindings.push_back(std::make_pair(name, getParamType(type, mod)));
+  [[nodiscard]] KORESymbol *getConstructor() const { return constructor; }
+  [[nodiscard]] std::vector<var_type> const &getBindings() const {
+    return bindings;
+  }
+  void addBinding(std::string const &name, ValueType type, llvm::Module *mod) {
+    bindings.emplace_back(name, getParamType(type, mod));
   }
   llvm::APInt getLiteral() const { return literal; }
-  DecisionNode *getChild() const { return child; }
+  [[nodiscard]] DecisionNode *getChild() const { return child; }
 };
 
 class SwitchNode : public DecisionNode {
@@ -128,29 +134,33 @@ class SwitchNode : public DecisionNode {
 
   bool isCheckNull;
 
-  SwitchNode(std::string const &name, llvm::Type *type, bool isCheckNull)
-      : name(name)
+  SwitchNode(std::string name, llvm::Type *type, bool isCheckNull)
+      : name(std::move(name))
       , type(type)
       , isCheckNull(isCheckNull) { }
 
 public:
-  void addCase(DecisionCase _case) { cases.push_back(_case); }
+  ~SwitchNode() override = default;
+  void addCase(DecisionCase const &_case) { cases.push_back(_case); }
 
   static SwitchNode *
   Create(std::string const &name, llvm::Type *type, bool isCheckNull) {
     return new SwitchNode(name, type, isCheckNull);
   }
 
-  std::string getName() const { return name; }
-  llvm::Type *getType() const { return type; }
-  std::vector<DecisionCase> const &getCases() const { return cases; }
+  [[nodiscard]] std::string getName() const { return name; }
+  [[nodiscard]] llvm::Type *getType() const { return type; }
+  [[nodiscard]] std::vector<DecisionCase> const &getCases() const {
+    return cases;
+  }
 
-  virtual void codegen(Decision *d);
-  virtual void preprocess(std::unordered_set<LeafNode *> &leaves) {
-    if (preprocessed)
+  void codegen(Decision *d) override;
+  void preprocess(std::unordered_set<LeafNode *> &leaves) override {
+    if (preprocessed) {
       return;
+    }
     bool hasDefault = false;
-    for (auto _case : cases) {
+    for (auto const &_case : cases) {
       _case.getChild()->preprocess(leaves);
       containsFailNode = containsFailNode || _case.getChild()->containsFailNode;
       hasDefault = hasDefault || _case.getConstructor() == nullptr;
@@ -172,25 +182,27 @@ class MakePatternNode : public DecisionNode {
   DecisionNode *child;
 
   MakePatternNode(
-      std::string const &name, llvm::Type *type, KOREPattern *pattern,
+      std::string name, llvm::Type *type, KOREPattern *pattern,
       std::vector<var_type> &uses, DecisionNode *child)
-      : name(name)
+      : name(std::move(name))
       , type(type)
       , pattern(pattern)
       , uses(uses)
       , child(child) { }
 
 public:
+  ~MakePatternNode() override = default;
   static MakePatternNode *Create(
       std::string const &name, llvm::Type *type, KOREPattern *pattern,
       std::vector<var_type> &uses, DecisionNode *child) {
     return new MakePatternNode(name, type, pattern, uses, child);
   }
 
-  virtual void codegen(Decision *d);
-  virtual void preprocess(std::unordered_set<LeafNode *> &leaves) {
-    if (preprocessed)
+  void codegen(Decision *d) override;
+  void preprocess(std::unordered_set<LeafNode *> &leaves) override {
+    if (preprocessed) {
       return;
+    }
     child->preprocess(leaves);
     containsFailNode = containsFailNode || child->containsFailNode;
     choiceDepth = child->choiceDepth;
@@ -212,32 +224,35 @@ class FunctionNode : public DecisionNode {
   llvm::Type *type;
 
   FunctionNode(
-      std::string const &name, std::string const &function, DecisionNode *child,
+      std::string name, std::string function, DecisionNode *child,
       ValueType cat, llvm::Type *type)
-      : name(name)
-      , function(function)
+      : name(std::move(name))
+      , function(std::move(function))
       , child(child)
       , cat(cat)
       , type(type) { }
 
 public:
+  ~FunctionNode() override = default;
   static FunctionNode *Create(
       std::string const &name, std::string const &function, DecisionNode *child,
       ValueType cat, llvm::Type *type) {
     return new FunctionNode(name, function, child, cat, type);
   }
 
-  std::vector<std::pair<var_type, ValueType>> const &getBindings() const {
+  [[nodiscard]] std::vector<std::pair<var_type, ValueType>> const &
+  getBindings() const {
     return bindings;
   }
-  void addBinding(std::string name, ValueType type, llvm::Module *mod) {
+  void addBinding(std::string const &name, ValueType type, llvm::Module *mod) {
     bindings.push_back({{name, getParamType(type, mod)}, type});
   }
 
-  virtual void codegen(Decision *d);
-  virtual void preprocess(std::unordered_set<LeafNode *> &leaves) {
-    if (preprocessed)
+  void codegen(Decision *d) override;
+  void preprocess(std::unordered_set<LeafNode *> &leaves) override {
+    if (preprocessed) {
       return;
+    }
     child->preprocess(leaves);
     containsFailNode = containsFailNode || child->containsFailNode;
     choiceDepth = child->choiceDepth;
@@ -256,25 +271,29 @@ class LeafNode : public DecisionNode {
 
   DecisionNode *child = nullptr;
 
-  LeafNode(std::string const &name)
-      : name(name) { }
+  LeafNode(std::string name)
+      : name(std::move(name)) { }
 
 public:
+  ~LeafNode() override = default;
   static LeafNode *Create(std::string const &name) {
     return new LeafNode(name);
   }
 
-  std::vector<var_type> const &getBindings() const { return bindings; }
-  void addBinding(std::string name, ValueType type, llvm::Module *mod) {
-    bindings.push_back(std::make_pair(name, getParamType(type, mod)));
+  [[nodiscard]] std::vector<var_type> const &getBindings() const {
+    return bindings;
+  }
+  void addBinding(std::string const &name, ValueType type, llvm::Module *mod) {
+    bindings.emplace_back(name, getParamType(type, mod));
   }
   void setChild(DecisionNode *child) { this->child = child; }
 
-  virtual void codegen(Decision *d);
-  virtual void preprocess(std::unordered_set<LeafNode *> &leaves) {
+  void codegen(Decision *d) override;
+  void preprocess(std::unordered_set<LeafNode *> &leaves) override {
     if (child != nullptr) {
-      if (preprocessed)
+      if (preprocessed) {
         return;
+      }
       leaves.insert(this);
       child->preprocess(leaves);
       containsFailNode = containsFailNode || child->containsFailNode;
@@ -296,17 +315,17 @@ class MakeIteratorNode : public DecisionNode {
   DecisionNode *child;
 
   MakeIteratorNode(
-      std::string const &collection, llvm::Type *collectionType,
-      std::string const &name, llvm::Type *type, std::string const &hookName,
-      DecisionNode *child)
-      : collection(collection)
+      std::string collection, llvm::Type *collectionType, std::string name,
+      llvm::Type *type, std::string hookName, DecisionNode *child)
+      : collection(std::move(collection))
       , collectionType(collectionType)
-      , name(name)
+      , name(std::move(name))
       , type(type)
-      , hookName(hookName)
+      , hookName(std::move(hookName))
       , child(child) { }
 
 public:
+  ~MakeIteratorNode() override = default;
   static MakeIteratorNode *Create(
       std::string const &collection, llvm::Type *collectionType,
       std::string const &name, llvm::Type *type, std::string const &hookName,
@@ -315,10 +334,11 @@ class MakeIteratorNode : public DecisionNode {
         collection, collectionType, name, type, hookName, child);
   }
 
-  virtual void codegen(Decision *d);
-  virtual void preprocess(std::unordered_set<LeafNode *> &leaves) {
-    if (preprocessed)
+  void codegen(Decision *d) override;
+  void preprocess(std::unordered_set<LeafNode *> &leaves) override {
+    if (preprocessed) {
       return;
+    }
     child->preprocess(leaves);
     containsFailNode = containsFailNode || child->containsFailNode;
     choiceDepth = child->choiceDepth;
@@ -336,17 +356,17 @@ class IterNextNode : public DecisionNode {
   DecisionNode *child;
 
   IterNextNode(
-      std::string const &iterator, llvm::Type *iteratorType,
-      std::string const &binding, llvm::Type *bindingType,
-      std::string const &hookName, DecisionNode *child)
-      : iterator(iterator)
+      std::string iterator, llvm::Type *iteratorType, std::string binding,
+      llvm::Type *bindingType, std::string hookName, DecisionNode *child)
+      : iterator(std::move(iterator))
       , iteratorType(iteratorType)
-      , binding(binding)
+      , binding(std::move(binding))
       , bindingType(bindingType)
-      , hookName(hookName)
+      , hookName(std::move(hookName))
       , child(child) { }
 
 public:
+  ~IterNextNode() override = default;
   static IterNextNode *Create(
       std::string const &iterator, llvm::Type *iteratorType,
       std::string const &binding, llvm::Type *bindingType,
@@ -355,10 +375,11 @@ class IterNextNode : public DecisionNode {
         iterator, iteratorType, binding, bindingType, hookName, child);
   }
 
-  virtual void codegen(Decision *d);
-  virtual void preprocess(std::unordered_set<LeafNode *> &leaves) {
-    if (preprocessed)
+  void codegen(Decision *d) override;
+  void preprocess(std::unordered_set<LeafNode *> &leaves) override {
+    if (preprocessed) {
       return;
+    }
     child->preprocess(leaves);
     containsFailNode = containsFailNode || child->containsFailNode;
     choiceDepth = child->choiceDepth + 1;
@@ -374,14 +395,14 @@ class Decision {
   llvm::IndirectBrInst *FailJump;
   llvm::AllocaInst *ChoiceBuffer;
   llvm::AllocaInst *ChoiceDepth;
-  llvm::BasicBlock *ChoiceBlock;
+  llvm::BasicBlock *ChoiceBlock{nullptr};
   llvm::Module *Module;
   llvm::LLVMContext &Ctx;
   ValueType Cat;
   llvm::PHINode *FailSubject, *FailPattern, *FailSort;
   llvm::AllocaInst *HasSearchResults;
 
-  std::map<var_type, llvm::AllocaInst *> symbols;
+  std::map<var_type, llvm::AllocaInst *> symbols{};
 
   llvm::Value *getTag(llvm::Value *);
 
@@ -404,7 +425,6 @@ class Decision {
       , FailJump(FailJump)
       , ChoiceBuffer(ChoiceBuffer)
       , ChoiceDepth(ChoiceDepth)
-      , ChoiceBlock(nullptr)
       , Module(Module)
       , Ctx(Module->getContext())
       , Cat(Cat)
diff --git a/include/kllvm/codegen/DecisionParser.h b/include/kllvm/codegen/DecisionParser.h
index 8bbf98dae..dbb095866 100644
--- a/include/kllvm/codegen/DecisionParser.h
+++ b/include/kllvm/codegen/DecisionParser.h
@@ -15,11 +15,11 @@ class DecisionNode;
 
 struct Residual {
   std::string occurrence;
-  KOREPattern *pattern;
+  KOREPattern *pattern{};
 };
 
 struct PartialStep {
-  DecisionNode *dt;
+  DecisionNode *dt{};
   std::vector<Residual> residuals;
 };
 
diff --git a/include/kllvm/codegen/ProofEvent.h b/include/kllvm/codegen/ProofEvent.h
index e83a7d2f2..3ff7e49d2 100644
--- a/include/kllvm/codegen/ProofEvent.h
+++ b/include/kllvm/codegen/ProofEvent.h
@@ -129,7 +129,6 @@ class ProofEvent {
       KOREAxiomDeclaration *axiom, llvm::Value *check_result,
       llvm::BasicBlock *current_block);
 
-public:
   ProofEvent(KOREDefinition *Definition, llvm::Module *Module)
       : Definition(Definition)
       , Module(Module)
diff --git a/include/kllvm/parser/KOREParser.h b/include/kllvm/parser/KOREParser.h
index 97c2d141f..bedd5b9f9 100644
--- a/include/kllvm/parser/KOREParser.h
+++ b/include/kllvm/parser/KOREParser.h
@@ -10,12 +10,11 @@
 #include <utility>
 #include <vector>
 
-namespace kllvm {
-namespace parser {
+namespace kllvm::parser {
 
 class KOREParser {
 public:
-  KOREParser(std::string filename)
+  KOREParser(std::string const &filename)
       : scanner(KOREScanner(filename))
       , loc(location(filename)) { }
 
@@ -74,7 +73,6 @@ class KOREParser {
   } buffer = {"", token::EMPTY};
 };
 
-} // end namespace parser
-} // end namespace kllvm
+} // namespace kllvm::parser
 
 #endif // KOREPARSER_
diff --git a/include/kllvm/parser/KOREScanner.h b/include/kllvm/parser/KOREScanner.h
index 96193b79f..afb746c7f 100644
--- a/include/kllvm/parser/KOREScanner.h
+++ b/include/kllvm/parser/KOREScanner.h
@@ -3,8 +3,7 @@
 
 #include "kllvm/parser/location.h"
 
-namespace kllvm {
-namespace parser {
+namespace kllvm::parser {
 
 enum class token {
   EMPTY,
@@ -41,7 +40,13 @@ class KOREScanner {
 
   friend class KOREParser;
 
-  typedef void *yyscan_t;
+  using yyscan_t = void *;
+
+  KOREScanner(KOREScanner const &other) = delete;
+  KOREScanner &operator=(KOREScanner const &other) = delete;
+
+  KOREScanner(KOREScanner &&other) = delete;
+  KOREScanner &operator=(KOREScanner &&other) = delete;
 
 private:
   yyscan_t scanner;
@@ -56,7 +61,6 @@ class KOREScanner {
   std::string stringBuffer;
 };
 
-} // end namespace parser
-} // end namespace kllvm
+} // namespace kllvm::parser
 
 #endif // KORESCANNER_H
diff --git a/include/kllvm/parser/location.h b/include/kllvm/parser/location.h
index f86f6a23f..1ef58f1cf 100644
--- a/include/kllvm/parser/location.h
+++ b/include/kllvm/parser/location.h
@@ -3,8 +3,7 @@
 
 #include <string>
 
-namespace kllvm {
-namespace parser {
+namespace kllvm::parser {
 
 class position {
 public:
@@ -41,7 +40,7 @@ operator<<(std::basic_ostream<YYChar> &ostr, position const &pos) {
 
 class location {
 public:
-  location(std::string filename)
+  location(std::string const &filename)
       : begin({filename, 1, 1})
       , end({filename, 1, 1}) { }
 
@@ -60,16 +59,16 @@ std::basic_ostream<YYChar> &
 operator<<(std::basic_ostream<YYChar> &ostr, location const &loc) {
   unsigned end_col = 0 < loc.end.column ? loc.end.column - 1 : 0;
   ostr << loc.begin;
-  if (loc.begin.filename != loc.end.filename)
+  if (loc.begin.filename != loc.end.filename) {
     ostr << '-' << loc.end.filename << ':' << loc.end.line << '.' << end_col;
-  else if (loc.begin.line < loc.end.line)
+  } else if (loc.begin.line < loc.end.line) {
     ostr << '-' << loc.end.line << '.' << end_col;
-  else if (loc.begin.column < end_col)
+  } else if (loc.begin.column < end_col) {
     ostr << '-' << end_col;
+  }
   return ostr;
 }
 
-} // namespace parser
-} // namespace kllvm
+} // namespace kllvm::parser
 
 #endif
diff --git a/include/kllvm/util/temporary_file.h b/include/kllvm/util/temporary_file.h
index a32fdfb25..73d367deb 100644
--- a/include/kllvm/util/temporary_file.h
+++ b/include/kllvm/util/temporary_file.h
@@ -29,6 +29,12 @@ class temporary_file {
     }
   }
 
+  temporary_file(temporary_file const &other) = delete;
+  temporary_file &operator=(temporary_file const &other) = delete;
+
+  temporary_file(temporary_file &&other) = delete;
+  temporary_file &operator=(temporary_file &&other) = delete;
+
   ~temporary_file() {
     close(temp_fd);
     remove(temp_filename.data());
@@ -40,7 +46,7 @@ class temporary_file {
 
   FILE *file_pointer(std::string const &mode = "r") {
     if (!temp_c_file) {
-      auto f = fdopen(temp_fd, mode.data());
+      auto *f = fdopen(temp_fd, mode.data());
       if (f) {
         temp_c_file = std::unique_ptr<FILE, deleter>(f);
       } else {
diff --git a/include/runtime/arena.h b/include/runtime/arena.h
index cf5f1b207..9880c341a 100644
--- a/include/runtime/arena.h
+++ b/include/runtime/arena.h
@@ -19,18 +19,18 @@ struct arena {
   char allocation_semispace_id;
 };
 
-typedef struct {
+using memory_block_header = struct {
   char *next_block;
   char *next_superblock;
   char semispace;
-} memory_block_header;
+};
 
 // Macro to define a new arena with the given ID. Supports IDs ranging from 0 to
 // 127.
 #define REGISTER_ARENA(name, id)                                               \
-  static struct arena name = {.allocation_semispace_id = id}
+  static struct arena name = {.allocation_semispace_id = (id)}
 
-#define mem_block_start(ptr)                                                   \
+#define MEM_BLOCK_START(ptr)                                                   \
   ((char *)(((uintptr_t)(ptr)-1) & ~(BLOCK_SIZE - 1)))
 
 // Resets the given arena.
diff --git a/include/runtime/collect.h b/include/runtime/collect.h
index be023c07c..b729e9b46 100644
--- a/include/runtime/collect.h
+++ b/include/runtime/collect.h
@@ -8,7 +8,7 @@
 
 struct block;
 using block_iterator = std::vector<block **>::iterator;
-typedef std::pair<block_iterator, block_iterator> (*BlockEnumerator)(void);
+using BlockEnumerator = std::pair<block_iterator, block_iterator> (*)();
 
 // This function is exported to the rest of the runtime to enable registering
 // more GC roots other than the top cell of the configuration.
@@ -27,7 +27,6 @@ using set_impl = set::iterator::tree_t;
 
 extern "C" {
 extern size_t numBytesLiveAtCollection[1 << AGE_WIDTH];
-bool during_gc(void);
 extern bool collect_old;
 size_t get_size(uint64_t, uint16_t);
 void migrate_once(block **);
@@ -41,26 +40,26 @@ void koreCollect(void **, uint8_t, layoutitem *);
 }
 
 #ifdef GC_DBG
-#define initialize_age()                                                       \
+#define INITIALIZE_AGE()                                                       \
   uint64_t age = (hdr & AGE_MASK) >> AGE_OFFSET;                               \
   uint64_t oldAge = age;
 #define increment_age()                                                        \
   if (age < ((1 << AGE_WIDTH) - 1))                                            \
     age++;
-#define migrate_header(block)                                                  \
+#define MIGRATE_HEADER(block)                                                  \
   block->h.hdr |= shouldPromote ? NOT_YOUNG_OBJECT_BIT : 0;                    \
   block->h.hdr &= ~AGE_MASK;                                                   \
   block->h.hdr |= age << AGE_OFFSET
 #else
-#define initialize_age() bool age = hdr & AGE_MASK;
+#define INITIALIZE_AGE() bool age = hdr & AGE_MASK;
 #define increment_age()
-#define migrate_header(block)                                                  \
+#define MIGRATE_HEADER(block)                                                  \
   block->h.hdr |= shouldPromote ? NOT_YOUNG_OBJECT_BIT : AGE_MASK
 #endif
 
-#define initialize_migrate()                                                   \
+#define INITIALIZE_MIGRATE()                                                   \
   bool isInYoungGen = is_in_young_gen_hdr(hdr);                                \
-  initialize_age() bool isInOldGen = is_in_old_gen_hdr(hdr);                   \
+  INITIALIZE_AGE() bool isInOldGen = is_in_old_gen_hdr(hdr);                   \
   if (!(isInYoungGen || (isInOldGen && collect_old))) {                        \
     return;                                                                    \
   }                                                                            \
diff --git a/include/runtime/collections/RBTree.h b/include/runtime/collections/RBTree.h
index a87f2149a..07ed3d5c8 100644
--- a/include/runtime/collections/RBTree.h
+++ b/include/runtime/collections/RBTree.h
@@ -42,13 +42,12 @@ class RBTree {
   // Virtual class, for a node of the red-black tree.
   struct Node {
     Node(Color c)
-        : c_(c)
-        , s_(0) { }
+        : c_(c) { }
     Color c_; // Color of this tree Node
-    size_t s_; // Size of the tree with root Node
+    size_t s_{0}; // Size of the tree with root Node
 
     // Return true if this object is a Leaf.
-    virtual bool is_leaf() const = 0;
+    [[nodiscard]] virtual bool is_leaf() const = 0;
     virtual ~Node() = default;
   };
 
@@ -60,8 +59,8 @@ class RBTree {
         : Node(c) {
       assert(c == Color::B || c == Color::BB);
     }
-    virtual bool is_leaf() const override { return true; }
-    virtual ~Leaf() = default;
+    [[nodiscard]] bool is_leaf() const override { return true; }
+    ~Leaf() override = default;
   };
 
   // An internal node of the red-black tree.
@@ -72,17 +71,17 @@ class RBTree {
         Color c, std::shared_ptr<Node> lft, T key, V val,
         std::shared_ptr<Node> rgt)
         : Node(c)
-        , lft_(lft)
+        , lft_(std::move(lft))
         , data_(key, val)
-        , rgt_(rgt) {
+        , rgt_(std::move(rgt)) {
       this->s_ = 1 + lft_->s_ + rgt_->s_;
     }
     std::shared_ptr<Node> lft_; // Left child
     std::pair<T, V> data_; // data_.first: Node key. data_.second: Node value.
     std::shared_ptr<Node> rgt_; // Right child
 
-    virtual bool is_leaf() const override { return false; }
-    virtual ~InternalNode() = default;
+    [[nodiscard]] bool is_leaf() const override { return false; }
+    ~InternalNode() override = default;
   };
 
   // Create an empty red-black tree, with the specified color. Only B and BB
@@ -100,16 +99,16 @@ class RBTree {
   }
 
   explicit RBTree(std::shared_ptr<Node> node)
-      : root_(node) { }
+      : root_(std::move(node)) { }
 
   // Return this Node's color when it is not empty.
-  Color root_color() const {
+  [[nodiscard]] Color root_color() const {
     assert(!empty());
     return root_->c_;
   }
 
   // Return this Node's color when it is empty.
-  Color leaf_color() const {
+  [[nodiscard]] Color leaf_color() const {
     assert(empty());
     return root_->c_;
   }
@@ -132,27 +131,27 @@ class RBTree {
   }
 
   // Return true if this tree is empty.
-  bool empty() const { return root_->is_leaf(); }
+  [[nodiscard]] bool empty() const { return root_->is_leaf(); }
 
   // Return the key stored in the root Node of this tree.
-  T const &root_key() const {
+  [[nodiscard]] T const &root_key() const {
     assert(!empty());
-    InternalNode const *r = static_cast<InternalNode const *>(root_.get());
+    auto const *r = static_cast<InternalNode const *>(root_.get());
     return r->data_.first;
   }
 
   // Return the value stored in the root Node of this tree.
-  V const &root_val() const {
+  [[nodiscard]] V const &root_val() const {
     assert(!empty());
-    InternalNode const *r = static_cast<InternalNode const *>(root_.get());
+    auto const *r = static_cast<InternalNode const *>(root_.get());
     return r->data_.second;
   }
 
   // Return a const reference to the data (key-value pair) stored in the root
   // Node of this tree.
-  std::pair<T, V> const &root_data() const {
+  [[nodiscard]] std::pair<T, V> const &root_data() const {
     assert(!empty());
-    InternalNode const *r = static_cast<InternalNode const *>(root_.get());
+    auto const *r = static_cast<InternalNode const *>(root_.get());
     return r->data_;
   }
 
@@ -172,71 +171,73 @@ class RBTree {
   // this tree.
   std::pair<T, V> &root_data_mutable() {
     assert(!empty());
-    InternalNode *r = static_cast<InternalNode *>(root_.get());
+    auto *r = static_cast<InternalNode *>(root_.get());
     return r->data_;
   }
 
   // Return the left subtree of this tree.
-  RBTree left() const {
+  [[nodiscard]] RBTree left() const {
     assert(!empty());
-    InternalNode const *r = static_cast<InternalNode const *>(root_.get());
+    auto const *r = static_cast<InternalNode const *>(root_.get());
     return RBTree(r->lft_);
   }
 
   // Return the right subtree of this tree.
-  RBTree right() const {
+  [[nodiscard]] RBTree right() const {
     assert(!empty());
-    InternalNode const *r = static_cast<InternalNode const *>(root_.get());
+    auto const *r = static_cast<InternalNode const *>(root_.get());
     return RBTree(r->rgt_);
   }
 
   // Return the size of this tree, i.e., the number of non-leaf nodes.
-  size_t size() const { return root_->s_; }
+  [[nodiscard]] size_t size() const { return root_->s_; }
 
   // Return true if key x is found in this tree. Otherwise, return false.
-  bool contains(T const &x) const {
+  [[nodiscard]] bool contains(T const &x) const {
     if (empty()) {
       return false;
     }
     T const &y = root_key();
     if (x < y) {
       return left().contains(x);
-    } else if (y < x) {
+    }
+    if (y < x) {
       return right().contains(x);
-    } else {
-      return true;
     }
+    return true;
   }
 
   // Return the corresponding value if key x is found in this tree. Otherwise,
   // throw an exception.
-  V const &at(T const &x) const {
+  [[nodiscard]] V const &at(T const &x) const {
     if (empty()) {
       KLLVM_HOOK_INVALID_ARGUMENT("Key not found for treemap lookup");
     }
     T const &y = root_key();
     if (x < y) {
       return left().at(x);
-    } else if (y < x) {
+    }
+    if (y < x) {
       return right().at(x);
-    } else {
-      return root_val();
     }
+    return root_val();
   }
 
   // Return a new red-black tree that contains all key-value pairs in this
   // tree plus the key value pair [x -> v]. If key x was already in this tree,
   // key x will be associated with value v in the resulting tree instead.
-  RBTree inserted(T const &x, V const &v) const { return ins(x, v).blacken(); }
+  [[nodiscard]] RBTree inserted(T const &x, V const &v) const {
+    return ins(x, v).blacken();
+  }
 
   // Return a new red-black tree that does not contain the key-value pair for
   // key x, if any.
-  RBTree deleted(T const &x) const { return redden().del(x); }
+  [[nodiscard]] RBTree deleted(T const &x) const { return redden().del(x); }
 
   // Return a red-black tree that is the concatenation of this tree and tree t.
   // Throw an exception if the sets of the keys in this tree and tree t are not
   // disjoint.
-  RBTree concat(RBTree const &t) const {
+  [[nodiscard]] RBTree concat(RBTree const &t) const {
     RBTree res = *this;
     for_each(t, [&res, this](T const &x, V const &v) {
       if (!contains(x)) {
@@ -279,7 +280,7 @@ class RBTree {
   // exception if the black invariant does not hold for this tree.
   // Black invariant: Every path from root to empty node contains the same
   // number of black nodes.
-  int assert_black_invariant() const {
+  int assert_black_invariant() const { // NOLINT(*-use-nodiscard)
     if (empty()) {
       return 0;
     }
@@ -310,7 +311,7 @@ class RBTree {
   }
 
 private:
-  RBTree ins(T const &x, V const &v) const {
+  [[nodiscard]] RBTree ins(T const &x, V const &v) const {
     assert(!empty(Color::BB));
 
     if (empty(Color::B)) {
@@ -322,24 +323,23 @@ class RBTree {
     if (c == Color::B) {
       if (x < ykey) {
         return balance(Color::B, left().ins(x, v), ykey, yval, right());
-      } else if (ykey < x) {
-        return balance(Color::B, left(), ykey, yval, right().ins(x, v));
-      } else {
-        return RBTree(Color::B, left(), x, v, right());
       }
-    } else {
-      assert(c == Color::R);
-      if (x < ykey) {
-        return RBTree(Color::R, left().ins(x, v), ykey, yval, right());
-      } else if (ykey < x) {
-        return RBTree(Color::R, left(), ykey, yval, right().ins(x, v));
-      } else {
-        return RBTree(Color::R, left(), x, v, right());
+      if (ykey < x) {
+        return balance(Color::B, left(), ykey, yval, right().ins(x, v));
       }
+      return RBTree(Color::B, left(), x, v, right());
+    }
+    assert(c == Color::R);
+    if (x < ykey) {
+      return RBTree(Color::R, left().ins(x, v), ykey, yval, right());
     }
+    if (ykey < x) {
+      return RBTree(Color::R, left(), ykey, yval, right().ins(x, v));
+    }
+    return RBTree(Color::R, left(), x, v, right());
   }
 
-  RBTree del(T const &x) const {
+  [[nodiscard]] RBTree del(T const &x) const {
     assert(!empty(Color::BB));
 
     // Black leaf
@@ -352,17 +352,15 @@ class RBTree {
     if (singleton(Color::R)) {
       if (ykey == x) {
         return RBTree();
-      } else {
-        return *this;
       }
+      return *this;
     }
     // Singleton black node
     if (singleton(Color::B)) {
       if (ykey == x) {
         return RBTree(Color::BB);
-      } else {
-        return *this;
       }
+      return *this;
     }
     // Black root with single left red child
     if (only_left_child(Color::B, Color::R)) {
@@ -370,26 +368,26 @@ class RBTree {
       assert(left().right().empty(Color::B));
       if (ykey == x) {
         return left().paint(Color::B);
-      } else if (ykey < x) {
-        return *this;
-      } else { // ykey > x
-        return RBTree(Color::B, left().del(x), ykey, yval, RBTree());
       }
+      if (ykey < x) {
+        return *this;
+      } // ykey > x
+      return RBTree(Color::B, left().del(x), ykey, yval, RBTree());
     }
     // Otherwise
     if (ykey < x) {
       return rotate(root_color(), left(), ykey, yval, right().del(x));
-    } else if (ykey > x) {
-      return rotate(root_color(), left().del(x), ykey, yval, right());
-    } else { // ykey == x
-      T minkey;
-      V minval;
-      RBTree new_right = right().min_delete(minkey, minval);
-      return rotate(root_color(), left(), minkey, minval, new_right);
     }
+    if (ykey > x) {
+      return rotate(root_color(), left().del(x), ykey, yval, right());
+    } // ykey == x
+    T minkey;
+    V minval;
+    RBTree new_right = right().min_delete(minkey, minval);
+    return rotate(root_color(), left(), minkey, minval, new_right);
   }
 
-  RBTree redden() const {
+  [[nodiscard]] RBTree redden() const {
     if (non_empty(Color::B) && left().non_empty(Color::B)
         && right().non_empty(Color::B)) {
       return paint(Color::R);
@@ -400,7 +398,7 @@ class RBTree {
     return *this;
   }
 
-  RBTree blacken() const {
+  [[nodiscard]] RBTree blacken() const {
     if (doubled_left() || doubled_right()) {
       return paint(Color::B);
     }
@@ -436,6 +434,7 @@ class RBTree {
     return rotate(root_color(), new_left, root_key(), root_val(), right());
   }
 
+  // NOLINTNEXTLINE(*-cognitive-complexity)
   static RBTree rotate(
       Color c, RBTree const &lft, T const &x, V const &v, RBTree const &rgt) {
     // Red parent
@@ -444,42 +443,53 @@ class RBTree {
         return balance(
             Color::B, RBTree(Color::R, lft.paint(Color::B), x, v, rgt.left()),
             rgt.root_key(), rgt.root_val(), rgt.right());
-      } else if (lft.empty(Color::BB) && rgt.non_empty(Color::B)) {
+      }
+      if (lft.empty(Color::BB) && rgt.non_empty(Color::B)) {
         return balance(
             Color::B, RBTree(Color::R, RBTree(), x, v, rgt.left()),
             rgt.root_key(), rgt.root_val(), rgt.right());
-      } else if (lft.non_empty(Color::B) && rgt.non_empty(Color::BB)) {
+      }
+      if (lft.non_empty(Color::B) && rgt.non_empty(Color::BB)) {
         return balance(
             Color::B, lft.left(), lft.root_key(), lft.root_val(),
             RBTree(Color::R, lft.right(), x, v, rgt.paint(Color::B)));
-      } else if (lft.non_empty(Color::B) && rgt.empty(Color::BB)) {
+      }
+      if (lft.non_empty(Color::B) && rgt.empty(Color::BB)) {
         return balance(
             Color::B, lft.left(), lft.root_key(), lft.root_val(),
             RBTree(Color::R, lft.right(), x, v, RBTree()));
-      } else {
-        return RBTree(c, lft, x, v, rgt);
       }
+
+      return RBTree(c, lft, x, v, rgt);
     }
+
     // Black parent
     if (c == Color::B) {
       if (lft.non_empty(Color::BB) && rgt.non_empty(Color::B)) {
         return balance(
             Color::BB, RBTree(Color::R, lft.paint(Color::B), x, v, rgt.left()),
             rgt.root_key(), rgt.root_val(), rgt.right());
-      } else if (lft.empty(Color::BB) && rgt.non_empty(Color::B)) {
+      }
+
+      if (lft.empty(Color::BB) && rgt.non_empty(Color::B)) {
         return balance(
             Color::BB, RBTree(Color::R, RBTree(), x, v, rgt.left()),
             rgt.root_key(), rgt.root_val(), rgt.right());
-      } else if (lft.non_empty(Color::B) && rgt.non_empty(Color::BB)) {
+      }
+
+      if (lft.non_empty(Color::B) && rgt.non_empty(Color::BB)) {
         return balance(
             Color::BB, lft.left(), lft.root_key(), lft.root_val(),
             RBTree(Color::R, lft.right(), x, v, rgt.paint(Color::B)));
-      } else if (lft.non_empty(Color::B) && rgt.empty(Color::BB)) {
+      }
+
+      if (lft.non_empty(Color::B) && rgt.empty(Color::BB)) {
         return balance(
             Color::BB, lft.left(), lft.root_key(), lft.root_val(),
             RBTree(Color::R, lft.right(), x, v, RBTree()));
-      } else if (
-          lft.non_empty(Color::BB) && rgt.non_empty(Color::R)
+      }
+
+      if (lft.non_empty(Color::BB) && rgt.non_empty(Color::R)
           && rgt.left().non_empty(Color::B)) {
         return RBTree(
             Color::B,
@@ -489,8 +499,9 @@ class RBTree {
                 rgt.left().root_key(), rgt.left().root_val(),
                 rgt.left().right()),
             rgt.root_key(), rgt.root_val(), rgt.right());
-      } else if (
-          lft.empty(Color::BB) && rgt.non_empty(Color::R)
+      }
+
+      if (lft.empty(Color::BB) && rgt.non_empty(Color::R)
           && rgt.left().non_empty(Color::B)) {
         return RBTree(
             Color::B,
@@ -499,8 +510,9 @@ class RBTree {
                 rgt.left().root_key(), rgt.left().root_val(),
                 rgt.left().right()),
             rgt.root_key(), rgt.root_val(), rgt.right());
-      } else if (
-          lft.non_empty(Color::R) && lft.right().non_empty(Color::B)
+      }
+
+      if (lft.non_empty(Color::R) && lft.right().non_empty(Color::B)
           && rgt.non_empty(Color::BB)) {
         return RBTree(
             Color::B, lft.left(), lft.root_key(), lft.root_val(),
@@ -509,8 +521,9 @@ class RBTree {
                 lft.right().root_val(),
                 RBTree(
                     Color::R, lft.right().right(), x, v, rgt.paint(Color::B))));
-      } else if (
-          lft.non_empty(Color::R) && lft.right().non_empty(Color::B)
+      }
+
+      if (lft.non_empty(Color::R) && lft.right().non_empty(Color::B)
           && rgt.empty(Color::BB)) {
         return RBTree(
             Color::B, lft.left(), lft.root_key(), lft.root_val(),
@@ -518,9 +531,9 @@ class RBTree {
                 Color::B, lft.right().left(), lft.right().root_key(),
                 lft.right().root_val(),
                 RBTree(Color::R, lft.right().right(), x, v, RBTree())));
-      } else {
-        return RBTree(c, lft, x, v, rgt);
       }
+
+      return RBTree(c, lft, x, v, rgt);
     }
     // Otherwise
     return RBTree(c, lft, x, v, rgt);
@@ -533,7 +546,9 @@ class RBTree {
       return RBTree(
           minus_one_color(c), lft.left().paint(Color::B), lft.root_key(),
           lft.root_val(), RBTree(Color::B, lft.right(), x, v, rgt));
-    } else if (lft.doubled_right()) {
+    }
+
+    if (lft.doubled_right()) {
       return RBTree(
           minus_one_color(c),
           RBTree(
@@ -541,57 +556,66 @@ class RBTree {
               lft.right().left()),
           lft.right().root_key(), lft.right().root_val(),
           RBTree(Color::B, lft.right().right(), x, v, rgt));
-    } else if (rgt.doubled_left()) {
+    }
+
+    if (rgt.doubled_left()) {
       return RBTree(
           minus_one_color(c), RBTree(Color::B, lft, x, v, rgt.left().left()),
           rgt.left().root_key(), rgt.left().root_val(),
           RBTree(
               Color::B, rgt.left().right(), rgt.root_key(), rgt.root_val(),
               rgt.right()));
-    } else if (rgt.doubled_right()) {
+    }
+
+    if (rgt.doubled_right()) {
       return RBTree(
           minus_one_color(c), RBTree(Color::B, lft, x, v, rgt.left()),
           rgt.root_key(), rgt.root_val(), rgt.right().paint(Color::B));
-    } else {
-      return RBTree(c, lft, x, v, rgt);
     }
+
+    return RBTree(c, lft, x, v, rgt);
   }
 
-  bool empty(Color c) const { return empty() && leaf_color() == c; }
+  [[nodiscard]] bool empty(Color c) const {
+    return empty() && leaf_color() == c;
+  }
 
-  bool non_empty(Color c) const { return !empty() && root_color() == c; }
+  [[nodiscard]] bool non_empty(Color c) const {
+    return !empty() && root_color() == c;
+  }
 
-  bool singleton(Color c) const {
+  [[nodiscard]] bool singleton(Color c) const {
     return !empty() && root_color() == c && left().empty(Color::B)
            && right().empty(Color::B);
   }
 
-  bool only_left_child(Color parent_color, Color child_color) const {
+  [[nodiscard]] bool
+  only_left_child(Color parent_color, Color child_color) const {
     return !empty() && root_color() == parent_color && !left().empty()
            && left().root_color() == child_color && right().empty(Color::B);
   }
 
-  bool only_right_child(Color parent_color, Color child_color) const {
+  [[nodiscard]] bool
+  only_right_child(Color parent_color, Color child_color) const {
     return !empty() && root_color() == parent_color && left().empty(Color::B)
            && !right().empty() && right().root_color() == child_color;
   }
 
-  bool doubled_left() const {
+  [[nodiscard]] bool doubled_left() const {
     return !empty() && root_color() == Color::R && !left().empty()
            && left().root_color() == Color::R;
   }
 
-  bool doubled_right() const {
+  [[nodiscard]] bool doubled_right() const {
     return !empty() && root_color() == Color::R && !right().empty()
            && right().root_color() == Color::R;
   }
 
-  RBTree paint(Color c) const {
+  [[nodiscard]] RBTree paint(Color c) const {
     assert(!empty());
     return RBTree(c, left(), root_key(), root_val(), right());
   }
 
-private:
   std::shared_ptr<Node> root_;
 };
 
diff --git a/include/runtime/collections/rangemap.h b/include/runtime/collections/rangemap.h
index 44ebd37e3..f0cfd75b0 100644
--- a/include/runtime/collections/rangemap.h
+++ b/include/runtime/collections/rangemap.h
@@ -10,6 +10,7 @@
 #include <optional>
 #include <stack>
 #include <stdexcept>
+#include <utility>
 #include <vector>
 
 namespace rng_map {
@@ -51,10 +52,10 @@ class Range {
   T &end_mutable() { return end_; }
 
   // Getter for the start of this range.
-  T const &start() const { return start_; }
+  [[nodiscard]] T const &start() const { return start_; }
 
   // Getter for the end of this range.
-  T const &end() const { return end_; }
+  [[nodiscard]] T const &end() const { return end_; }
 
   // The following methods define the ordering for objects of class Range.
   // Operator < is used to subsequently define >, ==, <=, >=, and !=.
@@ -78,16 +79,19 @@ class Range {
   }
 
   // Returns true if this range contains k.
-  bool contains(T const &k) const { return k >= start_ && k < end_; }
+  [[nodiscard]] bool contains(T const &k) const {
+    return k >= start_ && k < end_;
+  }
 
   // Returns true if this range is empty.
-  bool empty() const { return start_ >= end_; }
+  [[nodiscard]] bool empty() const { return start_ >= end_; }
 
   // Returns true if this range overlaps with range r.
-  bool overlaps(Range const &r) const {
+  [[nodiscard]] bool overlaps(Range const &r) const {
     if (r.end_ <= start_) {
       return false;
-    } else if (end_ <= r.start_) {
+    }
+    if (end_ <= r.start_) {
       return false;
     }
     return true;
@@ -95,10 +99,11 @@ class Range {
 
   // Returns true if this range and range r overlap or are adjacent, i.e.,
   // share a bound, either inclusive or exclusive.
-  bool is_relevant(Range const &r) const {
+  [[nodiscard]] bool is_relevant(Range const &r) const {
     if (r.end_ < start_) {
       return false;
-    } else if (end_ < r.start_) {
+    }
+    if (end_ < r.start_) {
       return false;
     }
     return true;
@@ -118,9 +123,9 @@ class RangeMap {
   // Create a rangemap on top of a red-black tree that uses ranges as keys.
   // The red black tree should already be a well-formed rangemap.
   RangeMap(rb_tree::RBTree<Range<T>, V> t)
-      : treemap_(t) { }
+      : treemap_(std::move(t)) { }
 
-  std::optional<std::pair<Range<T>, V>>
+  [[nodiscard]] std::optional<std::pair<Range<T>, V>>
   get_key_value(rb_tree::RBTree<Range<T>, V> const &t, T const &k) const {
     if (t.empty()) {
       return std::nullopt;
@@ -139,30 +144,34 @@ class RangeMap {
 
   // Return true if range r partially or completely overlaps with any range
   // stored in the ordered map t that is passed as an argument.
-  bool
+  [[nodiscard]] bool
   overlaps(rb_tree::RBTree<Range<T>, V> const &t, Range<T> const &r) const {
     if (t.empty()) {
       return false;
     }
+
     T const &start = r.start();
     T const &end = r.end();
     T const &rstart = t.root_key().start();
     T const &rend = t.root_key().end();
+
     if (rend <= start) {
       // The root is to the left of range r, possibly adjacent but not
       // overlapping. Continue looking for overlapping ranges to the right of
       // root.
       return overlaps(t.right(), r);
-    } else if (end <= rstart) {
+    }
+
+    if (end <= rstart) {
       // The root is to the right of range r, possibly adjacent but not
       // overlapping. Continue looking for overlapping ranges to the left of
       // root.
       return overlaps(t.left(), r);
-    } else {
-      // In any other case, range r somehow overlaps with root, either partially
-      // or completely.
-      return true;
     }
+
+    // In any other case, range r somehow overlaps with root, either partially
+    // or completely.
+    return true;
   }
 
   // Gather all <Range<T>, V> pairs in t that are overlapping or directly
@@ -268,7 +277,8 @@ class RangeMap {
   // Return the intersection ranges of this rangemap and rangemap m, i.e. all
   // ranges in this rangemap that overlap (fully or partially) with ranges in m
   // and are mapped to the same value in both rangemaps.
-  std::vector<Range<T>> get_intersection_ranges(RangeMap const &m) const {
+  [[nodiscard]] std::vector<Range<T>>
+  get_intersection_ranges(RangeMap const &m) const {
     std::vector<std::pair<Range<T>, V>> r1;
     for_each(treemap_, [&r1](Range<T> const &x, V const &v) {
       r1.emplace_back(std::make_pair(x, v));
@@ -319,20 +329,24 @@ class RangeMap {
   }
 
   // Getter for the rb-tree underlying this rangemap.
-  rb_tree::RBTree<Range<T>, V> treemap() const { return treemap_; }
+  [[nodiscard]] rb_tree::RBTree<Range<T>, V> treemap() const {
+    return treemap_;
+  }
 
   // Return the number of key ranges in the map.
-  size_t size() const { return treemap_.size(); }
+  [[nodiscard]] size_t size() const { return treemap_.size(); }
 
   // Returns true if this rangemap is empty.
-  bool empty() const { return treemap_.size() == 0; }
+  [[nodiscard]] bool empty() const { return treemap_.empty(); }
 
   // Return true if a range in this map contains the key k.
-  bool contains(T const &k) const { return get_key_value(k).has_value(); }
+  [[nodiscard]] bool contains(T const &k) const {
+    return get_key_value(k).has_value();
+  }
 
   // If the key k is contained in any range in this map, return the value
   // associated with k.
-  std::optional<V> get_value(T const &k) const {
+  [[nodiscard]] std::optional<V> get_value(T const &k) const {
     auto opt = get_key_value(k);
     if (opt.has_value()) {
       return opt.value().second;
@@ -342,7 +356,8 @@ class RangeMap {
 
   // If the key k is contained in any range in this map, return the key range-
   // value pair associated with k.
-  std::optional<std::pair<Range<T>, V>> get_key_value(T const &k) const {
+  [[nodiscard]] std::optional<std::pair<Range<T>, V>>
+  get_key_value(T const &k) const {
     return get_key_value(treemap_, k);
   }
 
@@ -355,7 +370,7 @@ class RangeMap {
      * existing range mapping to the same value, then the ranges will be
      * coalesced into a single contiguous range in the resulting map.
      */
-  RangeMap inserted(Range<T> const &r, V const &v) const {
+  [[nodiscard]] RangeMap inserted(Range<T> const &r, V const &v) const {
     // Empty ranges do not make sense here.
     if (r.empty()) {
       KLLVM_HOOK_INVALID_ARGUMENT("Insert empty range in range map");
@@ -418,7 +433,7 @@ class RangeMap {
      * map, then the boundaries of these ranges are adjusted in the resulting
      * map so that they do not overlap with the removed range.
      */
-  RangeMap deleted(Range<T> const &r) const {
+  [[nodiscard]] RangeMap deleted(Range<T> const &r) const {
     // Empty ranges do not make sense here.
     if (r.empty()) {
       KLLVM_HOOK_INVALID_ARGUMENT("Delete empty range from range map");
@@ -452,7 +467,9 @@ class RangeMap {
 
   // Return true if range r partially or completely overlaps with any key range
   // stored in this rangemap.
-  bool overlaps(Range<T> const &r) const { return overlaps(treemap_, r); }
+  [[nodiscard]] bool overlaps(Range<T> const &r) const {
+    return overlaps(treemap_, r);
+  }
 
   // Print this rangemap to output stream os.
   void print(std::ostream &os) const {
@@ -466,7 +483,7 @@ class RangeMap {
   // Return a rangemap that is the concatenation of this rangemap and rangemap
   // m. Throw an exception if any of the key ranges in this rangemap overlaps
   // with any of the key ranges in rangemap m.
-  RangeMap concat(RangeMap const &m) const {
+  [[nodiscard]] RangeMap concat(RangeMap const &m) const {
     RangeMap res = *this;
     for_each(m.treemap_, [&res, this](Range<T> const &x, V const &v) {
       if (!overlaps(x)) {
@@ -484,7 +501,7 @@ class RangeMap {
   // key range-value pairs whose keys are contained in ranges in both A and B
   // and are mapped to the same value. Then, we perform A - A^B, and return the
   // map resulting from deleting these ranges from A.
-  RangeMap difference(RangeMap const &m) const {
+  [[nodiscard]] RangeMap difference(RangeMap const &m) const {
     // Compute the intersection of this rangemap and m.
     std::vector<Range<T>> intersect = get_intersection_ranges(m);
     // Delete all collected intersection ranges from this rangemap.
@@ -498,7 +515,7 @@ class RangeMap {
   // Return true if this rangemap is included in rangemap m, i.e. all key
   // range-value pairs contained in this rangemap whose keys are also contained
   // in key ranges in m and are mapped to the same value.
-  bool inclusion(RangeMap const &m) const {
+  [[nodiscard]] bool inclusion(RangeMap const &m) const {
     // Compute the intersection of this rangemap and m.
     std::vector<Range<T>> intersect = get_intersection_ranges(m);
     // Compare the intersection ranges with this rangemap's ranges.
@@ -528,8 +545,11 @@ class RangeMap {
 template <class T, class V>
 class AbstractRangeMapIterator {
 
+private:
+  std::stack<rb_tree::RBTree<Range<T>, V>> stack_{};
+
 protected:
-  std::stack<rb_tree::RBTree<Range<T>, V>> stack_;
+  [[nodiscard]] auto const &stack() const { return stack_; }
 
   void update_stack_state(rb_tree::RBTree<Range<T>, V> const &t) {
     rb_tree::RBTree<Range<T>, V> tmp = t;
@@ -553,28 +573,26 @@ class AbstractRangeMapIterator {
   }
 
   // Return true if there are more elements in the underlying rangemap.
-  bool has_next() const { return !stack_.empty(); }
+  [[nodiscard]] bool has_next() const { return !stack_.empty(); }
 };
 
 template <class T, class V>
 class ConstRangeMapIterator : public AbstractRangeMapIterator<T, V> {
 
 public:
-  using AbstractRangeMapIterator<T, V>::stack_;
-
   // Create an iterator over rangemap m.
   ConstRangeMapIterator(RangeMap<T, V> m)
       : AbstractRangeMapIterator<T, V>(m) { }
 
   // Dereference operator.
   std::pair<Range<T>, V> const &operator*() const {
-    rb_tree::RBTree<Range<T>, V> const &t = stack_.top();
+    rb_tree::RBTree<Range<T>, V> const &t = this->stack().top();
     return t.root_data();
   }
 
   // Member access (arrow) operator.
   std::pair<Range<T>, V> const *operator->() const {
-    rb_tree::RBTree<Range<T>, V> const &t = stack_.top();
+    rb_tree::RBTree<Range<T>, V> const &t = this->stack().top();
     return &t.root_data();
   }
 };
diff --git a/include/runtime/header.h b/include/runtime/header.h
index f1cdc03dc..520bcaabc 100644
--- a/include/runtime/header.h
+++ b/include/runtime/header.h
@@ -28,26 +28,26 @@
 struct MatchLog {
   enum { SUCCESS = 0, FUNCTION, FAIL } kind;
 
-  char const *function;
-  char const *debugName;
-  void *result;
-  std::vector<void *> args;
-
-  char const *pattern;
-  void *subject;
-  char const *sort;
+  char const *function{};
+  char const *debugName{};
+  void *result{};
+  std::vector<void *> args{};
+
+  char const *pattern{};
+  void *subject{};
+  char const *sort{};
 };
 
 // the actual length is equal to the block header with the gc bits masked out.
 
-#define struct_base(struct_type, member_name, member_addr)                     \
+#define STRUCT_BASE(struct_type, member_name, member_addr)                     \
   ((struct_type *)((char *)(member_addr)-offsetof(struct_type, member_name)))
 
 extern "C" {
 // llvm: blockheader = type { i64 }
-typedef struct blockheader {
+using blockheader = struct blockheader {
   uint64_t hdr;
-} blockheader;
+};
 
 // A value b of type block* is either a constant or a block.
 // if (((uintptr_t)b) & 3) == 3, then it is a bound variable and
@@ -56,53 +56,53 @@ typedef struct blockheader {
 // of the symbol. Otherwise, if ((uintptr_t)b) & 1 == 0 then it is a pointer to
 // a block.
 // llvm: block = type { %blockheader, [0 x i64 *] }
-typedef struct block {
+using block = struct block {
   blockheader h;
   uint64_t *children[];
-} block;
+};
 
 // llvm: string = type { %blockheader, [0 x i8] }
-typedef struct string {
+using string = struct string {
   blockheader h;
   char data[];
-} string;
+};
 
 // llvm: stringbuffer = type { i64, i64, %string* }
-typedef struct stringbuffer {
+using stringbuffer = struct stringbuffer {
   blockheader h;
   uint64_t strlen;
   string *contents;
-} stringbuffer;
+};
 
-typedef struct mpz_hdr {
+using mpz_hdr = struct mpz_hdr {
   blockheader h;
   mpz_t i;
-} mpz_hdr;
+};
 
-typedef struct floating {
+using floating = struct floating {
   uint64_t exp; // number of bits in exponent range
   mpfr_t f;
-} floating;
+};
 
-typedef struct floating_hdr {
+using floating_hdr = struct floating_hdr {
   blockheader h;
   floating f;
-} floating_hdr;
+};
 
-typedef struct layoutitem {
+using layoutitem = struct layoutitem {
   uint64_t offset;
   uint16_t cat;
-} layoutitem;
+};
 
-typedef struct layout {
+using layout = struct layout {
   uint8_t nargs;
   layoutitem *args;
-} layout;
+};
 
-typedef struct {
+using writer = struct {
   FILE *file;
   stringbuffer *buffer;
-} writer;
+};
 
 bool hook_KEQUAL_lt(block *, block *);
 bool hook_KEQUAL_eq(block *, block *);
@@ -191,9 +191,11 @@ __attribute__((always_inline)) constexpr bool is_heap_block(T const *s) {
 
 class KElem {
 public:
-  KElem() { this->elem = NULL; }
+  KElem()
+      : elem(nullptr) { }
 
-  KElem(block *elem) { this->elem = elem; }
+  KElem(block *elem)
+      : elem(elem) { }
 
   bool operator==(KElem const &other) const {
     return hook_KEQUAL_eq(this->elem, other.elem);
@@ -222,11 +224,10 @@ struct kore_alloc_heap {
   static void *allocate(size_t size, Tags...) {
     if (during_gc()) {
       return ::operator new(size);
-    } else {
-      string *result = (string *)koreAllocToken(size + sizeof(blockheader));
-      init_with_len(result, size);
-      return result->data;
     }
+    auto *result = (string *)koreAllocToken(size + sizeof(blockheader));
+    init_with_len(result, size);
+    return result->data;
   }
 
   static void deallocate(size_t size, void *data) {
@@ -250,41 +251,40 @@ using list = immer::flex_vector<
     KElem, immer::memory_policy<
                immer::heap_policy<kore_alloc_heap>, immer::no_refcount_policy,
                immer::no_lock_policy>>;
-using map = immer::map<
-    KElem, KElem, HashBlock, std::equal_to<KElem>, list::memory_policy>;
-using set
-    = immer::set<KElem, HashBlock, std::equal_to<KElem>, list::memory_policy>;
+using map
+    = immer::map<KElem, KElem, HashBlock, std::equal_to<>, list::memory_policy>;
+using set = immer::set<KElem, HashBlock, std::equal_to<>, list::memory_policy>;
 using rangemap = rng_map::RangeMap<KElem, KElem>;
 
-typedef struct mapiter {
-  map::iterator curr;
-  map *map_item;
-} mapiter;
-
-typedef struct setiter {
-  set::iterator curr;
-  set *set_item;
-} setiter;
-
-typedef floating *SortFloat;
-typedef mpz_ptr SortInt;
-typedef string *SortString;
-typedef string *SortBytes;
-typedef stringbuffer *SortStringBuffer;
-typedef block *SortK;
-typedef block *SortKItem;
-typedef block *SortIOInt;
-typedef block *SortIOFile;
-typedef block *SortIOString;
-typedef block *SortJSON;
-typedef block *SortEndianness;
-typedef block *SortSignedness;
-typedef block *SortFFIType;
-typedef list *SortList;
-typedef map *SortMap;
-typedef set *SortSet;
-typedef block *SortRange;
-typedef rangemap *SortRangeMap;
+using mapiter = struct mapiter {
+  map::iterator curr{};
+  map *map_item{};
+};
+
+using setiter = struct setiter {
+  set::iterator curr{};
+  set *set_item{};
+};
+
+using SortFloat = floating *;
+using SortInt = mpz_ptr;
+using SortString = string *;
+using SortBytes = string *;
+using SortStringBuffer = stringbuffer *;
+using SortK = block *;
+using SortKItem = block *;
+using SortIOInt = block *;
+using SortIOFile = block *;
+using SortIOString = block *;
+using SortJSON = block *;
+using SortEndianness = block *;
+using SortSignedness = block *;
+using SortFFIType = block *;
+using SortList = list *;
+using SortMap = map *;
+using SortSet = set *;
+using SortRange = block *;
+using SortRangeMap = rangemap *;
 
 void *constructCompositePattern(uint32_t tag, std::vector<void *> &arguments);
 
@@ -359,7 +359,7 @@ char const *topSort(void);
 
 bool symbolIsInstantiation(uint32_t tag);
 
-typedef struct {
+using visitor = struct {
   void (*visitConfig)(writer *, block *, char const *, bool, void *);
   void (*visitMap)(
       writer *, map *, char const *, char const *, char const *, void *);
@@ -375,7 +375,7 @@ typedef struct {
   void (*visitSeparator)(writer *, void *);
   void (*visitRangeMap)(
       writer *, rangemap *, char const *, char const *, char const *, void *);
-} visitor;
+};
 
 void printMap(
     writer *, map *, char const *, char const *, char const *, void *);
diff --git a/lib/ast/AST.cpp b/lib/ast/AST.cpp
index e797ab8a6..83cb592f8 100644
--- a/lib/ast/AST.cpp
+++ b/lib/ast/AST.cpp
@@ -1467,11 +1467,11 @@ void KORECompositeSortDeclaration::print(
 void KORESymbolDeclaration::print(std::ostream &Out, unsigned indent) const {
   std::string Indent(indent, ' ');
   Out << Indent << (_isHooked ? "hooked-symbol " : "symbol ")
-      << symbol->getName();
+      << getSymbol()->getName();
   printSortVariables(Out);
   Out << "(";
   bool isFirst = true;
-  for (auto const &Argument : symbol->getArguments()) {
+  for (auto const &Argument : getSymbol()->getArguments()) {
     if (!isFirst) {
       Out << ",";
     }
@@ -1479,18 +1479,18 @@ void KORESymbolDeclaration::print(std::ostream &Out, unsigned indent) const {
     isFirst = false;
   }
   Out << ") : ";
-  symbol->getSort()->print(Out);
+  getSymbol()->getSort()->print(Out);
   Out << " ";
   printAttributeList(Out, attributes());
 }
 
 void KOREAliasDeclaration::print(std::ostream &Out, unsigned indent) const {
   std::string Indent(indent, ' ');
-  Out << Indent << "alias " << symbol->getName();
+  Out << Indent << "alias " << getSymbol()->getName();
   printSortVariables(Out);
   Out << "(";
   bool isFirst = true;
-  for (auto const &Argument : symbol->getArguments()) {
+  for (auto const &Argument : getSymbol()->getArguments()) {
     if (!isFirst) {
       Out << ",";
     }
@@ -1498,7 +1498,7 @@ void KOREAliasDeclaration::print(std::ostream &Out, unsigned indent) const {
     isFirst = false;
   }
   Out << ") : ";
-  symbol->getSort()->print(Out);
+  getSymbol()->getSort()->print(Out);
   Out << " where ";
   boundVariables->print(Out);
   Out << " := ";
diff --git a/lib/binary/ProofTraceParser.cpp b/lib/binary/ProofTraceParser.cpp
index 53f331ab5..5327c7fd3 100644
--- a/lib/binary/ProofTraceParser.cpp
+++ b/lib/binary/ProofTraceParser.cpp
@@ -22,8 +22,7 @@ void LLVMFunctionEvent::addArgument(LLVMEvent const &argument) {
 LLVMHookEvent::LLVMHookEvent(std::string _name, std::string _relativePosition)
     : name(std::move(_name))
     , relativePosition(std::move(_relativePosition))
-    , korePattern(nullptr)
-    , patternLength(0U) { }
+    , korePattern(nullptr) { }
 
 void LLVMHookEvent::addArgument(LLVMEvent const &argument) {
   arguments.push_back(argument);
@@ -40,15 +39,15 @@ void LLVMRewriteEvent::printSubstitution(
 void LLVMRuleEvent::print(std::ostream &Out, unsigned indent) const {
   std::string Indent(indent * indent_size, ' ');
   Out << fmt::format(
-      "{}rule: {} {}\n", Indent, ruleOrdinal, substitution.size());
+      "{}rule: {} {}\n", Indent, getRuleOrdinal(), getSubstitution().size());
   printSubstitution(Out, indent + 1U);
 }
 
 void LLVMSideConditionEvent::print(std::ostream &Out, unsigned indent) const {
   std::string Indent(indent * indent_size, ' ');
   Out << fmt::format(
-      "{}side condition entry: {} {}\n", Indent, ruleOrdinal,
-      substitution.size());
+      "{}side condition entry: {} {}\n", Indent, getRuleOrdinal(),
+      getSubstitution().size());
   printSubstitution(Out, indent + 1U);
 }
 
diff --git a/lib/codegen/CreateTerm.cpp b/lib/codegen/CreateTerm.cpp
index 34fc84bc8..62d1744e3 100644
--- a/lib/codegen/CreateTerm.cpp
+++ b/lib/codegen/CreateTerm.cpp
@@ -292,7 +292,7 @@ sptr<KORESort> termSort(KOREPattern *pattern) {
 }
 
 llvm::Value *CreateTerm::alloc_arg(
-    KORECompositePattern *pattern, int idx, std::string locationStack) {
+    KORECompositePattern *pattern, int idx, std::string const &locationStack) {
   KOREPattern *p = pattern->getArguments()[idx].get();
   std::string newLocation = fmt::format("{}:{}", locationStack, idx);
   if (isInjectionSymbol(p, Definition->getInjSymbol())) {
@@ -752,7 +752,7 @@ llvm::Value *CreateTerm::createFunctionCall(
  * triangle injection pair */
 llvm::Value *CreateTerm::notInjectionCase(
     KORECompositePattern *constructor, llvm::Value *val,
-    std::string locationStack) {
+    std::string const &locationStack) {
   KORESymbol const *symbol = constructor->getConstructor();
   KORESymbolDeclaration *symbolDecl
       = Definition->getSymbolDeclarations().at(symbol->getName());
diff --git a/lib/codegen/DecisionParser.cpp b/lib/codegen/DecisionParser.cpp
index e916344ad..72cae9ee1 100644
--- a/lib/codegen/DecisionParser.cpp
+++ b/lib/codegen/DecisionParser.cpp
@@ -24,7 +24,7 @@ namespace kllvm {
 
 class DTPreprocessor {
 private:
-  std::map<yaml_node_t *, DecisionNode *> uniqueNodes;
+  std::map<yaml_node_t *, DecisionNode *> uniqueNodes{};
   std::map<std::string, KORESymbol *> const &syms;
   std::map<ValueType, sptr<KORECompositeSort>> const &sorts;
   KORESymbol *dv;
@@ -111,10 +111,9 @@ class DTPreprocessor {
       llvm::Module *mod, yaml_document_t *doc)
       : syms(syms)
       , sorts(sorts)
+      , dv(KORESymbol::Create("\\dv").release())
       , doc(doc)
-      , mod(mod) {
-    dv = KORESymbol::Create("\\dv").release();
-  }
+      , mod(mod) { }
 
   static std::string to_string(std::vector<std::string> const &occurrence) {
     std::string result;
diff --git a/runtime/alloc/arena.cpp b/runtime/alloc/arena.cpp
index 2c4d7c6a4..e9839db03 100644
--- a/runtime/alloc/arena.cpp
+++ b/runtime/alloc/arena.cpp
@@ -188,10 +188,10 @@ char *movePtr(char *ptr, size_t size, char const *arena_end_ptr) {
   if (next_ptr == arena_end_ptr) {
     return nullptr;
   }
-  if (next_ptr != mem_block_start(ptr) + BLOCK_SIZE) {
+  if (next_ptr != MEM_BLOCK_START(ptr) + BLOCK_SIZE) {
     return next_ptr;
   }
-  char *next_block = *(char **)mem_block_start(ptr);
+  char *next_block = *(char **)MEM_BLOCK_START(ptr);
   if (!next_block) {
     return nullptr;
   }
@@ -199,7 +199,7 @@ char *movePtr(char *ptr, size_t size, char const *arena_end_ptr) {
 }
 
 ssize_t ptrDiff(char *ptr1, char *ptr2) {
-  if (mem_block_start(ptr1) == mem_block_start(ptr2)) {
+  if (MEM_BLOCK_START(ptr1) == MEM_BLOCK_START(ptr2)) {
     return ptr1 - ptr2;
   }
   memory_block_header *hdr = mem_block_header(ptr2);
diff --git a/runtime/collect/collect.cpp b/runtime/collect/collect.cpp
index d7b9eb36a..54c300745 100644
--- a/runtime/collect/collect.cpp
+++ b/runtime/collect/collect.cpp
@@ -47,7 +47,7 @@ void migrate(block **blockPtr) {
     return;
   }
   uint64_t const hdr = currBlock->h.hdr;
-  initialize_migrate();
+  INITIALIZE_MIGRATE();
   uint16_t layout = layout_hdr(hdr);
   size_t lenInBytes = get_size(hdr, layout);
   auto **forwardingAddress = (block **)(currBlock + 1);
@@ -62,7 +62,7 @@ void migrate(block **blockPtr) {
     numBytesLiveAtCollection[oldAge] += lenInBytes;
 #endif
     memcpy(newBlock, currBlock, lenInBytes);
-    migrate_header(newBlock);
+    MIGRATE_HEADER(newBlock);
     *forwardingAddress = newBlock;
     currBlock->h.hdr |= FWD_PTR_BIT;
     *blockPtr = newBlock;
@@ -90,7 +90,7 @@ static void migrate_string_buffer(stringbuffer **bufferPtr) {
   stringbuffer *buffer = *bufferPtr;
   uint64_t const hdr = buffer->h.hdr;
   uint64_t const cap = len(buffer->contents);
-  initialize_migrate();
+  INITIALIZE_MIGRATE();
   if (!hasForwardingAddress) {
     stringbuffer *newBuffer = nullptr;
     string *newContents = nullptr;
@@ -107,7 +107,7 @@ static void migrate_string_buffer(stringbuffer **bufferPtr) {
 #endif
     memcpy(newContents, buffer->contents, sizeof(string) + buffer->strlen);
     memcpy(newBuffer, buffer, sizeof(stringbuffer));
-    migrate_header(newBuffer);
+    MIGRATE_HEADER(newBuffer);
     newBuffer->contents = newContents;
     *(stringbuffer **)(buffer->contents) = newBuffer;
     buffer->h.hdr |= FWD_PTR_BIT;
@@ -116,9 +116,9 @@ static void migrate_string_buffer(stringbuffer **bufferPtr) {
 }
 
 static void migrate_mpz(mpz_ptr *mpzPtr) {
-  mpz_hdr *intgr = struct_base(mpz_hdr, i, *mpzPtr);
+  mpz_hdr *intgr = STRUCT_BASE(mpz_hdr, i, *mpzPtr);
   uint64_t const hdr = intgr->h.hdr;
-  initialize_migrate();
+  INITIALIZE_MIGRATE();
   if (!hasForwardingAddress) {
     mpz_hdr *newIntgr = nullptr;
     string *newLimbs = nullptr;
@@ -127,7 +127,7 @@ static void migrate_mpz(mpz_ptr *mpzPtr) {
     numBytesLiveAtCollection[oldAge] += sizeof(mpz_hdr);
 #endif
     if (hasLimbs) {
-      string *limbs = struct_base(string, data, intgr->i->_mp_d);
+      string *limbs = STRUCT_BASE(string, data, intgr->i->_mp_d);
       size_t lenLimbs = len(limbs);
 
 #ifdef GC_DBG
@@ -137,22 +137,22 @@ static void migrate_mpz(mpz_ptr *mpzPtr) {
       assert(intgr->i->_mp_alloc * sizeof(mp_limb_t) == lenLimbs);
 
       if (shouldPromote || (isInOldGen && collect_old)) {
-        newIntgr = struct_base(mpz_hdr, i, koreAllocIntegerOld(0));
+        newIntgr = STRUCT_BASE(mpz_hdr, i, koreAllocIntegerOld(0));
         newLimbs = (string *)koreAllocTokenOld(sizeof(string) + lenLimbs);
       } else {
-        newIntgr = struct_base(mpz_hdr, i, koreAllocInteger(0));
+        newIntgr = STRUCT_BASE(mpz_hdr, i, koreAllocInteger(0));
         newLimbs = (string *)koreAllocToken(sizeof(string) + lenLimbs);
       }
       memcpy(newLimbs, limbs, sizeof(string) + lenLimbs);
     } else {
       if (shouldPromote || (isInOldGen && collect_old)) {
-        newIntgr = struct_base(mpz_hdr, i, koreAllocIntegerOld(0));
+        newIntgr = STRUCT_BASE(mpz_hdr, i, koreAllocIntegerOld(0));
       } else {
-        newIntgr = struct_base(mpz_hdr, i, koreAllocInteger(0));
+        newIntgr = STRUCT_BASE(mpz_hdr, i, koreAllocInteger(0));
       }
     }
     memcpy(newIntgr, intgr, sizeof(mpz_hdr));
-    migrate_header(newIntgr);
+    MIGRATE_HEADER(newIntgr);
     if (hasLimbs) {
       newIntgr->i->_mp_d = (mp_limb_t *)newLimbs->data;
     }
@@ -163,13 +163,13 @@ static void migrate_mpz(mpz_ptr *mpzPtr) {
 }
 
 static void migrate_floating(floating **floatingPtr) {
-  floating_hdr *flt = struct_base(floating_hdr, f, *floatingPtr);
+  floating_hdr *flt = STRUCT_BASE(floating_hdr, f, *floatingPtr);
   uint64_t const hdr = flt->h.hdr;
-  initialize_migrate();
+  INITIALIZE_MIGRATE();
   if (!hasForwardingAddress) {
     floating_hdr *newFlt = nullptr;
     string *newLimbs = nullptr;
-    string *limbs = struct_base(string, data, flt->f.f->_mpfr_d - 1);
+    string *limbs = STRUCT_BASE(string, data, flt->f.f->_mpfr_d - 1);
     size_t lenLimbs = len(limbs);
 
 #ifdef GC_DBG
@@ -183,15 +183,15 @@ static void migrate_floating(floating **floatingPtr) {
         <= lenLimbs);
 
     if (shouldPromote || (isInOldGen && collect_old)) {
-      newFlt = struct_base(floating_hdr, f, koreAllocFloatingOld(0));
+      newFlt = STRUCT_BASE(floating_hdr, f, koreAllocFloatingOld(0));
       newLimbs = (string *)koreAllocTokenOld(sizeof(string) + lenLimbs);
     } else {
-      newFlt = struct_base(floating_hdr, f, koreAllocFloating(0));
+      newFlt = STRUCT_BASE(floating_hdr, f, koreAllocFloating(0));
       newLimbs = (string *)koreAllocToken(sizeof(string) + lenLimbs);
     }
     memcpy(newLimbs, limbs, sizeof(string) + lenLimbs);
     memcpy(newFlt, flt, sizeof(floating_hdr));
-    migrate_header(newFlt);
+    MIGRATE_HEADER(newFlt);
     newFlt->f.f->_mpfr_d = (mp_limb_t *)newLimbs->data + 1;
     *(floating **)(flt->f.f->_mpfr_d) = &newFlt->f;
     flt->h.hdr |= FWD_PTR_BIT;
@@ -287,7 +287,7 @@ void koreCollect(void **roots, uint8_t nroots, layoutitem *typeInfo) {
   if (collect_old || !previous_oldspace_alloc_ptr) {
     scan_ptr = oldspace_ptr();
   } else {
-    if (mem_block_start(previous_oldspace_alloc_ptr + 1)
+    if (MEM_BLOCK_START(previous_oldspace_alloc_ptr + 1)
         == previous_oldspace_alloc_ptr) {
       // this means that the previous oldspace allocation pointer points to an
       // address that is megabyte-aligned. This can only happen if we have just
diff --git a/runtime/collect/migrate_collection.cpp b/runtime/collect/migrate_collection.cpp
index 534cbc939..b8652f1bb 100644
--- a/runtime/collect/migrate_collection.cpp
+++ b/runtime/collect/migrate_collection.cpp
@@ -5,7 +5,7 @@
 #include <cstring>
 
 void migrate_collection_node(void **nodePtr) {
-  string *currBlock = struct_base(string, data, *nodePtr);
+  string *currBlock = STRUCT_BASE(string, data, *nodePtr);
   if (youngspace_collection_id()
           != getArenaSemispaceIDOfObject((void *)currBlock)
       && oldspace_collection_id()
@@ -13,7 +13,7 @@ void migrate_collection_node(void **nodePtr) {
     return;
   }
   uint64_t const hdr = currBlock->h.hdr;
-  initialize_migrate();
+  INITIALIZE_MIGRATE();
   size_t lenInBytes = get_size(hdr, 0);
   if (!hasForwardingAddress) {
     string *newBlock = nullptr;
@@ -26,7 +26,7 @@ void migrate_collection_node(void **nodePtr) {
     numBytesLiveAtCollection[oldAge] += lenInBytes;
 #endif
     memcpy(newBlock, currBlock, lenInBytes);
-    migrate_header(newBlock);
+    MIGRATE_HEADER(newBlock);
     *(void **)(currBlock + 1) = newBlock + 1;
     currBlock->h.hdr |= FWD_PTR_BIT;
   }
diff --git a/runtime/collect/migrate_roots.cpp b/runtime/collect/migrate_roots.cpp
index fcd68cf8d..10a64ad05 100644
--- a/runtime/collect/migrate_roots.cpp
+++ b/runtime/collect/migrate_roots.cpp
@@ -22,7 +22,7 @@ void migrateRoots() {
   migrate_collection_node((void **)&m);
   if (kllvm_randStateInitialized) {
     auto &rand = kllvm_randState->_mp_seed->_mp_d;
-    string *limbs = struct_base(string, data, rand);
+    string *limbs = STRUCT_BASE(string, data, rand);
     migrate((block **)&limbs);
     rand = (mp_limb_t *)limbs->data;
   }
diff --git a/scripts/clang-tidy.sh b/scripts/clang-tidy.sh
index e13fe0b7a..367aed953 100755
--- a/scripts/clang-tidy.sh
+++ b/scripts/clang-tidy.sh
@@ -25,6 +25,7 @@ mapfile -t inputs < <(find "${source_dirs[@]}" -name '*.cpp' -or -name '*.h')
 
 "${driver}"                           \
   "${inputs[@]}"                      \
+  -header-filter 'include/(kllvm|runtime)/'              \
   -clang-tidy-binary "${clang_tidy}"  \
   -j "$(nproc)"                       \
   -p "${BUILD_DIR}" "$@"              \
diff --git a/unittests/runtime-collections/rangemaps.cpp b/unittests/runtime-collections/rangemaps.cpp
index 7ba1fa1ee..773942483 100644
--- a/unittests/runtime-collections/rangemaps.cpp
+++ b/unittests/runtime-collections/rangemaps.cpp
@@ -50,13 +50,13 @@ BOOST_AUTO_TEST_CASE(rangemap_test_concat_failure) {
   auto m1
       = (rng_map::RangeMap<int, int>()).inserted(rng_map::Range<int>(0, 3), 2);
   auto map2 = m1.inserted(rng_map::Range<int>(8, 9), 4);
-  BOOST_CHECK_THROW(map1.concat(map2), std::invalid_argument);
+  BOOST_CHECK_THROW((void)map1.concat(map2), std::invalid_argument);
   auto map3
       = (rng_map::RangeMap<int, int>()).inserted(rng_map::Range<int>(3, 6), 2);
-  BOOST_CHECK_THROW(map1.concat(map3), std::invalid_argument);
+  BOOST_CHECK_THROW((void)map1.concat(map3), std::invalid_argument);
   auto map4
       = (rng_map::RangeMap<int, int>()).inserted(rng_map::Range<int>(5, 8), 2);
-  BOOST_CHECK_THROW(map1.concat(map4), std::invalid_argument);
+  BOOST_CHECK_THROW((void)map1.concat(map4), std::invalid_argument);
 }
 
 BOOST_AUTO_TEST_CASE(rangemap_test_contains_key) {
diff --git a/unittests/runtime-collections/treemaps.cpp b/unittests/runtime-collections/treemaps.cpp
index 779439a69..1592afa5e 100644
--- a/unittests/runtime-collections/treemaps.cpp
+++ b/unittests/runtime-collections/treemaps.cpp
@@ -107,14 +107,14 @@ BOOST_AUTO_TEST_CASE(treemap_test_concat_success) {
 BOOST_AUTO_TEST_CASE(treemap_test_concat_failure) {
   auto m1 = (rb_tree::RBTree<int, int>()).inserted(0, 1);
   auto m2 = (rb_tree::RBTree<int, int>()).inserted(0, 2);
-  BOOST_CHECK_THROW(m1.concat(m2), std::invalid_argument);
+  BOOST_CHECK_THROW((void)m1.concat(m2), std::invalid_argument);
 }
 
 BOOST_AUTO_TEST_CASE(treemap_test_at) {
   auto map = (rb_tree::RBTree<int, int>()).inserted(0, 1);
   auto result = map.at(0);
   BOOST_CHECK_EQUAL(result, 1);
-  BOOST_CHECK_THROW(map.at(2), std::invalid_argument);
+  BOOST_CHECK_THROW((void)map.at(2), std::invalid_argument);
 }
 
 BOOST_AUTO_TEST_CASE(treemap_test_contains) {