diff --git a/CMakeLists.txt b/CMakeLists.txt
index ba5ed6996..7c812176b 100644
--- a/CMakeLists.txt
+++ b/CMakeLists.txt
@@ -104,6 +104,24 @@ macro(add_decompilation_pipeline_test CATEGORY INPUT_FILE CONFIGURATION OUTPUT T
       FIXTURES_SETUP PrepareDecompilation_fixture_${TARGET_NAME}
       )
 
+    # test VMA
+    add_test(NAME vma_${TARGET_NAME} COMMAND revng --prefix=.
+      opt -S
+      -vma
+      -vma-mincut-iter=50
+      ${TARGET_NAME}_prepared.ll
+      -o /dev/null
+      )
+    set_property(TEST vma_${TARGET_NAME} APPEND PROPERTY
+      DEPENDS prepare_${TARGET_NAME}
+      )
+    set_property(TEST vma_${TARGET_NAME} APPEND PROPERTY
+      FIXTURES_REQUIRED PrepareDecompilation_fixture_${TARGET_NAME}
+      )
+    set_property(TEST vma_${TARGET_NAME} APPEND PROPERTY
+      FIXTURES_SETUP VMA_fixture_${TARGET_NAME}
+      )
+
     # test combing and decompilation without DLA
     add_test(NAME decompilation_${TARGET_NAME} COMMAND revng --prefix=.
       opt -S
diff --git a/include/revng-c/ValueManipulationAnalysis/TypeColors.h b/include/revng-c/ValueManipulationAnalysis/TypeColors.h
new file mode 100644
index 000000000..a187a7612
--- /dev/null
+++ b/include/revng-c/ValueManipulationAnalysis/TypeColors.h
@@ -0,0 +1,112 @@
+#pragma once
+
+//
+// Copyright rev.ng Srls. See LICENSE.md for details.
+//
+
+#include <bitset>
+#include <cstddef>
+#include <cstdint>
+
+#include "llvm/ADT/StringRef.h"
+#include "llvm/Support/raw_ostream.h"
+
+#include "revng/Support/Debug.h"
+
+namespace vma {
+
+/// \brief Index of each color in the bitset
+enum ColorIndex : uint8_t {
+  POINTERNESS_INDEX,
+  UNSIGNEDNESS_INDEX,
+  BOOLNESS_INDEX,
+  SIGNEDNESS_INDEX,
+  FLOATNESS_INDEX,
+  NUMBERNESS_INDEX,
+  MAX_COLORS
+};
+
+/// \brief Useful constants representing one, none and all colors
+enum BaseColor : unsigned {
+  NO_COLOR = 0,
+  POINTERNESS = (1 << POINTERNESS_INDEX),
+  UNSIGNEDNESS = (1 << UNSIGNEDNESS_INDEX),
+  BOOLNESS = (1 << BOOLNESS_INDEX),
+  SIGNEDNESS = (1 << SIGNEDNESS_INDEX),
+  FLOATNESS = (1 << FLOATNESS_INDEX),
+  NUMBERNESS = (1 << NUMBERNESS_INDEX),
+  ALL_COLORS = (1 << MAX_COLORS) - 1
+};
+
+/// \brief Name of each color, used for printing
+const llvm::StringRef TypeColorName[] = { "P", "U", "B", "S", "F", "N" };
+
+/// \brief Set of colors, stored as a bitset
+struct ColorSet {
+  using BitsetT = std::bitset<MAX_COLORS>;
+  BitsetT Bits;
+
+  ColorSet() = default;
+  ~ColorSet() = default;
+  ColorSet(const ColorSet &) = default;
+  ColorSet(ColorSet &&) = default;
+  ColorSet &operator=(const ColorSet &) = default;
+  ColorSet &operator=(ColorSet &&) = default;
+
+  ColorSet(const unsigned U) : Bits(U) {}
+  ColorSet(const BitsetT B) : Bits(B) {}
+  ColorSet(const BitsetT &B) : Bits(B) {}
+  ColorSet(BitsetT &&B) : Bits(B) {}
+
+  /// \brief Check if this ColorSet contains all colors of the argument
+  bool contains(const ColorSet &Other) const {
+    return (Bits | Other.Bits) == Bits;
+  }
+
+  /// \brief Add all colors of the argument to this ColorSet
+  void addColor(const ColorSet &Other) { Bits |= Other.Bits; }
+
+  /// \brief Count how many valid type candidates are contained in this ColorSet
+  size_t countValid() const { return (Bits & BitsetT(~NUMBERNESS)).count(); }
+
+  /// \brief Print the name of the colors contained in this ColorSet
+  void print(llvm::raw_ostream &Out) const debug_function {
+    if (Bits == ALL_COLORS) {
+      Out << "all";
+      return;
+    }
+
+    for (size_t I = 0; I < MAX_COLORS; ++I)
+      if (Bits.test(I))
+        Out << TypeColorName[I];
+  }
+
+  /// \brief Index of the next set bit, starting from \a StartIndex (excluded)
+  /// \param Idx  Where to start from (if == -1 start from the first)
+  /// \return MAX_COLORS if there's no set bit after this index
+  ColorIndex nextSetBit(int StartIndex) const {
+    if (StartIndex < 0)
+      StartIndex = -1;
+
+    for (int I = StartIndex + 1; I < MAX_COLORS; I++) {
+      if (Bits.test(I))
+        return ColorIndex(I);
+    }
+
+    return MAX_COLORS;
+  }
+
+  /// \brief Index of the first set bit
+  /// \return MAX_COLORS if there's no set bit
+  ColorIndex firstSetBit() const { return nextSetBit(/*StartIndex*/ -1); }
+
+  friend bool operator==(const ColorSet &Lhs, const ColorSet &Rhs) {
+    return Lhs.Bits == Rhs.Bits;
+  }
+
+  friend bool operator!=(const ColorSet &Lhs, const ColorSet &Rhs) {
+    return !(Lhs == Rhs);
+  }
+};
+
+} // namespace vma
\ No newline at end of file
diff --git a/include/revng-c/ValueManipulationAnalysis/ValueManipulationAnalysis.h b/include/revng-c/ValueManipulationAnalysis/ValueManipulationAnalysis.h
new file mode 100644
index 000000000..19813c3ff
--- /dev/null
+++ b/include/revng-c/ValueManipulationAnalysis/ValueManipulationAnalysis.h
@@ -0,0 +1,32 @@
+#pragma once
+
+//
+// Copyright rev.ng Srls. See LICENSE.md for details.
+//
+#include <map>
+
+#include "llvm/IR/Value.h"
+#include "llvm/Pass.h"
+
+#include "revng-c/ValueManipulationAnalysis/TypeColors.h"
+
+/// \brief Assign a type color for each Use and Value of a function
+class ValueManipulationAnalysis : public llvm::FunctionPass {
+public:
+  using ColorMapT = std::map<const llvm::Value *, const vma::ColorSet>;
+  static char ID;
+
+  // Ctors
+  ValueManipulationAnalysis() : llvm::FunctionPass(ID) {}
+
+  // FunctionPass methods
+  bool runOnFunction(llvm::Function &F) override;
+  void getAnalysisUsage(llvm::AnalysisUsage &AU) const override;
+
+  ///\brief ColorMap getter
+  ///\return A map between `llvm::Value*`s and their type color
+  const ColorMapT &getColorMap() const { return ColorMap; }
+
+private:
+  ColorMapT ColorMap;
+};
\ No newline at end of file
diff --git a/lib/CMakeLists.txt b/lib/CMakeLists.txt
index f16b332f8..a386fe200 100644
--- a/lib/CMakeLists.txt
+++ b/lib/CMakeLists.txt
@@ -17,3 +17,4 @@ add_subdirectory(RemoveLLVMDbgIntrinsics)
 add_subdirectory(RemoveNewPCCalls)
 add_subdirectory(TargetFunctionOption)
 add_subdirectory(ThreadSafeClangTooling)
+add_subdirectory(ValueManipulationAnalysis)
diff --git a/lib/ValueManipulationAnalysis/CMakeLists.txt b/lib/ValueManipulationAnalysis/CMakeLists.txt
new file mode 100644
index 000000000..fe73954bd
--- /dev/null
+++ b/lib/ValueManipulationAnalysis/CMakeLists.txt
@@ -0,0 +1,14 @@
+#
+# Copyright rev.ng Srls. See LICENSE.md for details.
+#
+
+revng_add_analyses_library(ValueManipulationAnalysis revngc
+  ValueManipulationAnalysis.cpp
+  TypeFlowGraph.cpp
+  TypeFlowNode.cpp
+  Mincut.cpp
+  ContractedGraph.cpp)
+
+target_link_libraries(ValueManipulationAnalysis
+  revng::revngSupport
+  revng::revngModel)
diff --git a/lib/ValueManipulationAnalysis/ContractedGraph.cpp b/lib/ValueManipulationAnalysis/ContractedGraph.cpp
new file mode 100644
index 000000000..4f836b91b
--- /dev/null
+++ b/lib/ValueManipulationAnalysis/ContractedGraph.cpp
@@ -0,0 +1,267 @@
+//
+// Copyright rev.ng Srls. See LICENSE.md for details.
+//
+
+#include <memory>
+
+#include "llvm/ADT/DepthFirstIterator.h"
+#include "llvm/ADT/STLExtras.h"
+#include "llvm/ADT/SetVector.h"
+#include "llvm/Support/raw_ostream.h"
+
+#include "revng/Support/Assert.h"
+#include "revng/Support/Debug.h"
+#include "revng/Support/IRHelpers.h"
+
+#include "revng-c/ValueManipulationAnalysis/TypeColors.h"
+
+#include "ContractedGraph.h"
+
+#include "TypeFlowGraph.h"
+#include "TypeFlowNode.h"
+
+using namespace vma;
+
+ContractedNode *
+ContractedGraph::addNode(std::optional<TypeFlowNode *> InitialContent = {}) {
+  Nodes.push_back(std::make_unique<ContractedNode>());
+  const auto &NewNode = Nodes.back();
+
+  if (InitialContent) {
+    NewNode->InitialNodes.insert(*InitialContent);
+    ReverseMap[*InitialContent] = NewNode.get();
+  }
+
+  return NewNode.get();
+}
+
+void ContractedGraph::contract(size_t EdgeIndex) {
+  revng_assert(EdgeIndex < NActiveEdges);
+
+  EdgeT &E = EdgeList[EdgeIndex];
+  ContractedNode *CN1 = getMapEntry(E.first);
+  ContractedNode *CN2 = getMapEntry(E.second);
+
+  // Verify that the nodes belongs to the graph (expensive)
+  if (VerifyLog.isEnabled()) {
+    const auto IsCN1 = [CN1](std::unique_ptr<ContractedNode> &N) {
+      return N.get() == CN1;
+    };
+    revng_assert(llvm::find_if(Nodes, IsCN1));
+
+    const auto IsCN2 = [CN2](std::unique_ptr<ContractedNode> &N) {
+      return N.get() == CN2;
+    };
+    revng_assert(llvm::find_if(Nodes, IsCN2));
+  }
+
+  auto IsSpecialNode = [this](ContractedNode *CN) {
+    return (CN == this->NodesToColor or CN == this->NodesToUncolor);
+  };
+
+  bool IsCN1Special = IsSpecialNode(CN1);
+  bool IsCN2Special = IsSpecialNode(CN2);
+  bool BothAreSpecial = IsCN1Special and IsCN2Special;
+  bool NoneIsSpecial = not IsCN1Special and not IsCN2Special;
+
+  // Never merge the two special nodes together
+  if (BothAreSpecial or (CN1 == CN2)) {
+    // Move the contracted edge after the active part of the list
+    NActiveEdges--;
+    std::swap(E, EdgeList[NActiveEdges]);
+    return;
+  }
+
+  ContractedNode *NodeToKeep, *NodeToRemove;
+
+  // Never remove a special node. If both are not special, remove the one with
+  // less nodes.
+  if (IsCN1Special or (NoneIsSpecial and CN1->totalSize() > CN2->totalSize())) {
+    NodeToKeep = CN1;
+    NodeToRemove = CN2;
+  } else {
+    NodeToKeep = CN2;
+    NodeToRemove = CN1;
+  }
+
+  // Move content
+  NodeToKeep->AdditionalNodes.set_union(NodeToRemove->InitialNodes);
+  NodeToKeep->AdditionalNodes.set_union(NodeToRemove->AdditionalNodes);
+
+  // Update Map
+  for (TypeFlowNode *TFGNode : NodeToRemove->InitialNodes)
+    getMapEntry(TFGNode) = NodeToKeep;
+  for (TypeFlowNode *TFGNode : NodeToRemove->AdditionalNodes)
+    getMapEntry(TFGNode) = NodeToKeep;
+
+  // Move the contracted edge after the active part of the list
+  NActiveEdges--;
+  revng_assert(NActiveEdges < EdgeList.size());
+  std::swap(E, EdgeList[NActiveEdges]);
+}
+
+void ContractedGraph::reset() {
+  for (auto &CN : Nodes) {
+    CN->reset();
+    for (auto *TFGNode : CN->InitialNodes)
+      ReverseMap[TFGNode] = CN.get();
+  }
+
+  NActiveEdges = EdgeList.size();
+}
+
+void ContractedGraph::check() {
+  // Check edges
+  for (auto &E : EdgeList) {
+    revng_assert(E.first != nullptr);
+    revng_assert(E.second != nullptr);
+
+    // The edge must exist in the TypeFlowGraph
+    revng_assert(llvm::is_contained(E.first->successors(), E.second));
+    // Only one edge between these two nodes must exist
+    revng_assert(1 == llvm::count(EdgeList, E));
+    // Both nodes of the edge must be in the map
+    revng_assert(ReverseMap.count(E.first));
+    revng_assert(ReverseMap.count(E.second));
+  }
+
+  const auto IsCentralNode = [Col(this->Color)](const TypeFlowNode *TFGNode) {
+    return TFGNode->isUndecided() and TFGNode->Candidates.contains(Col);
+  };
+
+  // Check map
+  for (const auto &[CurNode, Contracted] : ReverseMap) {
+    {
+      revng_assert(CurNode != nullptr);
+      revng_assert(Contracted != nullptr);
+
+      // The map entries must be nodes of the graph
+      revng_assert(1 == llvm::count_if(Nodes, [C(Contracted)](const auto &N) {
+                     return N.get() == C;
+                   }));
+      // The map entries must be coherent
+      const auto &Initial = Contracted->InitialNodes;
+      const auto &Additional = Contracted->AdditionalNodes;
+      revng_assert(1 == (Initial.count(CurNode) + Additional.count(CurNode)));
+    }
+
+    // The neighbors of the node should also be in the map
+    for (TypeFlowNode *Succ : CurNode->successors()) {
+      unsigned CNEdges = llvm::count(EdgeList, EdgeT{ CurNode, Succ });
+      unsigned TFEdges = llvm::count(CurNode->successors(), Succ);
+
+      if (IsCentralNode(CurNode) or IsCentralNode(Succ)) {
+        revng_assert(ReverseMap.count(Succ));
+        revng_assert(CNEdges == TFEdges);
+      } else if (not IsCentralNode(CurNode) and not IsCentralNode(Succ)) {
+        revng_assert(CNEdges == 0);
+      }
+    }
+    // Check that the right nodes belong to the special nodes
+    if (not IsCentralNode(CurNode)) {
+      if (CurNode->Candidates.contains(Color))
+        revng_assert(Contracted == NodesToColor);
+      else
+        revng_assert(Contracted == NodesToUncolor);
+    }
+  }
+
+  // Check nodes
+  for (auto &CN : Nodes) {
+    revng_assert(CN != nullptr);
+    for (auto *TFGNode : CN->InitialNodes) {
+      revng_assert(TFGNode != nullptr);
+
+      // Initial nodes must be unique
+      revng_assert(1 == llvm::count_if(Nodes, [TFGNode](auto &CN2) {
+                     return CN2.get()->InitialNodes.count(TFGNode);
+                   }));
+
+      revng_assert(ReverseMap.count(TFGNode));
+
+      // Check that the right nodes belong to the special nodes
+      if (not IsCentralNode(TFGNode)) {
+        if (TFGNode->Candidates.contains(Color))
+          revng_assert(CN.get() == NodesToColor);
+        else
+          revng_assert(CN.get() == NodesToUncolor);
+      }
+    }
+
+    for (auto *TFGNode : CN->AdditionalNodes) {
+      revng_assert(TFGNode != nullptr);
+      revng_assert(ReverseMap.count(TFGNode));
+    }
+  }
+}
+
+///\brief Insert a TypeFlowNode in the right ContractedNode
+///
+/// If the TypeFlowNode is a "border" node (i.e. it's decided or it doesn't
+/// have the right color) it will be inserted in the corresponding "special"
+/// node (NodesToColor or NodesToUncolor).
+/// Otherwise, a new ContractedNode is created.
+static void addInitialNode(ContractedGraph &G, TypeFlowNode *TFGNode) {
+  ContractedNode *Node;
+  if (G.ReverseMap.find(TFGNode) != G.ReverseMap.end())
+    return;
+
+  bool HasWrongColor = not TFGNode->Candidates.contains(G.Color);
+
+  if (HasWrongColor) {
+    // Wrong color => uncolor
+    Node = G.NodesToUncolor;
+  } else if (TFGNode->isDecided()) {
+    // Right color and decided => color
+    Node = G.NodesToColor;
+  } else if (TFGNode->isUndecided()) {
+    // Right color and undecided => create a new node
+    G.Nodes.push_back(std::make_unique<ContractedNode>());
+    Node = G.Nodes.back().get();
+  } else {
+    // Unreachable
+    revng_abort();
+  }
+
+  Node->InitialNodes.insert(TFGNode);
+  G.ReverseMap[TFGNode] = Node;
+  ++G.NTypeFlowNodes;
+}
+
+void vma::makeContractedGraph(ContractedGraph &G,
+                              TypeFlowNode *Entry,
+                              const ColorSet CurColor) {
+  // Check entrypoint properties
+  revng_assert(Entry->isDecided() and Entry->Candidates.contains(CurColor));
+
+  // Create special nodes
+  G.NodesToColor = G.addNode(Entry);
+  G.NodesToUncolor = G.addNode();
+  G.NTypeFlowNodes = 1;
+
+  const auto IsBorderNode = [CurColor](const TypeFlowNode *TFNode) {
+    return TFNode->isDecided() or TFNode->isUncolored()
+           or (not TFNode->Candidates.contains(CurColor));
+  };
+
+  // Visit the TypeFlowGraph depth-first. Stop when you find a decided node of
+  // any color or an undecided node that doesn't have CurColor as a candidate.
+  llvm::df_iterator_default_set<TypeFlowNode *> DfsExtSet;
+  for (TypeFlowNode *Reachable : llvm::depth_first_ext(Entry, DfsExtSet)) {
+    // Add current node
+    addInitialNode(G, Reachable);
+
+    for (TypeFlowNode *Succ : Reachable->successors()) {
+      if (IsBorderNode(Reachable) and IsBorderNode(Succ)) {
+        // Mark the node as "not to visit" by putting it in the visited set
+        if (llvm::all_of(Succ->successors(), IsBorderNode))
+          DfsExtSet.insert(Succ);
+      } else {
+        // Add successor
+        addInitialNode(G, Succ);
+        // Add edge
+        G.EdgeList.push_back({ Reachable, Succ });
+      }
+    }
+  }
+}
diff --git a/lib/ValueManipulationAnalysis/ContractedGraph.h b/lib/ValueManipulationAnalysis/ContractedGraph.h
new file mode 100644
index 000000000..ab06155f9
--- /dev/null
+++ b/lib/ValueManipulationAnalysis/ContractedGraph.h
@@ -0,0 +1,111 @@
+#pragma once
+
+//
+// Copyright rev.ng Srls. See LICENSE.md for details.
+//
+
+#include "llvm/ADT/STLExtras.h"
+#include "llvm/ADT/SetVector.h"
+
+#include "TypeFlowGraph.h"
+#include "TypeFlowNode.h"
+
+namespace vma {
+
+///\brief Super-node that contains TypeFlowGraph nodes
+struct ContractedNode {
+  ///\brief The initial content of the node
+  llvm::SmallSetVector<TypeFlowNode *, 8> InitialNodes;
+  ///\brief Additional nodes that have been collapsed inside this super-node
+  llvm::SmallSetVector<TypeFlowNode *, 8> AdditionalNodes;
+
+  ///\brief Reset the content to the initialization value
+  void reset() { AdditionalNodes.clear(); }
+
+  ///\brief Count the number of TypeFlowNodes collapsed inside this super-node
+  unsigned totalSize() { return InitialNodes.size() + AdditionalNodes.size(); }
+
+  ///\brief Check if a TypeFlowNode is part of this super node
+  bool contains(TypeFlowNode *TFN) const {
+    return InitialNodes.count(TFN) or AdditionalNodes.count(TFN);
+  }
+};
+
+///\brief Graph of super-nodes built upon the TypeFlowGraph
+struct ContractedGraph {
+  using EdgeT = std::pair<TypeFlowNode *, TypeFlowNode *>;
+  using EdgeContainerT = llvm::SmallVector<EdgeT, 8>;
+  using NodeContainerT = llvm::SmallVector<std::unique_ptr<ContractedNode>, 8>;
+  using ReverseMapT = llvm::SmallDenseMap<TypeFlowNode *, ContractedNode *>;
+
+  ///\brief Color that is being decided by contracting this graph
+  const ColorSet Color;
+
+  ///\brief Container of the ContractedNodes, owned by the graph
+  NodeContainerT Nodes;
+  ///\brief Number of unique TypeFlowNodes inside all the ContractedNodes
+  size_t NTypeFlowNodes = 0;
+  ///\brief Set of TypeFlowNodes that will eventually be assigned to Color
+  ContractedNode *NodesToColor;
+  ///\brief Set of TypeFlowNodes from which Color will be eventually removed
+  ContractedNode *NodesToUncolor;
+
+  ///\brief Maps each TypeFlowNode to the ContractedNode it is currently in
+  ReverseMapT ReverseMap;
+
+  ///\brief List of edges of the TypeFlowGraph that we want to contract
+  EdgeContainerT EdgeList;
+  ///\brief Edges that have been already collapsed are moved after this index
+  unsigned NActiveEdges = 0;
+
+  ContractedGraph() = delete;
+  ContractedGraph(const ColorSet &CurColor) : Color(CurColor){};
+  ContractedGraph(const TypeFlowGraph &N) = delete;
+  ContractedGraph(ContractedGraph &&N) = delete;
+  ContractedGraph &operator=(const ContractedGraph &N) = delete;
+  ContractedGraph &operator=(ContractedGraph &&N) = delete;
+
+  ///\brief Add a new ContractedNode with an (optional) initial content
+  ContractedNode *addNode(std::optional<TypeFlowNode *> InitialContent);
+
+  ///\brief Returns a reference to the corresponding entry in the ReverseMap
+  ContractedNode *&getMapEntry(TypeFlowNode *TFGNode) {
+    const auto &MapIt = ReverseMap.find(TFGNode);
+
+    revng_assert(MapIt != ReverseMap.end());
+    return MapIt->second;
+  }
+
+  ///\brief Contract the edge at \a EdgeIndex
+  ///
+  /// One of the two nodes of the edge is collapsed into the other, transferring
+  /// all its content and incoming/outgoing edge to the node it is collapsed
+  /// with. The rules for choosing which node to collapse and which to keep are:
+  /// 1. If both nodes are special, don't collapse
+  /// 2. If one node is a special node, always collapse the other
+  /// 3. If none of the two is special, keep the one with more nodes inside
+  /// Note that \a EdgeIndex must be less that \a NActiveEdges, meaning that the
+  /// collapsed edge must be active.
+  void contract(size_t EdgeIndex);
+  ///\brief Reset each Node and the ReverseMap to the original state
+  void reset();
+
+  ///\brief Check the consistency of the Graph
+  ///\note Expensive Check
+  void check();
+};
+
+/// \brief Return a ContractedGraph built starting from an \a Entry Node
+///
+/// This function identifies a connected component of undecided nodes
+/// that all have Color as a candidate. The ContractedGraph shall contain a
+/// ContractedNode for each of these nodes. The neighbors of these nodes will
+/// also be added in the graph, inside one of the two special ContractedNodes
+/// (NodesToColo or NodesToUncolor).
+///\param Entry The ContractedGraph will we built starting from this node
+///\param CurColor The color which has to be assigned when contracting
+void makeContractedGraph(ContractedGraph &G,
+                         TypeFlowNode *Entry,
+                         const ColorSet CurColor);
+
+} // namespace vma
\ No newline at end of file
diff --git a/lib/ValueManipulationAnalysis/Mincut.cpp b/lib/ValueManipulationAnalysis/Mincut.cpp
new file mode 100644
index 000000000..7efa151f3
--- /dev/null
+++ b/lib/ValueManipulationAnalysis/Mincut.cpp
@@ -0,0 +1,307 @@
+//
+// Copyright rev.ng Srls. See LICENSE.md for details.
+//
+
+#include <algorithm>
+#include <functional>
+#include <limits>
+#include <random>
+
+#include "llvm/ADT/DepthFirstIterator.h"
+#include "llvm/ADT/GraphTraits.h"
+#include "llvm/ADT/STLExtras.h"
+#include "llvm/ADT/SmallSet.h"
+#include "llvm/Support/Debug.h"
+#include "llvm/Support/GraphWriter.h"
+
+#include "revng/ADT/GenericGraph.h"
+#include "revng/Support/Assert.h"
+#include "revng/Support/Debug.h"
+#include "revng/Support/IRHelpers.h"
+
+#include "revng-c/ValueManipulationAnalysis/TypeColors.h"
+
+#include "Mincut.h"
+
+#include "ContractedGraph.h"
+#include "TypeFlowNode.h"
+
+using namespace vma;
+
+static Logger<> MincutLog("vma-mincut");
+
+static llvm::cl::opt<unsigned> MincutIterOpt("vma-mincut-iter",
+                                             llvm ::cl::desc("Specify the "
+                                                             "number of karger "
+                                                             "iterations for "
+                                                             "the mincut "
+                                                             "algorithm"));
+
+static unsigned calcCost(ContractedGraph &G) {
+  auto ContractedSize = G.NodesToColor->totalSize()
+                        + G.NodesToUncolor->totalSize();
+  revng_assert(G.NTypeFlowNodes == ContractedSize);
+  unsigned Cost = 0;
+
+  llvm::SmallSet<TypeFlowNode *, 16> Visited;
+
+  // Cost of a node in the NodesToColor set
+  auto CostOfNodeToColor = [&Visited, &G](TypeFlowNode *TFGNode) {
+    // Pay the cost only for the nodes that are being decided by the mincut
+    if (not TFGNode->isUndecided())
+      return 0U;
+
+    unsigned AdditionalCost = 0;
+
+    // If the node is undecided and belongs to NodesToColor, it means that all
+    // of its successors that have the right color are also in NodesToColor.
+    // This means that successors that do not belong to NodesToColor have
+    // automatically the wrong color.
+    for (auto *Succ : TFGNode->successors())
+      if (not G.NodesToColor->contains(Succ))
+        AdditionalCost++;
+
+    Visited.insert(TFGNode);
+    return AdditionalCost;
+  };
+
+  for (auto *TFGNode : G.NodesToColor->InitialNodes)
+    Cost += CostOfNodeToColor(TFGNode);
+  for (auto *TFGNode : G.NodesToColor->AdditionalNodes)
+    Cost += CostOfNodeToColor(TFGNode);
+
+  // Cost of a node in the NodesToUncolor set
+  auto CostOfNodeToUncolor = [&Visited, &G](TypeFlowNode *TFGNode) {
+    // Pay the cost only for the nodes that are being decided by the mincut
+    if (not TFGNode->isUndecided())
+      return 0U;
+
+    unsigned AdditionalCost = 0;
+
+    // If the node belongs to NodesToUncolor, remove G.Color from the candidates
+    ColorSet NodeColor = TFGNode->Candidates;
+    NodeColor.Bits.reset(G.Color.firstSetBit());
+
+    for (auto *Succ : TFGNode->successors()) {
+      if (Visited.count(Succ))
+        continue;
+
+      ColorSet CommonColors;
+      CommonColors.Bits = Succ->Candidates.Bits & NodeColor.Bits;
+      // If the node and its successor have no common candidates, pay a cost
+      if (CommonColors.countValid() == 0)
+        AdditionalCost++;
+    }
+
+    Visited.insert(TFGNode);
+    return AdditionalCost;
+  };
+
+  for (auto *TFGNode : G.NodesToUncolor->InitialNodes)
+    Cost += CostOfNodeToUncolor(TFGNode);
+  for (auto *TFGNode : G.NodesToUncolor->AdditionalNodes)
+    Cost += CostOfNodeToUncolor(TFGNode);
+
+  return Cost;
+}
+
+void vma::karger(ContractedGraph &G,
+                 unsigned &BestCost,
+                 ContractedNode &BestNodesToColor,
+                 ContractedNode &BestNodesToUncolor) {
+
+  // Fixed seed generated with /dev/urandom
+  static const unsigned RandSeed = 320464148;
+  // Seed the random generator for repeatability
+  srand(RandSeed);
+
+  // TODO: find a sane default, e.g. 10 * log2 (G.size())
+  const unsigned int DefaultNIter = 50U;
+  const unsigned NIter = (MincutIterOpt ? MincutIterOpt : DefaultNIter);
+
+  // Execute many times (Monte-carlo)
+  for (size_t Iter = 0; Iter < NIter; Iter++) {
+    G.reset();
+
+    auto SpecialNodesDimension = [&G]() {
+      return G.NodesToColor->totalSize() + G.NodesToUncolor->totalSize();
+    };
+
+    // Execute Karger until all nodes have been collapsed in a special supernode
+    while (G.NTypeFlowNodes > SpecialNodesDimension()) {
+      unsigned RandIdx = rand() % G.NActiveEdges;
+      G.contract(RandIdx);
+    }
+
+    if (VerifyLog.isEnabled())
+      G.check();
+
+    unsigned Cost = calcCost(G);
+
+    // Update best solution
+    if (Cost < BestCost) {
+      BestCost = Cost;
+      std::swap(BestNodesToColor.AdditionalNodes,
+                G.NodesToColor->AdditionalNodes);
+      std::swap(BestNodesToUncolor.AdditionalNodes,
+                G.NodesToUncolor->AdditionalNodes);
+
+      revng_log(MincutLog,
+                "Karger new best cost: " << BestCost << " [iteration: " << Iter
+                                         << "]");
+
+      revng_log(MincutLog, "Best choice: divided");
+    }
+
+    if (BestCost == 0)
+      break;
+  }
+}
+
+///\brief Generate the solution in which all nodes of \a G are colored
+static void generateColorAllSolution(ContractedGraph &G) {
+  for (auto &CN : G.Nodes) {
+    if (CN.get() == G.NodesToColor or CN.get() == G.NodesToUncolor)
+      continue;
+
+    for (TypeFlowNode *TFGNode : CN->InitialNodes) {
+      revng_assert(not TFGNode->isDecided()
+                   or not TFGNode->Candidates.contains(G.Color));
+      G.NodesToColor->AdditionalNodes.insert(TFGNode);
+      G.getMapEntry(TFGNode) = G.NodesToColor;
+    }
+  }
+}
+
+///\brief Generate the solution in which all nodes of \a G are uncolored
+static void moveAllColoredToUncolored(ContractedGraph &G) {
+  std::swap(G.NodesToUncolor->AdditionalNodes, G.NodesToColor->AdditionalNodes);
+  for (TypeFlowNode *TFGNode : G.NodesToUncolor->AdditionalNodes) {
+    revng_assert(not TFGNode->isDecided()
+                 or not TFGNode->Candidates.contains(G.Color));
+    G.getMapEntry(TFGNode) = G.NodesToUncolor;
+  }
+}
+
+///\brief Generate the two simplest cuts (color all and uncolor all)
+static void generateNaiveSolutions(ContractedGraph &G,
+                                   unsigned &BestCost,
+                                   ContractedNode &BestNodesToColor,
+                                   ContractedNode &BestNodesToUncolor) {
+  generateColorAllSolution(G);
+  unsigned ColorAllCost = calcCost(G);
+
+  moveAllColoredToUncolored(G);
+  unsigned RemoveAllCost = calcCost(G);
+
+  revng_log(MincutLog,
+            "cost of coloring all: "
+              << ColorAllCost << "  cost of removing all: " << RemoveAllCost);
+
+  if (RemoveAllCost < ColorAllCost) {
+    BestCost = RemoveAllCost;
+    BestNodesToColor.AdditionalNodes.clear();
+    std::swap(BestNodesToUncolor.AdditionalNodes,
+              G.NodesToUncolor->AdditionalNodes);
+
+    revng_log(MincutLog, "Best choice: remove all");
+  } else {
+    BestCost = ColorAllCost;
+    std::swap(BestNodesToColor.AdditionalNodes,
+              G.NodesToUncolor->AdditionalNodes);
+    BestNodesToUncolor.AdditionalNodes.clear();
+
+    revng_log(MincutLog, "Best choice: color all");
+  }
+}
+
+void vma::minCut(TypeFlowGraph &TG) {
+  // Apply karger one color at a time, using the color index in the bitset as
+  // ordering criterion.
+  for (unsigned I = 0; I < MAX_COLORS; I++) {
+    ColorSet CurColor(1 << I);
+
+    revng_log(MincutLog, "------ Color: " << dumpToString(CurColor));
+
+    for (TypeFlowNode *N : TG.nodes()) {
+      // Check if we can start building a ContractedGraph from the current node
+      auto HasUndecidedNeighbors = [CurColor](TypeFlowNode *TFGNodeode) {
+        return llvm::any_of(TFGNodeode->successors(),
+                            [CurColor](TypeFlowNode *Succ) {
+                              return Succ->isUndecided()
+                                     and Succ->Candidates.contains(CurColor);
+                            });
+      };
+      if (not(N->isDecided() and N->Candidates.contains(CurColor)
+              and HasUndecidedNeighbors(N)))
+        continue;
+
+      // Build Contracted graph
+      ContractedGraph G{ CurColor };
+      makeContractedGraph(G, N, CurColor);
+
+      if (VerifyLog.isEnabled())
+        G.check();
+
+      revng_log(MincutLog, "------ New karger: " << G.NTypeFlowNodes);
+      revng_log(MincutLog,
+                "Karger with "
+                  << G.NTypeFlowNodes
+                  << " nodes, NodesToColor: " << G.NodesToColor->totalSize()
+                  << "  NodesToUncolor: " << G.NodesToUncolor->totalSize());
+
+      // Keep track of the best solution
+      unsigned BestCost = std::numeric_limits<unsigned>::max();
+      ContractedNode BestNodesToColor = *G.NodesToColor;
+      ContractedNode BestNodesToUncolor = *G.NodesToUncolor;
+
+      // Try to color all and uncolor all
+      generateNaiveSolutions(G, BestCost, BestNodesToColor, BestNodesToUncolor);
+
+      // If NodesToUncolor is empty there's no point in trying karger
+      if (G.NodesToUncolor->InitialNodes.size() > 0)
+        karger(G, BestCost, BestNodesToColor, BestNodesToUncolor);
+
+      revng_log(MincutLog,
+                "Final solution "
+                  << G.NTypeFlowNodes
+                  << " nodes, NodesToColor: " << BestNodesToColor.totalSize()
+                  << "  NodesToUncolor: " << BestNodesToUncolor.totalSize());
+
+      // Color all nodes that belong to NodesToColor
+      for (TypeFlowNode *TFGNode : BestNodesToColor.InitialNodes) {
+        revng_assert(TFGNode->Candidates.contains(G.Color));
+        TFGNode->Candidates = G.Color;
+      }
+      for (TypeFlowNode *TFGNode : BestNodesToColor.AdditionalNodes) {
+        revng_assert(TFGNode->Candidates.contains(G.Color));
+        TFGNode->Candidates = G.Color;
+      }
+      // Uncolor all nodes that belong to NodesToColor
+      for (TypeFlowNode *TFGNode : BestNodesToUncolor.InitialNodes) {
+        revng_assert(not TFGNode->isDecided()
+                     or not TFGNode->Candidates.contains(G.Color));
+        TFGNode->Candidates.Bits.reset(I);
+      }
+      for (TypeFlowNode *TFGNode : BestNodesToUncolor.AdditionalNodes) {
+        revng_assert(not TFGNode->isDecided()
+                     or not TFGNode->Candidates.contains(G.Color));
+        TFGNode->Candidates.Bits.reset(I);
+      }
+
+      revng_log(MincutLog, "CurCost after applying mincut  " << countCasts(TG));
+    }
+
+    // Remove CurColor from the candidates of any remaining grey node before
+    // going to another color
+    for (TypeFlowNode *N : TG.nodes())
+      if (N->isUndecided() and N->Candidates.contains(CurColor))
+        N->Candidates.Bits.reset(I);
+
+    revng_log(MincutLog, "CurCost after resetting color  " << countCasts(TG));
+
+    applyMajorityVoting(TG);
+    revng_log(MincutLog,
+              "CurCost after applying majority voting  " << countCasts(TG));
+  }
+}
diff --git a/lib/ValueManipulationAnalysis/Mincut.h b/lib/ValueManipulationAnalysis/Mincut.h
new file mode 100644
index 000000000..9dba2ef40
--- /dev/null
+++ b/lib/ValueManipulationAnalysis/Mincut.h
@@ -0,0 +1,34 @@
+#pragma once
+
+//
+// Copyright rev.ng Srls. See LICENSE.md for details.
+//
+
+#include "ContractedGraph.h"
+#include "TypeFlowGraph.h"
+
+namespace vma {
+
+/// \brief Contract the graph until you end with only two nodes
+///
+/// This implementation guarantees that NodesToColor and NodesToUncolor are
+/// never merged, therefore they will be the only two nodes remaining at the
+/// end. The algorithm is applied many times in a monte-carlo fashion.
+/// \param G The graph to contract
+/// \param BestCost The current cost, will be updated if a better one is found
+/// \param BestNodesToColor Where to store the NodesToColor of the best solution
+/// \param BestNodesToUncolor Where to store the NodesToUncolor of the best sol.
+void karger(ContractedGraph &G,
+            unsigned &BestCost,
+            ContractedNode &BestNodesToColor,
+            ContractedNode &BestNodesToUncolor);
+
+/// \brief Assign undecided nodes applying Karger one color at a time
+///
+/// This function reasons one color at a time. It creates a ContractedGraph for
+/// each connected component of undecided nodes that have a given color among
+/// their candidates. A probabilistic algorithm is then applied to find, in each
+/// ContractedGraph, the minimal cut that divides the nodes of the current color
+/// from nodes of other colors.
+void minCut(TypeFlowGraph &TG);
+} // namespace vma
\ No newline at end of file
diff --git a/lib/ValueManipulationAnalysis/TypeFlowGraph.cpp b/lib/ValueManipulationAnalysis/TypeFlowGraph.cpp
new file mode 100644
index 000000000..0516cface
--- /dev/null
+++ b/lib/ValueManipulationAnalysis/TypeFlowGraph.cpp
@@ -0,0 +1,485 @@
+//
+// Copyright rev.ng Srls. See LICENSE.md for details.
+//
+
+#include "llvm/ADT/DepthFirstIterator.h"
+#include "llvm/ADT/PostOrderIterator.h"
+#include "llvm/ADT/STLExtras.h"
+#include "llvm/ADT/SmallSet.h"
+#include "llvm/ADT/SmallVector.h"
+#include "llvm/IR/Argument.h"
+#include "llvm/IR/CFG.h"
+#include "llvm/IR/GlobalValue.h"
+#include "llvm/IR/Instruction.h"
+#include "llvm/IR/Value.h"
+#include "llvm/Support/Casting.h"
+#include "llvm/Support/Debug.h"
+#include "llvm/Support/raw_ostream.h"
+
+#include "revng/ADT/ReversePostOrderTraversal.h"
+#include "revng/Support/Assert.h"
+#include "revng/Support/Debug.h"
+
+#include "revng-c/ValueManipulationAnalysis/TypeColors.h"
+
+#include "TypeFlowGraph.h"
+
+#include "TypeFlowGraphWriter.h"
+#include "TypeFlowNode.h"
+
+using namespace vma;
+using namespace llvm;
+
+static Logger<> TGLog("vma-tg");
+
+// --------------- TypeFlowGraph
+
+TypeFlowNode *TypeFlowGraph::addNodeContaining(const UseOrValue &NC) {
+  revng_assert(not ContentToNodeMap.count(NC));
+
+  NodeColorProperty InitialColors = nodeColors(NC);
+  auto *N = this->addNode(NC, InitialColors);
+  ContentToNodeMap[NC] = N;
+
+  return N;
+}
+
+TypeFlowNode *
+TypeFlowGraph::getNodeContaining(const UseOrValue &Content) const {
+  const auto &It = ContentToNodeMap.find(Content);
+  revng_assert(It != ContentToNodeMap.end());
+
+  return It->second;
+}
+
+void TypeFlowGraph::dump(const llvm::Twine &Title, std::string FileName) {
+  llvm::WriteGraph(this,
+                   this->Func->getName() + Title,
+                   false,
+                   this->Func->getName() + Title,
+                   FileName);
+}
+
+void TypeFlowGraph::print(llvm::raw_ostream &OS) {
+  llvm::WriteGraph(OS, this);
+}
+
+void TypeFlowGraph::view() {
+  llvm::ViewGraph(this, this->Func->getName(), false, this->Func->getName());
+}
+
+// --------------- TypeFlowGraph manipulation
+
+///\brief Check if two nodes are already connected before adding the successor
+static bool
+addSuccessorIfAbsent(TypeFlowNode *N1, TypeFlowNode *N2, const EdgeLabel &E) {
+  if (llvm::is_contained(N1->successors(), N2))
+    return false;
+
+  N1->addSuccessor(N2, E);
+  return true;
+}
+
+/// \brief Add edge (possibly both ways) between two nodes, based on the content
+static bool connect(TypeFlowNode *N1, TypeFlowNode *N2) {
+
+  // Value -> Value: no connection
+  if (N1->isValue() and N2->isValue())
+    return false;
+
+  // Use -> Use: check that they have the same user before connecting
+  if (N1->isUse() and N2->isUse()) {
+    auto *N1User = N1->getUse()->getUser();
+    auto *N2User = N2->getUse()->getUser();
+
+    if (N1User != N2User)
+      return false;
+
+    const Instruction *I = cast<Instruction>(N1User);
+
+    switch (I->getOpcode()) {
+      // Currently the only instructions for which there is a typeflow between
+      // the operands are comparisons
+    case Instruction::ICmp: {
+      bool Connected = false;
+
+      Connected |= addSuccessorIfAbsent(N1, N2, ALL_COLORS);
+      Connected |= addSuccessorIfAbsent(N2, N1, ALL_COLORS);
+
+      return Connected;
+    }
+
+    default:
+      return false;
+    }
+  }
+
+  // If it's not Use->Use or Value->Value, one of the two is a Value and the
+  // other one is a Use
+  revng_assert((N1->isValue() and N2->isUse())
+               or (N1->isUse() and N2->isValue()));
+
+  TypeFlowNode *ValNode = N1->isValue() ? N1 : N2;
+  TypeFlowNode *UseNode = N1->isUse() ? N1 : N2;
+
+  revng_assert(ValNode->isValue() and UseNode->isUse());
+
+  // Use -> Value: connect according to the accepted colors
+  if (UseNode->getUse()->get() == ValNode->getValue()) {
+    bool Connected = false;
+
+    Connected |= addSuccessorIfAbsent(ValNode, UseNode, UseNode->Accepted);
+    Connected |= addSuccessorIfAbsent(UseNode, ValNode, ValNode->Accepted);
+
+    return Connected;
+  }
+
+  // Use -> User: connect according to user opcode
+  if (UseNode->getUse()->getUser() == ValNode->getValue()) {
+    const Instruction *I = cast<Instruction>(UseNode->getUse()->getUser());
+    const size_t OpNo = UseNode->getUse()->getOperandNo();
+
+    const auto AddBidirectionalEdge =
+      [](TypeFlowNode *N1, TypeFlowNode *N2, const ColorSet C) {
+        bool Connected = false;
+        Connected |= addSuccessorIfAbsent(N1, N2, C);
+        Connected |= addSuccessorIfAbsent(N2, N1, C);
+        return Connected;
+      };
+
+    switch (I->getOpcode()) {
+    case Instruction::LShr:
+      // TODO: What to do when shifting booleans and pointers is still a
+      // matter of discussion. For now the decision is that if a pointer or a
+      // boolean gets shifted, it is not a pointer/boolean anymore, so we
+      // don't add propagation edges forward for these colors. Also, if the
+      // result of a shift is used in a boolean/pointer sense, this doesn't
+      // give us enough information to color the operands, so don't propagate
+      // backwards either.
+      if (OpNo == 0)
+        return AddBidirectionalEdge(UseNode, ValNode, UNSIGNEDNESS);
+      break;
+
+    case Instruction::AShr:
+      if (OpNo == 0)
+        return AddBidirectionalEdge(UseNode, ValNode, SIGNEDNESS);
+      break;
+
+    case Instruction::Shl:
+      if (OpNo == 0)
+        return AddBidirectionalEdge(UseNode,
+                                    ValNode,
+                                    (SIGNEDNESS | UNSIGNEDNESS));
+      break;
+
+    case Instruction::Add: {
+      bool Connected = false;
+      Connected |= addSuccessorIfAbsent(UseNode, ValNode, ~FLOATNESS);
+      Connected |= addSuccessorIfAbsent(ValNode,
+                                        UseNode,
+                                        ~(FLOATNESS | POINTERNESS
+                                          | NUMBERNESS));
+      return Connected;
+      break;
+    }
+
+    case Instruction::Mul:
+    case Instruction::Sub:
+      return AddBidirectionalEdge(UseNode,
+                                  ValNode,
+                                  ~(FLOATNESS | POINTERNESS | NUMBERNESS));
+      break;
+
+    case Instruction::PHI:
+    case Instruction::FPToUI:
+    case Instruction::IntToPtr:
+    case Instruction::PtrToInt:
+    case Instruction::FPToSI:
+    case Instruction::UIToFP:
+    case Instruction::SIToFP:
+    case Instruction::BitCast:
+    case Instruction::SExt:
+    case Instruction::ZExt:
+    case Instruction::Trunc:
+      return AddBidirectionalEdge(UseNode, ValNode, ~NUMBERNESS);
+      break;
+
+    case Instruction::And:
+    case Instruction::Or:
+    case Instruction::Xor:
+      return AddBidirectionalEdge(UseNode,
+                                  ValNode,
+                                  ~(FLOATNESS | POINTERNESS | NUMBERNESS));
+      break;
+    }
+  }
+
+  return false;
+}
+
+TypeFlowGraph vma::makeTypeFlowGraphFromFunction(const llvm::Function *F) {
+  TypeFlowGraph TG;
+  TG.Func = F;
+
+  // Visit values before users (a part from phis)
+  for (const BasicBlock *BB : ReversePostOrderTraversal(F)) {
+    for (const Instruction &I : *BB) {
+
+      auto IsPhiInstr = [](const llvm::User *Inst) {
+        return cast<Instruction>(Inst)->getOpcode() == Instruction::PHI;
+      };
+
+      const auto ShouldValueBeAdded = [](const llvm::Value *V) {
+        return isa<Instruction>(V) or isa<Argument>(V);
+      };
+
+      const auto ShouldUseBeAdded = [&ShouldValueBeAdded](const llvm::Use *U) {
+        return ShouldValueBeAdded(U->get());
+      };
+
+      if (TGLog.isEnabled()) {
+        std::string S;
+        llvm::raw_string_ostream OS(S);
+        I.printAsOperand(OS);
+        revng_log(TGLog, "VISITING: [" << &I << "]  " << S);
+      }
+
+      // Add the Value node
+      TypeFlowNode *InstNode;
+      if (TG.ContentToNodeMap.count(&I)) {
+        // If the instruction has already been added, it must be because of a
+        // phi
+        revng_assert(any_of(I.users(), IsPhiInstr));
+        InstNode = TG.ContentToNodeMap[&I];
+      } else if (ShouldValueBeAdded(&I)) {
+        InstNode = TG.addNodeContaining(&I);
+      } else {
+        // Skip values that should not be added to the TypeFlowGraph
+        continue;
+      }
+
+      revng_log(TGLog, "INST: " << InstNode);
+
+      // Add a Use node for each operand
+      SmallVector<TypeFlowNode *, 2> PrevOperands;
+      for (const Use &Op : I.operands()) {
+        if (not ShouldUseBeAdded(&Op))
+          continue;
+
+        TypeFlowNode *UseNode = TG.addNodeContaining(&Op);
+        connect(UseNode, InstNode);
+        revng_log(TGLog, "USE: " << UseNode);
+
+        // Connect Uses to Uses
+        for (auto *Prev : PrevOperands)
+          connect(UseNode, Prev);
+
+        PrevOperands.push_back(UseNode);
+
+        // The operand value should have already been visited, unless the
+        // instruction is a phi or the operand is a non-instruction
+        // (constant, global, arg).
+        if (not TG.ContentToNodeMap.count(Op.get())) {
+          revng_assert(I.getOpcode() == Instruction::PHI
+                       or not isa<Instruction>(Op.get()));
+          TG.addNodeContaining(Op.get());
+        }
+
+        auto *OpValNode = TG.ContentToNodeMap[Op.get()];
+        revng_log(TGLog, "OP_VAL: " << OpValNode);
+
+        // Connect Operand Use to the Instruction's Value
+        connect(UseNode, OpValNode);
+      }
+    }
+  }
+
+  return TG;
+}
+
+void vma::propagateColors(TypeFlowGraph &TG) {
+  propagateColor<POINTERNESS>(TG);
+  propagateColor<SIGNEDNESS>(TG);
+  propagateColor<UNSIGNEDNESS>(TG);
+  propagateColor<BOOLNESS>(TG);
+  propagateColor<FLOATNESS>(TG);
+  // Numberness is propagated separately by propagateNumberness(), since it
+  // has to be propagated through pattern matching
+}
+
+template<unsigned Filter>
+void vma::propagateColor(TypeFlowGraph &TG) {
+  // Check that only one color at a time is being propagated
+  revng_assert(ColorSet(Filter).countValid() == 1);
+
+  llvm::df_iterator_default_set<TypeFlowNode *> Visited;
+
+  for (auto *Node : TG.nodes()) {
+    bool AlreadyVisited = (Visited.find(Node) != Visited.end());
+    // Start from nodes that have only the desired color
+    if (AlreadyVisited or not Node->Candidates.contains(ColorSet(Filter)))
+      continue;
+
+    // Explore only the edges that have the desired color
+    for (TypeFlowNode *Reachable :
+         llvm::depth_first_ext(EdgeFilteredTG<Filter>(Node), Visited)) {
+      // If a node is reachable from a source with a certain color through edges
+      // that all have that color, by construction it should also accept that
+      // color
+      revng_assert(Reachable->Accepted.contains(Filter));
+      Reachable->Candidates.addColor(Filter);
+    }
+  }
+}
+
+bool vma::propagateNumberness(TypeFlowGraph &TG) {
+  // TODO: backward propagate pointerness for known patterns (e.g. value + const
+  // = ptr)
+  // TODO: forward propagate numberness for known patterns (e.g. n+n = n )
+
+  // For now, just reset all numberness flags
+  for (auto *N : TG.nodes())
+    N->Candidates.Bits.reset(NUMBERNESS_INDEX);
+
+  return false;
+}
+
+void vma::makeBidirectional(TypeFlowGraph &TG) {
+  // Add each node as a successor of its successors
+  for (TypeFlowNode *N : TG.nodes()) {
+    llvm::SmallVector<TypeFlowNode *, 2> ToModify;
+
+    for (auto *Succ : N->successors())
+      if (not llvm::is_contained(Succ->successors(), N))
+        ToModify.push_back(Succ);
+
+    for (auto *M : ToModify)
+      M->addSuccessor(N);
+  }
+
+  // Verify that predecessors and successors are the same in all nodes
+  if (VerifyLog.isEnabled()) {
+    auto AllSuccessorsArePredecessors = [](TypeFlowNode *N) {
+      const auto IsPredecessorOfN = [N](TypeFlowNode *N2) {
+        return llvm::is_contained(N->predecessors(), N2);
+      };
+
+      return llvm::all_of(N->successors(), IsPredecessorOfN);
+    };
+
+    revng_assert(llvm::all_of(TG.nodes(), AllSuccessorsArePredecessors));
+  }
+}
+
+unsigned vma::countCasts(const TypeFlowGraph &TG) {
+  llvm::SmallSet<const TypeFlowNode *, 16> Visited;
+  unsigned Cost = 0;
+
+  for (const TypeFlowNode *TGNode : TG.nodes()) {
+    const auto &NodeBits = TGNode->Candidates.Bits;
+    // Ignore nodes with no candidates
+    if (NodeBits.count() == 0 or NodeBits == NUMBERNESS)
+      continue;
+
+    for (const TypeFlowNode *Succ : TGNode->successors()) {
+      // Ignore already visited nodes
+      if (Visited.count(Succ))
+        continue;
+
+      const auto &SuccBits = Succ->Candidates.Bits;
+
+      // If they have no common candidates it means there's a cast
+      if ((SuccBits & NodeBits) == 0)
+        Cost += 1;
+    }
+
+    Visited.insert(TGNode);
+  }
+
+  return Cost;
+}
+
+/// \brief If the majority of the neighbors agree on a color, return it
+///
+/// Under certain conditions, we can color a node only looking at its decided
+/// neighbors, i.e. those neighbors that are colored with exactly one color.
+/// In particular, if the majority of the decided neighbors agree on a color,
+/// and the node can be colored with that color, we are sure that the node
+/// should be colored with that color.
+/// The voting works as follows: if the number of decided neighbors who agree on
+/// a color is such that it would remain the most popular color even if all the
+/// undecided nodes were to be assigned to any other color, then the color wind
+/// the majority voting.
+static llvm::Optional<ColorSet> majorityVote(const TypeFlowNode *Node) {
+  // Don't try to assign a color to an already decided or uncolored node
+  revng_assert(Node->isUndecided());
+
+  ///\brief Holds a counter for a given color
+  struct ColorFrequency {
+    ColorSet Color;
+    unsigned Frequency;
+
+    ColorFrequency() = delete;
+    ColorFrequency(ColorIndex Idx) : Color(1 << Idx), Frequency(0) {}
+  };
+
+  // Create a counter for each color
+  llvm::SmallVector<ColorFrequency, MAX_COLORS> ColorCounters;
+
+  for (size_t I = 0; I < MAX_COLORS; ++I)
+    ColorCounters.push_back(ColorIndex(I));
+
+  // For each color, count the number of decided neighbors with that color
+  int NUndecided = 0;
+  for (const TypeFlowNode *Succ : Node->successors()) {
+    const ColorSet SuccColor = Succ->Candidates;
+
+    if (Succ->isDecided() and Node->Candidates.contains(SuccColor)) {
+      // Since the node is decided, its color has exactly one set bit
+      ColorIndex I = SuccColor.firstSetBit();
+      // The index of the set bit corresponds to the color
+      ColorCounters[I].Frequency += 1;
+    } else if (Succ->isUndecided()) {
+      NUndecided++;
+    }
+  }
+
+  auto SortByFrequency = [](ColorFrequency &CF1, ColorFrequency &CF2) {
+    return CF1.Frequency > CF2.Frequency;
+  };
+
+  llvm::sort(ColorCounters, SortByFrequency);
+
+  ColorFrequency Max = ColorCounters[0];
+  ColorFrequency SecondMax = ColorCounters[1];
+
+  // If the most common color among the decided neighbors is still the most
+  // common even if all the undecided nodes are colored with the second most
+  // common color, then we have a winner.
+  if (Max.Frequency > (SecondMax.Frequency + NUndecided)) {
+    revng_assert(Node->Candidates.contains(Max.Color));
+    return Max.Color;
+  }
+
+  return {};
+}
+
+bool vma::applyMajorityVoting(TypeFlowGraph &TG) {
+  bool Modified = false;
+
+  do {
+    Modified = false;
+
+    for (TypeFlowNode *N : TG.nodes()) {
+      if (N->isUndecided()) {
+        // Check if the neighbors of a node agree on a certain color
+        if (auto VotedColor = majorityVote(N)) {
+          N->Candidates = *VotedColor;
+          Modified = true;
+        }
+      }
+    }
+  } while (Modified);
+
+  return Modified;
+}
diff --git a/lib/ValueManipulationAnalysis/TypeFlowGraph.h b/lib/ValueManipulationAnalysis/TypeFlowGraph.h
new file mode 100644
index 000000000..083cd04c4
--- /dev/null
+++ b/lib/ValueManipulationAnalysis/TypeFlowGraph.h
@@ -0,0 +1,106 @@
+#pragma once
+
+//
+// Copyright rev.ng Srls. See LICENSE.md for details.
+//
+
+#include <set>
+
+#include "llvm/ADT/DenseMap.h"
+#include "llvm/IR/Function.h"
+#include "llvm/Support/raw_ostream.h"
+
+#include "revng/ADT/FilteredGraphTraits.h"
+#include "revng/ADT/GenericGraph.h"
+
+#include "revng-c/ValueManipulationAnalysis/TypeColors.h"
+
+#include "TypeFlowNode.h"
+
+namespace vma {
+
+// --------------- TypeFlowGraph
+
+/// \brief Graph representing how type information flows between values and uses
+///
+/// Nodes represent `llvm::Value`s and `llvm::Use`s and their candidate types,
+/// edges represent how type information is propagated.
+struct TypeFlowGraph : public GenericGraph<TypeFlowNode> {
+  TypeFlowGraph() = default;
+  TypeFlowGraph(const TypeFlowGraph &N) = default;
+  TypeFlowGraph(TypeFlowGraph &&N) = default;
+  TypeFlowGraph &operator=(const TypeFlowGraph &N) = default;
+  TypeFlowGraph &operator=(TypeFlowGraph &&N) = default;
+
+  TypeFlowNode *addNodeContaining(const UseOrValue &);
+  TypeFlowNode *getNodeContaining(const UseOrValue &) const;
+
+  /// \brief Print the graph on a `.dot` file
+  /// \param Title title of the graph
+  /// \param FileName if not specified, the default is `/tmp/<random string>`
+  void
+  dump(const llvm::Twine &Title = "", std::string FileName = "") debug_function;
+
+  /// \brief Dump a dot representation of the graph to the given stream
+  void print(llvm::raw_ostream &OS) debug_function;
+
+  /// \brief Show the graph in a window, to be used inside a debugger
+  void view() debug_function;
+
+  const llvm::Function *Func;
+  std::map<UseOrValue, TypeFlowNode *> ContentToNodeMap;
+};
+
+// --------------- TypeFlowGraph manipulation
+
+/// \brief Add to \a TG the `llvm::Use`s and `llvm::Value`s inside \a F
+TypeFlowGraph makeTypeFlowGraphFromFunction(const llvm::Function *F);
+
+/// \brief Propagate colors from colored nodes trough colored edges
+void propagateColors(TypeFlowGraph &TG);
+
+/// \brief Propagate a single color
+template<unsigned Filter>
+void propagateColor(TypeFlowGraph &TG);
+
+/// \brief Propagate Numberness and Pointerness with special rules
+/// \return true if the TypeFlowGraph was modified
+bool propagateNumberness(TypeFlowGraph &TG);
+
+///\brief Make the graph undirected by adding all reciprocal edges
+void makeBidirectional(TypeFlowGraph &TG);
+
+/// \brief Count the number of edges connecting nodes with disjoint candidates
+unsigned countCasts(const TypeFlowGraph &TG);
+
+/// \brief Recursively assign grey nodes based on the color of their neighbors
+///
+/// See also TypeFlowNode::majorityVote()
+/// \return True if at least one node was modified
+bool applyMajorityVoting(TypeFlowGraph &TG);
+
+// --------------- Filtered Graphs implementation
+
+/// \brief Select only edge that contain a given color
+template<unsigned FilterColor>
+inline bool hasColor(llvm::GraphTraits<TypeFlowGraph *>::EdgeRef &Edge) {
+  return Edge.Colors.contains(FilterColor);
+}
+
+/// \brief Filtered Graph with only edges of a given color
+template<unsigned FilterColor>
+using EdgeFilteredTG = EdgeFilteredGraph<TypeFlowNode *, hasColor<FilterColor>>;
+
+/// \brief Select only undecided nodes
+inline bool
+bothHaveManyCandidates(const llvm::GraphTraits<TypeFlowGraph *>::NodeRef &Src,
+                       const llvm::GraphTraits<TypeFlowGraph *>::NodeRef &Tgt) {
+
+  return Src->isUndecided() and Tgt->isUndecided();
+}
+
+/// \brief Filtered Graph with only undecided nodes
+using NodeFilteredTG = NodePairFilteredGraph<TypeFlowNode *,
+                                             bothHaveManyCandidates>;
+
+} // namespace vma
diff --git a/lib/ValueManipulationAnalysis/TypeFlowGraphWriter.h b/lib/ValueManipulationAnalysis/TypeFlowGraphWriter.h
new file mode 100644
index 000000000..e8dc6fda7
--- /dev/null
+++ b/lib/ValueManipulationAnalysis/TypeFlowGraphWriter.h
@@ -0,0 +1,185 @@
+#pragma once
+
+//
+// Copyright rev.ng Srls. See LICENSE.md for details.
+//
+
+#include <map>
+#include <ostream>
+
+#include "llvm/IR/Function.h"
+#include "llvm/IR/InstIterator.h"
+#include "llvm/IR/Instruction.h"
+#include "llvm/Support/DOTGraphTraits.h"
+#include "llvm/Support/Debug.h"
+#include "llvm/Support/GraphWriter.h"
+
+#include "revng/Support/Assert.h"
+#include "revng/Support/IRHelpers.h"
+
+#include "revng-c/ValueManipulationAnalysis/TypeColors.h"
+
+#include "TypeFlowGraph.h"
+
+namespace llvm {
+
+template<>
+struct DOTGraphTraits<vma::TypeFlowGraph *> : public DefaultDOTGraphTraits {
+  using GraphT = vma::TypeFlowGraph *;
+  using NodeT = typename llvm::GraphTraits<GraphT>::NodeRef;
+  using EdgeIteratorT = typename llvm::GraphTraits<GraphT>::ChildIteratorType;
+  static constexpr inline int IgnoreGraphvizPorts = -1;
+
+  // Colors for printing ColorSets
+  static constexpr llvm::StringRef ColorCode[vma::MAX_COLORS] = {
+    // pointerness
+    "\"#8db596\"",
+    // unsignedness
+    "\"#ec5858\"",
+    // boolness
+    "\"#93abd3\"",
+    // signedness
+    "\"#fd8c04\"",
+    // floatness
+    "\"#734046\"",
+    // numberness
+    "white"
+  };
+
+  DOTGraphTraits(bool IsSimple = false) : DefaultDOTGraphTraits(IsSimple) {}
+
+  static std::string getGraphName(GraphT G) {
+    StringRef FuncName = G->Func->getName();
+    return "TypeFlowGraph of " + FuncName.str();
+  }
+
+  static std::string getNodeLabel(NodeT Node, GraphT Graph) {
+    std::string OutSStr;
+    llvm::raw_string_ostream Out(OutSStr);
+
+    // Node label
+    if (Node->isValue()) {
+      const Value *V = Node->getValue();
+
+      if (isa<Argument>(V))
+        Out << "arg ";
+
+      if (isa<Instruction>(V))
+        Out << *(dyn_cast<Instruction>(V));
+      else
+        V->printAsOperand(Out);
+
+      Out << "}\n{";
+    } else {
+      const Use *U = Node->getUse();
+
+      // Const uses have labels, since const nodes are not printed
+      if (isa<ConstantData>(U->get())) {
+        Out << "const ";
+        U->get()->printAsOperand(Out);
+
+        Out << "}\n{";
+      }
+    }
+
+    // Node colors
+    Out << "color : " << dumpToString(Node->Candidates)
+        << "}\n{accepted: " << dumpToString(Node->Accepted);
+
+    return Out.str();
+  }
+
+  static std::string getNodeAttributes(NodeT Node, GraphT Graph) {
+    std::string OutSStr;
+    llvm::raw_string_ostream Out(OutSStr);
+
+    // Draw a square for values and a circle for uses
+    if (Node->isUse()) {
+      const Use *U = Node->getUse();
+
+      Out << "shape=oval, width=0.3, height=0.3, tooltip=\"operand #"
+          << U->getOperandNo() << "\"";
+    } else {
+      Out << "shape=box ";
+      if (Node->isValue()
+          and (Node->getValue()->getType()->isLabelTy()
+               or Node->getValue()->getType()->isVoidTy()))
+        Out << ", color=lightgrey ";
+    }
+
+    // Fill nodes: 0 colors = white, 1 color = colored, > 1 color = grey
+    if (Node->isUndecided()) {
+      Out << " style=filled, fillcolor=lightgrey, color=lightgrey";
+    } else if (Node->isDecided()) {
+      auto First = Node->Candidates.firstSetBit();
+      revng_assert(First != vma::NUMBERNESS_INDEX);
+
+      Out << " style=filled, fillcolor=" << ColorCode[First].str()
+          << ", color=" << ColorCode[First].str();
+    }
+
+    return Out.str();
+  }
+
+  static bool isNodeHidden(NodeT Node) {
+    // Don't print a node and its incoming/outgoing edges if it's a constant
+    // Constant values are printed in their Uses nodes, to not pollute the
+    // graph with meaningless arcs between the same constant and multiple
+    // uses.
+    if (Node->isValue() and isa<ConstantData>(Node->getValue()))
+      return true;
+    return false;
+  }
+
+  static std::string
+  getEdgeAttributes(NodeT Node, EdgeIteratorT EI, GraphT Graph) {
+    return "constraint=false, color=\"#8bcdcd\", fontcolor=\"#3797a4\", "
+           "labeldistance=2,"
+           "labelangle=40,"
+           " headlabel=\""
+           + dumpToString(EI.getCurrent()->Colors) + "\"";
+  }
+
+  static void addCustomGraphFeatures(GraphT G, GraphWriter<GraphT> &GW) {
+    const Function *F = G->Func;
+
+    // Add dataflow arrows (Operand -> OpUse -> Instruction):
+    // This gives a better ranking of the nodes and a better overall
+    // understanding of the graph.
+    for (const Instruction &I : instructions(*F)) {
+      if (not G->ContentToNodeMap.contains(&I)
+          or isNodeHidden(G->getNodeContaining(&I)))
+        continue;
+
+      NodeT ValNode = G->getNodeContaining(&I);
+
+      for (const auto &O : I.operands()) {
+        // Connect Operand Uses to Instructions
+        if (not G->ContentToNodeMap.contains(&O)
+            or isNodeHidden(G->getNodeContaining(&O)))
+          continue;
+
+        NodeT OpUse = G->getNodeContaining(&O);
+        GW.emitEdge(OpUse,
+                    IgnoreGraphvizPorts,
+                    ValNode,
+                    IgnoreGraphvizPorts,
+                    "color=lightgrey, minlen=2");
+
+        // Connect Operands to Operand Uses
+        if (not G->ContentToNodeMap.contains(O.get())
+            or isNodeHidden(G->getNodeContaining(O.get())))
+          continue;
+
+        NodeT OpNode = G->getNodeContaining(O.get());
+        GW.emitEdge(OpNode,
+                    IgnoreGraphvizPorts,
+                    OpUse,
+                    IgnoreGraphvizPorts,
+                    "color=lightgrey, minlen=2");
+      }
+    }
+  }
+};
+
+} // namespace llvm
\ No newline at end of file
diff --git a/lib/ValueManipulationAnalysis/TypeFlowNode.cpp b/lib/ValueManipulationAnalysis/TypeFlowNode.cpp
new file mode 100644
index 000000000..041fcd418
--- /dev/null
+++ b/lib/ValueManipulationAnalysis/TypeFlowNode.cpp
@@ -0,0 +1,200 @@
+//
+// Copyright rev.ng Srls. See LICENSE.md for details.
+//
+
+#include <algorithm>
+#include <cstddef>
+#include <variant>
+
+#include "llvm/ADT/STLExtras.h"
+#include "llvm/IR/Constants.h"
+#include "llvm/IR/GlobalValue.h"
+#include "llvm/IR/Instruction.h"
+#include "llvm/IR/Instructions.h"
+
+#include "revng/Support/Assert.h"
+#include "revng/Support/IRHelpers.h"
+
+#include "revng-c/ValueManipulationAnalysis/TypeColors.h"
+
+#include "TypeFlowNode.h"
+
+using namespace vma;
+using namespace llvm;
+
+NodeColorProperty vma::nodeColors(const UseOrValue &Content) {
+  // Arguments, constants, globals etc.
+  if (isValue(Content)) {
+    const Value *V = getValue(Content);
+
+    if (isa<Argument>(V))
+      return { /*initial=*/NO_COLOR, /*accepted=*/ALL_COLORS };
+
+    // Constants and globals should not be infected, since they don't belong to
+    // a single function
+    if (isa<Constant>(V) or isa<GlobalValue>(V))
+      return { /*initial=*/NO_COLOR, /*accepted=*/NO_COLOR };
+
+    if (not isa<Instruction>(V))
+      return { /*initial=*/NO_COLOR, /*accepted=*/NO_COLOR };
+  }
+
+  // Instructions and operand uses should be the only thing remaining
+  bool IsContentInst = isInst(Content);
+  revng_assert(IsContentInst or isUse(Content));
+
+  // If the content of the node is an Instruction's Value, assign colors
+  // based on the instruction's opcode. Otherwise, if we are creating a node for
+  // one of the operands, find which the user of the operand and check its
+  // opcode.
+  const Instruction *I = IsContentInst ?
+                           cast<Instruction>(getValue(Content)) :
+                           cast<Instruction>(getUse(Content)->getUser());
+
+  switch (I->getOpcode()) {
+  case Instruction::FNeg:
+  case Instruction::FAdd:
+  case Instruction::FMul:
+  case Instruction::FSub:
+  case Instruction::FDiv:
+  case Instruction::FRem:
+  case Instruction::FPExt:
+    return { /*initial=*/FLOATNESS, /*accepted=*/FLOATNESS };
+    break;
+
+  case Instruction::FCmp:
+    if (IsContentInst)
+      return { /*initial=*/BOOLNESS, /*accepted=*/BOOLNESS };
+    else
+      return { /*initial=*/FLOATNESS, /*accepted=*/FLOATNESS };
+    break;
+
+  case Instruction::ICmp:
+    if (IsContentInst)
+      return { /*initial=*/BOOLNESS, /*accepted=*/BOOLNESS };
+    if (cast<ICmpInst>(I)->isSigned())
+      return { /*initial=*/SIGNEDNESS, /*accepted=*/SIGNEDNESS };
+    if (cast<ICmpInst>(I)->isUnsigned())
+      return { /*initial=*/UNSIGNEDNESS,
+               /*accepted=*/UNSIGNEDNESS | POINTERNESS };
+    break;
+
+  case Instruction::SDiv:
+  case Instruction::SRem:
+    return { /*initial=*/(SIGNEDNESS | NUMBERNESS),
+             /*accepted=*/(SIGNEDNESS | NUMBERNESS) };
+    break;
+
+  case Instruction::UDiv:
+  case Instruction::URem:
+    return { /*initial=*/(UNSIGNEDNESS | NUMBERNESS),
+             /*accepted=*/(UNSIGNEDNESS | NUMBERNESS) };
+    break;
+
+  case Instruction::Alloca:
+    if (IsContentInst)
+      return { /*initial=*/POINTERNESS,
+               /*accepted=*/POINTERNESS };
+    if (getUse(Content)->get() == cast<AllocaInst>(I)->getArraySize())
+      return { /*initial=*/UNSIGNEDNESS,
+               /*accepted=*/UNSIGNEDNESS };
+    break;
+
+  case Instruction::Load:
+    if (isUse(Content)
+        && getOpNo(Content) == cast<LoadInst>(I)->getPointerOperandIndex())
+      return { /*initial=*/POINTERNESS,
+               /*accepted=*/POINTERNESS };
+    break;
+
+  case Instruction::Store:
+    if (isUse(Content)
+        && getOpNo(Content) == cast<StoreInst>(I)->getPointerOperandIndex())
+      return { /*initial=*/POINTERNESS,
+               /*accepted=*/POINTERNESS };
+    break;
+
+  case Instruction::AShr:
+    if (IsContentInst or getOpNo(Content) == 0)
+      return { /*initial=*/SIGNEDNESS,
+               /*accepted=*/SIGNEDNESS };
+    if (getOpNo(Content) == 1)
+      return { /*initial=*/UNSIGNEDNESS,
+               /*accepted=*/~(FLOATNESS | POINTERNESS) };
+    break;
+
+  case Instruction::LShr:
+    if (IsContentInst or getOpNo(Content) == 0)
+      // TODO: rule on first operand too strict?
+      return { /*initial=*/UNSIGNEDNESS,
+               /*accepted=*/UNSIGNEDNESS };
+    if (getOpNo(Content) == 1)
+      return { /*initial=*/UNSIGNEDNESS,
+               /*accepted=*/~(FLOATNESS | POINTERNESS) };
+    break;
+
+  case Instruction::Shl:
+    if (IsContentInst)
+      return { /*initial=*/NO_COLOR,
+               /*accepted=*/~(FLOATNESS | POINTERNESS) };
+    if (getOpNo(Content) == 0)
+      // TODO: rule on first operand too strict?
+      return { /*initial = */ NO_COLOR,
+               /*accepted=*/
+               (SIGNEDNESS | UNSIGNEDNESS | BOOLNESS) };
+    if (getOpNo(Content) == 1)
+      return { /*initial=*/UNSIGNEDNESS,
+               /*accepted=*/~(FLOATNESS | POINTERNESS) };
+    break;
+
+  case Instruction::Mul:
+    return { /*initial=*/NUMBERNESS,
+             /*accepted=*/~(FLOATNESS | POINTERNESS) };
+    break;
+
+  case Instruction::Br:
+    if (isUse(Content) && cast<BranchInst>(I)->isConditional()
+        && getUse(Content)->get() == cast<BranchInst>(I)->getCondition())
+      return { /*initial=*/BOOLNESS, /*accepted=*/BOOLNESS };
+    break;
+
+  case Instruction::Select:
+    if (isUse(Content)
+        && getUse(Content)->get() == cast<SelectInst>(I)->getCondition())
+      return { /*initial=*/BOOLNESS, /*accepted=*/BOOLNESS };
+    break;
+
+  case Instruction::Trunc:
+  case Instruction::And:
+  case Instruction::Or:
+  case Instruction::Xor:
+    // TODO: Restrict more what can be accepted by bitwise operations?
+    return { /*initial=*/NO_COLOR, /*accepted=*/~NUMBERNESS };
+    break;
+
+  case Instruction::GetElementPtr:
+    revng_abort("Didn't expect to find a GEP here");
+    break;
+  }
+
+  return { /*initial=*/NO_COLOR, /*accepted=*/~NUMBERNESS };
+}
+
+void TypeFlowNodeData::print(llvm::raw_ostream &Out) const {
+  if (this->isValue()) {
+    Out << "value ";
+    this->getValue()->print(Out);
+  } else {
+    Value *Val = this->getUse()->get();
+    Value *User = this->getUse()->getUser();
+
+    Out << "use of ";
+    Val->printAsOperand(Out);
+    Out << " in ";
+    User->print(Out);
+  }
+}
+
+std::string TypeFlowNodeData::toString() const {
+  return dumpToString(this);
+}
diff --git a/lib/ValueManipulationAnalysis/TypeFlowNode.h b/lib/ValueManipulationAnalysis/TypeFlowNode.h
new file mode 100644
index 000000000..2c7af8580
--- /dev/null
+++ b/lib/ValueManipulationAnalysis/TypeFlowNode.h
@@ -0,0 +1,128 @@
+#pragma once
+
+//
+// Copyright rev.ng Srls. See LICENSE.md for details.
+//
+#include <variant>
+
+#include "llvm/ADT/DenseMap.h"
+#include "llvm/IR/Instruction.h"
+#include "llvm/IR/Use.h"
+#include "llvm/IR/Value.h"
+#include "llvm/Support/raw_ostream.h"
+
+#include "revng/ADT/GenericGraph.h"
+#include "revng/Support/Assert.h"
+
+#include "revng-c/ValueManipulationAnalysis/TypeColors.h"
+
+namespace vma {
+
+// --------------- Node content
+
+/// \brief The atomic element to which we want to attach type information
+using UseOrValue = std::variant<const llvm::Use *, const llvm::Value *>;
+
+inline bool isValue(const UseOrValue &Content) {
+  return std::holds_alternative<const llvm::Value *>(Content);
+};
+
+inline bool isUse(const UseOrValue &Content) {
+  return std::holds_alternative<const llvm::Use *>(Content);
+};
+
+inline const llvm::Value *getValue(const UseOrValue &Content) {
+  revng_assert(isValue(Content));
+  return std::get<const llvm::Value *>(Content);
+};
+
+inline const llvm::Use *getUse(const UseOrValue &Content) {
+  revng_assert(isUse(Content));
+  return std::get<const llvm::Use *>(Content);
+};
+
+///\brief Check if the variant is holding an Instruction's output Value
+inline bool isInst(const UseOrValue &Content) {
+  return isValue(Content) && isa<llvm::Instruction>(getValue(Content));
+}
+
+///\brief Get the index of an operand inside its Instruction
+inline unsigned getOpNo(const UseOrValue &Content) {
+  revng_assert(isUse(Content));
+  return getUse(Content)->getOperandNo();
+};
+
+// --------------- Node Color initialization
+
+///\brief Represents the initial color of a node and the ones it can accept
+struct NodeColorProperty {
+  const ColorSet InitialColor = NO_COLOR;
+  const ColorSet AcceptedColors = NO_COLOR;
+
+  NodeColorProperty(ColorSet Initial, ColorSet Accepted) :
+    InitialColor(Initial), AcceptedColors(Accepted) {}
+};
+
+/// \brief Return the type colors associated to a given Use or Value
+NodeColorProperty nodeColors(const UseOrValue &NC);
+
+// --------------- TypeFlowGraph Node
+
+/// \brief Label of a TypeFlowGraph edge
+///
+/// Indicates which colors can be propagated from the source node to the target
+/// node of an edge on the TypeFlowGraph.
+struct EdgeLabel {
+  ColorSet Colors;
+
+  EdgeLabel() : Colors(NO_COLOR) {}
+  EdgeLabel(ColorSet C) : Colors(C) {}
+  EdgeLabel(unsigned U) : Colors(U) {}
+};
+
+/// \brief Node data containing colors for an `llvm::Use` or `llvm::Value`
+class TypeFlowNodeData {
+public:
+  ///\brief LLVM Use or Value to which the type information is attached
+  const UseOrValue Content;
+  ///\brief Candidate types for this node
+  ColorSet Candidates;
+  ///\brief Types which this node can be infected with
+  const ColorSet Accepted;
+
+public:
+  TypeFlowNodeData() = delete;
+  TypeFlowNodeData(const UseOrValue &NC, const NodeColorProperty Colors) :
+    Content(NC),
+    Candidates(Colors.InitialColor),
+    Accepted(Colors.AcceptedColors) {}
+
+  TypeFlowNodeData(const TypeFlowNodeData &N) = default;
+  TypeFlowNodeData(TypeFlowNodeData &&N) = default;
+  TypeFlowNodeData &operator=(const TypeFlowNodeData &N) = delete;
+  TypeFlowNodeData &operator=(TypeFlowNodeData &&N) = delete;
+
+public:
+  bool isUse() const { return vma::isUse(Content); }
+  bool isValue() const { return vma::isValue(Content); }
+  const llvm::Use *getUse() const { return vma::getUse(Content); }
+  const llvm::Value *getValue() const { return vma::getValue(Content); }
+
+  /// \brief Has no candidate color
+  bool isUncolored() const { return Candidates.countValid() == 0; }
+  /// \brief Has exactly one candidate color
+  bool isDecided() const { return Candidates.countValid() == 1; }
+  /// \brief Has more than one candidate color
+  bool isUndecided() const { return Candidates.countValid() > 1; }
+
+  /// \brief Print a textual representation of the node's content
+  void print(llvm::raw_ostream &Out) const debug_function;
+
+  /// \brief Print the content of the node to a string
+  std::string toString() const debug_function;
+};
+
+/// \brief Add GenericGraph's BidirectionalNode interface
+using TypeFlowNode = BidirectionalNode<TypeFlowNodeData, EdgeLabel, false>;
+
+} // namespace vma
diff --git a/lib/ValueManipulationAnalysis/ValueManipulationAnalysis.cpp b/lib/ValueManipulationAnalysis/ValueManipulationAnalysis.cpp
new file mode 100644
index 000000000..c40efac45
--- /dev/null
+++ b/lib/ValueManipulationAnalysis/ValueManipulationAnalysis.cpp
@@ -0,0 +1,100 @@
+//
+// Copyright rev.ng Srls. See LICENSE.md for details.
+//
+
+#include <cstddef>
+
+#include "llvm/ADT/STLExtras.h"
+#include "llvm/Support/Debug.h"
+
+#include "revng/Model/LoadModelPass.h"
+#include "revng/Support/Assert.h"
+#include "revng/Support/FunctionTags.h"
+
+#include "revng-c/ValueManipulationAnalysis/TypeColors.h"
+#include "revng-c/ValueManipulationAnalysis/ValueManipulationAnalysis.h"
+
+#include "Mincut.h"
+#include "TypeFlowGraph.h"
+#include "TypeFlowNode.h"
+
+using namespace llvm;
+using namespace vma;
+
+static Logger<> VMALog("vma");
+static Logger<> GraphLog("vma-graph");
+static Logger<> TimerLogger("vma-timer");
+
+char ValueManipulationAnalysis::ID = 0;
+using Register = RegisterPass<ValueManipulationAnalysis>;
+static Register X("vma", "Value Manipulation Analysis", false, false);
+
+using VMA = ValueManipulationAnalysis;
+
+// LLVM Pass
+void VMA::getAnalysisUsage(llvm::AnalysisUsage &AU) const {
+  AU.addRequired<LoadModelWrapperPass>();
+  AU.setPreservesAll();
+}
+
+bool VMA::runOnFunction(Function &F) {
+  // Skip non-isolated functions
+  auto FTags = FunctionTags::TagsSet::from(&F);
+  if (not FTags.contains(FunctionTags::Lifted))
+    return false;
+
+  revng_log(VMALog, "------ Function: " << F.getName() << " ------");
+
+  // Color initialization
+  ColorMap.clear();
+  TypeFlowGraph TG = makeTypeFlowGraphFromFunction(&F);
+
+  // Color propagation
+  do {
+    propagateColors(TG);
+  } while (propagateNumberness(TG));
+
+  // Mincut preprocessing
+  makeBidirectional(TG);
+  applyMajorityVoting(TG);
+
+  if (GraphLog.isEnabled())
+    TG.view();
+
+  // Assign grey nodes
+  if (llvm::any_of(TG.nodes(),
+                   [](TypeFlowNode *N) { return N->isUndecided(); })) {
+
+    revng_log(VMALog, "Executing mincut");
+
+    std::chrono::steady_clock::time_point Begin;
+    if (TimerLogger.isEnabled()) {
+      Begin = std::chrono::steady_clock::now();
+    }
+
+    minCut(TG);
+
+    if (TimerLogger.isEnabled()) {
+      auto End = std::chrono::steady_clock::now();
+      auto Dur = End - Begin;
+      revng_log(TimerLogger, "total time: " << Dur.count());
+      revng_log(TimerLogger, "total dim: " << TG.size());
+    }
+  } else {
+    revng_log(VMALog, "Nothing to assign");
+  }
+
+  if (GraphLog.isEnabled())
+    TG.view();
+  revng_log(VMALog, "Total function cost: " << countCasts(TG));
+
+  // Populate Output Map
+  for (const auto *N : TG.nodes()) {
+    revng_assert(N->Candidates.countValid() <= 1);
+
+    if (N->isValue())
+      ColorMap.insert({ N->getValue(), N->Candidates });
+  }
+
+  return false;
+}
diff --git a/tests/Unit/UnitTests.cmake b/tests/Unit/UnitTests.cmake
index 32788a6b2..003bede4b 100644
--- a/tests/Unit/UnitTests.cmake
+++ b/tests/Unit/UnitTests.cmake
@@ -50,6 +50,24 @@ target_link_libraries(test_combingpass
   ${LLVM_LIBRARIES})
 add_test(NAME test_combingpass COMMAND ./bin/test_combingpass -- "${SRC}/TestGraphs/")
 
+#
+# test_vma
+#
+
+revng_add_private_executable(test_vma "${SRC}/ValueManipulationAnalysis.cpp")
+target_compile_definitions(test_vma
+  PRIVATE "BOOST_TEST_DYN_LINK=1")
+target_include_directories(test_vma
+  PRIVATE "${CMAKE_SOURCE_DIR}")
+target_link_libraries(test_vma
+  ValueManipulationAnalysis
+  revng::revngSupport
+  Boost::unit_test_framework
+  ${LLVM_LIBRARIES})
+add_test(NAME test_vma COMMAND ./bin/test_vma)
+set_tests_properties(test_vma PROPERTIES LABELS "unit")
+
+
 revng_add_private_executable(decompile_function "${SRC}/DecompileFunction.cpp")
 target_include_directories(decompile_function
   PRIVATE "${CMAKE_SOURCE_DIR}"
@@ -60,6 +78,7 @@ target_link_libraries(decompile_function
   Decompiler
   revng::revngModel
   revng::revngSupport
+  Boost::unit_test_framework
   ${LLVM_LIBRARIES})
 
 # End-to-end tests for the decompilation pipeline public API decompileFunction
diff --git a/tests/Unit/ValueManipulationAnalysis.cpp b/tests/Unit/ValueManipulationAnalysis.cpp
new file mode 100644
index 000000000..4ca22d298
--- /dev/null
+++ b/tests/Unit/ValueManipulationAnalysis.cpp
@@ -0,0 +1,724 @@
+/// \file ValueManipulationAnalysis.cpp
+/// \brief Test the ValueManipulationAnalysis analysis
+
+//
+// Copyright rev.ng Srls. See LICENSE.md for details.
+//
+
+#define BOOST_TEST_MODULE ValueManipulationAnalysis
+bool init_unit_test();
+
+#include "boost/test/unit_test.hpp"
+
+#include "llvm/ADT/STLExtras.h"
+#include "llvm/IR/InstIterator.h"
+#include "llvm/IR/Verifier.h"
+
+#include "revng/Support/Debug.h"
+#include "revng/Support/IRHelpers.h"
+#include "revng/UnitTestHelpers/LLVMTestHelpers.h"
+#include "revng/UnitTestHelpers/UnitTestHelpers.h"
+
+#include "revng-c/ValueManipulationAnalysis/TypeColors.h"
+#include "revng-c/ValueManipulationAnalysis/ValueManipulationAnalysis.h"
+
+#include "lib/ValueManipulationAnalysis/Mincut.h"
+#include "lib/ValueManipulationAnalysis/TypeFlowGraph.h"
+#include "lib/ValueManipulationAnalysis/TypeFlowNode.h"
+
+using namespace llvm;
+using namespace vma;
+
+// Node types
+enum NodeType : unsigned { VALUE, USE, MAX_TYPES };
+const inline std::string NodeTypeName[MAX_TYPES] = { "values", "uses  " };
+
+// Counters
+using ColorCounter = std::array<unsigned, MAX_COLORS>;
+using TypeCounter = std::array<unsigned, MAX_TYPES>;
+
+struct ExpectedShape {
+  TypeCounter Types;
+  ColorCounter Colors;
+  unsigned NCasts;
+  unsigned NUndecided;
+
+  ExpectedShape(TypeCounter T,
+                ColorCounter C,
+                unsigned NCasts,
+                unsigned NUndecided) :
+    Types(T), Colors(C), NCasts(NCasts), NUndecided(NUndecided) {}
+};
+
+///\brief Keep a count of how many nodes are colored with each color
+static ColorCounter countColors(const TypeFlowGraph &TG) {
+  ColorCounter CC = { 0 };
+
+  for (const TypeFlowNode *const N : nodes(&TG))
+    for (size_t I = 0; I < MAX_COLORS; I++)
+      CC[I] += N->Candidates.Bits.test(I);
+
+  return CC;
+}
+
+///\brief Keep a count of how many nodes of each type there are in \a TG
+static TypeCounter countTypes(const TypeFlowGraph &TG) {
+  TypeCounter TC = { 0 };
+
+  for (const TypeFlowNode *const N : nodes(&TG)) {
+    if (N->isUse())
+      TC[USE] += 1;
+    else if (N->isValue())
+      TC[VALUE] += 1;
+    else
+      revng_abort();
+  }
+
+  return TC;
+}
+
+/// \brief Check that the TG nodes have the expected types and colors
+static void checkShape(const TypeFlowGraph &TG, const ExpectedShape &Expected) {
+  const TypeCounter &ExpectedTypes = Expected.Types;
+  const ColorCounter &ExpectedColors = Expected.Colors;
+  const TypeCounter ActualType = countTypes(TG);
+  const ColorCounter ActualColor = countColors(TG);
+
+  dbgs() << " What    Expected  Actual\n";
+
+  // Check that there are the expected number of nodes of each type
+  for (size_t I = 0; I < MAX_TYPES; I++) {
+    dbgs() << NodeTypeName[I] << "\t" << ExpectedTypes[I] << "\t"
+           << ActualType[I] << "\n";
+    revng_check(ExpectedTypes[I] == ActualType[I]);
+  }
+
+  // Check that there are the expected number of nodes of each color
+  for (size_t I = 0; I < MAX_COLORS; I++) {
+    dbgs() << vma::TypeColorName[I] << "    \t" << ExpectedColors[I] << "\t"
+           << ActualColor[I] << "\n";
+    revng_check(ActualColor[I] == ExpectedColors[I]);
+  }
+
+  // Check number of casts in the graph
+  unsigned ActualCasts = countCasts(TG);
+  dbgs() << "casts \t" << Expected.NCasts << "\t" << ActualCasts << "\n";
+  revng_check(Expected.NCasts == ActualCasts);
+
+  // Check number of undecided nodes
+  auto IsUndecided = [](const TypeFlowNode *N) { return N->isUndecided(); };
+  unsigned NUndecided = llvm::count_if(TG.nodes(), IsUndecided);
+  dbgs() << "undecided\t" << Expected.NUndecided << "\t" << NUndecided << "\n";
+  revng_check(NUndecided == Expected.NUndecided);
+}
+
+/// \brief Check that the information in the graph are consistent
+static void checkTGCorrectness(TypeFlowGraph &TG) {
+  // Check consistency between the graph and the reverse map
+  for (TypeFlowNode *N : TG.nodes()) {
+    auto MapIter = TG.ContentToNodeMap.find(N->Content);
+    revng_check(MapIter != TG.ContentToNodeMap.end());
+    revng_check(MapIter->second == N);
+  }
+
+  for (auto &Elem : TG.ContentToNodeMap) {
+    revng_check(Elem.second != nullptr);
+
+    auto NodeIter = llvm::find(TG.nodes(), Elem.second);
+    revng_check(NodeIter != TG.nodes().end());
+    revng_check((*NodeIter)->Content == Elem.first);
+  }
+
+  for (const TypeFlowNode *N : TG.nodes()) {
+    // Candidates should be a subset of accepted colors
+    revng_check(N->Accepted.contains(N->Candidates));
+    // Nodes can contain either uses or values
+    revng_check(N->isUse() xor N->isValue());
+
+    // If a Use node is in the TG, there must also be a node associated to the
+    // user and one for the used value
+    if (N->isUse()) {
+      revng_check(TG.ContentToNodeMap.contains(N->getUse()->get()));
+      revng_check(TG.ContentToNodeMap.contains(N->getUse()->getUser()));
+    }
+
+    // No double edges between nodes
+    for (const auto *Succ : N->successors())
+      revng_check(llvm::count(N->successors(), Succ));
+  }
+}
+
+///\brief Check that a TypeFlowGraph is initialized correctly from a function
+static void checkInit(const char *Body,
+                      const ExpectedShape ExpectedInit,
+                      const ExpectedShape ExpectedAfterProp,
+                      const ExpectedShape ExpectedFinal) {
+  // Read the LLVM IR
+  LLVMContext C;
+  std::unique_ptr<llvm::Module> M = loadModule(C, Body);
+  revng_check(not verifyModule(*M, &dbgs()));
+
+  Function *F = M->getFunction("main");
+
+  // Build the TG
+  TypeFlowGraph TG = makeTypeFlowGraphFromFunction(F);
+  checkTGCorrectness(TG);
+  checkShape(TG, ExpectedInit);
+
+  // Propagate
+  propagateColors(TG);
+  checkTGCorrectness(TG);
+  checkShape(TG, ExpectedAfterProp);
+
+  // Numberness
+  propagateNumberness(TG);
+  for (auto *N : TG.nodes())
+    revng_check(not N->Candidates.Bits.test(NUMBERNESS_INDEX));
+
+  // Undirected graph
+  makeBidirectional(TG);
+  for (auto *N : TG.nodes())
+    revng_check(llvm::size(N->successors()) == llvm::size(N->predecessors()));
+
+  // Mincut
+  minCut(TG);
+  checkShape(TG, ExpectedFinal);
+}
+
+// Test cases
+
+BOOST_AUTO_TEST_CASE(TestTGInit) {
+
+  VerifyLog.enable();
+
+  // Alloca
+  checkInit(R"LLVM(
+    %0 = alloca i32, align 4
+    %1 = alloca i32, align 4
+    unreachable
+  )LLVM",
+            /*Init=*/
+            { { /*values=*/3,
+                /*uses=*/0 },
+              { /*pointers=*/2,
+                /*unsigned=*/0,
+                /*bools=*/0,
+                /*signed=*/0,
+                /*floats=*/0,
+                /*numbers=*/0 },
+              /*casts=*/0,
+              /*undecided=*/0 },
+            /*After propagation=*/
+            { { /*values=*/3,
+                /*uses=*/0 },
+              { /*pointers=*/2,
+                /*unsigned=*/0,
+                /*bools=*/0,
+                /*signed=*/0,
+                /*floats=*/0,
+                /*numbers=*/0 },
+              /*casts=*/0,
+              /*undecided=*/0 },
+            /*Final=*/
+            { { /*values=*/3,
+                /*uses=*/0 },
+              { /*pointers=*/2,
+                /*unsigned=*/0,
+                /*bools=*/0,
+                /*signed=*/0,
+                /*floats=*/0,
+                /*numbers=*/0 },
+              /*casts=*/0,
+              /*undecided=*/0 });
+
+  // Alloca + Load
+  checkInit(R"LLVM(
+    %0 = alloca i32, align 4
+    %1 = alloca i32, align 4
+    %2 = load i32, i32* %0, align 4
+    %3 = load i32, i32* %1, align 4
+    unreachable
+  )LLVM",
+            /*Init=*/
+            { { /*values=*/5,
+                /*uses=*/2 },
+              { /*pointers=*/4,
+                /*unsigned=*/0,
+                /*bools=*/0,
+                /*signed=*/0,
+                /*floats=*/0,
+                /*numbers=*/0 },
+              /*casts=*/0,
+              /*undecided=*/0 },
+            /*After propagation=*/
+            { { /*values=*/5,
+                /*uses=*/2 },
+              { /*pointers=*/4,
+                /*unsigned=*/0,
+                /*bools=*/0,
+                /*signed=*/0,
+                /*floats=*/0,
+                /*numbers=*/0 },
+              /*casts=*/0,
+              /*undecided=*/0 },
+            /*Final=*/
+            { { /*values=*/5,
+                /*uses=*/2 },
+              { /*pointers=*/4,
+                /*unsigned=*/0,
+                /*bools=*/0,
+                /*signed=*/0,
+                /*floats=*/0,
+                /*numbers=*/0 },
+              /*casts=*/0,
+              /*undecided=*/0 });
+
+  // Ptr forward (with add)
+  checkInit(R"LLVM(
+    %0 = alloca i32, align 4
+    %1 = alloca i32, align 4
+    %2 = load i32, i32* %0, align 4
+    %3 = load i32, i32* %1, align 4
+    %4 = add i32 %2, %3
+    %5 = sdiv i32 %2, 2
+    %6 = inttoptr i32 %3 to i32*
+    store i32 10, i32* %6, align 4
+    unreachable
+  )LLVM",
+            /*Init=*/
+            { { /*values=*/9,
+                /*uses=*/7 },
+              { /*pointers=*/5,
+                /*unsigned=*/0,
+                /*bools=*/0,
+                /*signed=*/2,
+                /*floats=*/0,
+                /*numbers=*/2 },
+              /*casts=*/2,
+              /*undecided=*/0 },
+            /*After propagation=*/
+            { { /*values=*/9,
+                /*uses=*/7 },
+              { /*pointers=*/10, //< pointerness doesn't go past add
+                /*unsigned=*/0,
+                /*bools=*/0,
+                /*signed=*/9,
+                /*floats=*/0,
+                /*numbers=*/2 },
+              /*casts=*/0,
+              /*undecided=*/5 },
+            /*Final=*/
+            { { /*values=*/9,
+                /*uses=*/7 },
+              { /*pointers=*/10,
+                /*unsigned=*/0,
+                /*bools=*/0,
+                /*signed=*/4,
+                /*floats=*/0,
+                /*numbers=*/0 },
+              /*casts=*/1,
+              /*undecided=*/0 });
+
+  // Ptr backward (with add)
+  checkInit(R"LLVM(
+    %0 = alloca i32, align 4
+    %1 = alloca i32, align 4
+    %2 = load i32, i32* %0, align 4
+    %3 = load i32, i32* %1, align 4
+    %4 = add i32 %2, %3
+    %5 = inttoptr i32 %4 to i32*
+    store i32 10, i32* %5, align 4
+    unreachable
+  )LLVM",
+            /*Init=*/
+            { { /*value=*/8,
+                /*uses=*/6 },
+              { /*pointers=*/5,
+                /*unsigned=*/0,
+                /*bools=*/0,
+                /*signed=*/0,
+                /*floats=*/0,
+                /*numbers=*/0 },
+              /*casts=*/1,
+              /*undecided=*/0 },
+            /*After propagation=*/
+            { { /*value=*/8,
+                /*uses=*/6 },
+              { /*pointers=*/8,
+                /*unsigned=*/0,
+                /*bools=*/0,
+                /*signed=*/0,
+                /*floats=*/0,
+                /*numbers=*/0 },
+              /*casts=*/2,
+              /*undecided=*/0 },
+            /*Final=*/
+            { { /*value=*/8,
+                /*uses=*/6 },
+              { /*pointers=*/8,
+                /*unsigned=*/0,
+                /*bools=*/0,
+                /*signed=*/0,
+                /*floats=*/0,
+                /*numbers=*/0 },
+              /*casts=*/2,
+              /*undecided=*/0 });
+
+  // Side propagation (with add)
+  checkInit(R"LLVM(
+    %0 = alloca i32, align 4
+    %1 = alloca i32, align 4
+    %2 = load i32, i32* %0, align 4
+    %3 = load i32, i32* %1, align 4
+    %4 = add i32 %2, %3
+    %5 = sdiv i32 %2, 2
+    %6 = udiv i32 %3, 3
+    unreachable
+  )LLVM",
+            /*Init=*/
+            { { /*values=*/8,
+                /*uses=*/6 },
+              { /*pointers=*/4,
+                /*unsigned=*/2,
+                /*bools=*/0,
+                /*signed=*/2,
+                /*floats=*/0,
+                /*numbers=*/4 },
+              /*casts=*/2,
+              /*undecided=*/0 },
+            /*After propagation=*/
+            { { /*values=*/8,
+                /*uses=*/6 },
+              { /*pointers=*/4,
+                /*unsigned=*/7,
+                /*bools=*/0,
+                /*signed=*/7,
+                /*floats=*/0,
+                /*numbers=*/4 },
+              /*casts=*/0,
+              /*undecided=*/5 },
+            /*Final=*/
+            { { /*values=*/8,
+                /*uses=*/6 },
+              { /*pointers=*/4,
+                /*unsigned=*/7,
+                /*bools=*/0,
+                /*signed=*/2,
+                /*floats=*/0,
+                /*numbers=*/0 },
+              /*casts=*/1,
+              /*undecided=*/0 });
+
+  // Side propagation (with icmp)
+  checkInit(R"LLVM(
+    %0 = alloca i32, align 4
+    %1 = alloca i32, align 4
+    %2 = load i32, i32* %0, align 4
+    %3 = load i32, i32* %1, align 4
+    %4 = icmp eq i32 %2, %3
+    %5 = icmp sgt i32 %2, 2
+    %6 = icmp ugt i32 %3, 3
+    unreachable
+  )LLVM",
+            /*Init=*/
+            { { /*values=*/8,
+                /*uses=*/6 },
+              { /*pointers=*/4,
+                /*unsigned=*/1,
+                /*bools=*/3,
+                /*signed=*/1,
+                /*floats=*/0,
+                /*numbers=*/0 },
+              /*casts=*/2,
+              /*undecided=*/0 },
+            /*After propagation=*/
+            { { /*values=*/8,
+                /*uses=*/6 },
+              { /*pointers=*/4,
+                /*unsigned=*/5,
+                /*bools=*/3,
+                /*signed=*/5,
+                /*floats=*/0,
+                /*numbers=*/0 },
+              /*casts=*/0,
+              /*undecided=*/4 },
+            /*Final=*/
+            { { /*values=*/8,
+                /*uses=*/6 },
+              { /*pointers=*/4,
+                /*unsigned=*/5,
+                /*bools=*/3,
+                /*signed=*/1,
+                /*floats=*/0,
+                /*numbers=*/0 },
+              /*casts=*/1,
+              /*undecided=*/0 });
+
+  // Mul + ptr (backward)
+  checkInit(R"LLVM(
+    %0 = alloca i32, align 4
+    %1 = alloca i32, align 4
+    %2 = alloca i32, align 4
+    %3 = load i32, i32* %0, align 4
+    %4 = load i32, i32* %1, align 4
+    %5 = load i32, i32* %2, align 4
+    %6 = mul i32 %3, %4
+    %7 = add i32 %5, %6
+    %8 = inttoptr i32 %7 to i32*
+    store i32 10, i32* %8
+    unreachable
+  )LLVM",
+            /*Init=*/
+            { { /*values=*/11,
+                /*uses=*/9 },
+              { /*pointers=*/7,
+                /*unsigned=*/0,
+                /*bools=*/0,
+                /*signed=*/0,
+                /*floats=*/0,
+                /*numbers=*/3 },
+              /*casts=*/1,
+              /*undecided=*/0 },
+            /*After propagation=*/
+            { { /*values=*/11,
+                /*uses=*/9 },
+              { /*pointers=*/10,
+                /*unsigned=*/0,
+                /*bools=*/0,
+                /*signed=*/0,
+                /*floats=*/0,
+                /*numbers=*/3 },
+              /*casts=*/2,
+              /*undecided=*/0 },
+            /*Final=*/
+            { { /*values=*/11,
+                /*uses=*/9 },
+              { /*pointers=*/10,
+                /*unsigned=*/0,
+                /*bools=*/0,
+                /*signed=*/0,
+                /*floats=*/0,
+                /*numbers=*/0 },
+              /*casts=*/2,
+              /*undecided=*/0 });
+
+  // Mul + ptr (forward)
+  checkInit(R"LLVM(
+    %0 = alloca i32, align 4
+    %1 = alloca i32, align 4
+    %2 = alloca i32, align 4
+    %3 = load i32, i32* %0, align 4
+    %4 = load i32, i32* %1, align 4
+    %5 = load i32, i32* %2, align 4
+    %6 = mul i32 %3, %4
+    %7 = add i32 %5, %6
+    %8 = inttoptr i32 %5 to i32*
+    store i32 10, i32* %8
+    unreachable
+  )LLVM",
+            /*Init=*/
+            { { /*values=*/11,
+                /*uses=*/9 },
+              { /*pointers=*/7,
+                /*unsigned=*/0,
+                /*bools=*/0,
+                /*signed=*/0,
+                /*floats=*/0,
+                /*numbers=*/3 },
+              /*casts=*/1,
+              /*undecided=*/0 },
+            /*After propagation=*/
+            { { /*values=*/11,
+                /*uses=*/9 },
+              { /*pointers=*/12,
+                /*unsigned=*/0,
+                /*bools=*/0,
+                /*signed=*/0,
+                /*floats=*/0,
+                /*numbers=*/3 },
+              /*casts=*/1,
+              /*undecided=*/0 },
+            /*Final=*/
+            { { /*values=*/11,
+                /*uses=*/9 },
+              { /*pointers=*/12,
+                /*unsigned=*/0,
+                /*bools=*/0,
+                /*signed=*/0,
+                /*floats=*/0,
+                /*numbers=*/0 },
+              /*casts=*/1,
+              /*undecided=*/0 });
+
+  // And with bools
+  checkInit(R"LLVM(
+    %0 = alloca i32, align 4
+    %1 = alloca i32, align 4
+    %2 = load i32, i32* %0, align 4
+    %3 = load i32, i32* %1, align 4
+    %4 = icmp eq i32 %2, 2
+    %5 = icmp eq i32 %3, 3
+    %6 = and i1 %5, %4
+    unreachable
+  )LLVM",
+            /*Init=*/
+            { { /*values=*/8,
+                /*uses=*/6 },
+              { /*pointers=*/4,
+                /*unsigned=*/0,
+                /*bools=*/2,
+                /*signed=*/0,
+                /*floats=*/0,
+                /*numbers=*/0 },
+              /*casts=*/2,
+              /*undecided=*/0 },
+            /*After propagation=*/
+            { { /*values=*/8,
+                /*uses=*/6 },
+              { /*pointers=*/4,
+                /*unsigned=*/0,
+                /*bools=*/5,
+                /*signed=*/0,
+                /*floats=*/0,
+                /*numbers=*/0 },
+              /*casts=*/0,
+              /*undecided=*/0 },
+            /*Final=*/
+            { { /*values=*/8,
+                /*uses=*/6 },
+              { /*pointers=*/4,
+                /*unsigned=*/0,
+                /*bools=*/5,
+                /*signed=*/0,
+                /*floats=*/0,
+                /*numbers=*/0 },
+              /*casts=*/0,
+              /*undecided=*/0 });
+
+  // Shift ptr
+  checkInit(R"LLVM(
+    %0 = alloca i32, align 4
+    %1 = alloca i32, align 4
+    %2 = load i32, i32* %0, align 4
+    %3 = load i32, i32* %1, align 4
+    %4 = inttoptr i32 %2 to i32*
+    store i32 10, i32* %4
+    %5 = shl i32 %2, %3
+    unreachable
+  )LLVM",
+            /*Init=*/
+            { { /*values=*/8,
+                /*uses=*/6 },
+              { /*pointers=*/5,
+                /*unsigned=*/1,
+                /*bools=*/0,
+                /*signed=*/0,
+                /*floats=*/0,
+                /*numbers=*/0 },
+              /*casts=*/2,
+              /*undecided=*/0 },
+            /*After propagation=*/
+            { { /*values=*/8,
+                /*uses=*/6 },
+              { /*pointers=*/8,
+                /*unsigned=*/2,
+                /*bools=*/0,
+                /*signed=*/0,
+                /*floats=*/0,
+                /*numbers=*/0 },
+              /*casts=*/1,
+              /*undecided=*/0 },
+            /*Final=*/
+            { { /*values=*/8,
+                /*uses=*/6 },
+              { /*pointers=*/8,
+                /*unsigned=*/2,
+                /*bools=*/0,
+                /*signed=*/0,
+                /*floats=*/0,
+                /*numbers=*/0 },
+              /*casts=*/1,
+              /*undecided=*/0 });
+
+  // Set last bit to 0
+  checkInit(R"LLVM(
+    %0 = alloca i32, align 4
+    %1 = load i32, i32* %0, align 4
+    %2 = inttoptr i32 %1 to i32*
+    store i32 10, i32* %2
+    %3 = and i32 %1, 254
+    unreachable
+  )LLVM",
+            /*Init=*/
+            { { /*values=*/6,
+                /*uses=*/4 },
+              { /*pointers=*/3,
+                /*unsigned=*/0,
+                /*bools=*/0,
+                /*signed=*/0,
+                /*floats=*/0,
+                /*numbers=*/0 },
+              /*casts=*/1,
+              /*undecided=*/0 },
+            /*Final=*/
+            { { /*values=*/6,
+                /*uses=*/4 },
+              { /*pointers=*/7,
+                /*unsigned=*/0,
+                /*bools=*/0,
+                /*signed=*/0,
+                /*floats=*/0,
+                /*numbers=*/0 },
+              /*casts=*/1,
+              /*undecided=*/0 },
+            /*After propagation=*/
+            { { /*values=*/6,
+                /*uses=*/4 },
+              { /*pointers=*/7,
+                /*unsigned=*/0,
+                /*bools=*/0,
+                /*signed=*/0,
+                /*floats=*/0,
+                /*numbers=*/0 },
+              /*casts=*/1,
+              /*undecided=*/0 });
+}
+
+BOOST_AUTO_TEST_CASE(TestMajorityVoting) {
+  const auto AddNode = [](TypeFlowGraph &G, unsigned Color) {
+    UseOrValue DummyContent;
+    ColorSet DecidedColor(Color);
+    NodeColorProperty InitColors(DecidedColor, DecidedColor);
+
+    return G.addNode(DummyContent, InitColors);
+  };
+
+  TypeFlowGraph G;
+  TypeFlowNode *Undecided1 = AddNode(G, (POINTERNESS | UNSIGNEDNESS));
+  TypeFlowNode *Undecided2 = AddNode(G, (POINTERNESS | UNSIGNEDNESS));
+  Undecided1->addSuccessor(Undecided2);
+
+  TypeFlowNode *Decided1 = AddNode(G, POINTERNESS);
+  TypeFlowNode *Decided2 = AddNode(G, POINTERNESS);
+  TypeFlowNode *Decided3 = AddNode(G, UNSIGNEDNESS);
+  TypeFlowNode *Decided4 = AddNode(G, SIGNEDNESS);
+  Undecided1->addSuccessor(Decided1);
+  Undecided1->addSuccessor(Decided2);
+  Undecided1->addSuccessor(Decided3);
+  Undecided1->addSuccessor(Decided4);
+
+  makeBidirectional(G);
+  applyMajorityVoting(G);
+
+  revng_check(Undecided1->Candidates == (POINTERNESS | UNSIGNEDNESS));
+  revng_check(Undecided2->Candidates == (POINTERNESS | UNSIGNEDNESS));
+
+  TypeFlowNode *Decided5 = AddNode(G, POINTERNESS);
+  Undecided1->addSuccessor(Decided5);
+
+  makeBidirectional(G);
+  applyMajorityVoting(G);
+
+  revng_check(Undecided1->Candidates == POINTERNESS);
+  revng_check(Undecided2->Candidates == POINTERNESS);
+}