diff --git a/source/fuzz/equivalence_relation.h b/source/fuzz/equivalence_relation.h
index 7bb8b66..6d0b63e 100644
--- a/source/fuzz/equivalence_relation.h
+++ b/source/fuzz/equivalence_relation.h
@@ -68,17 +68,14 @@
 template <typename T, typename PointerHashT, typename PointerEqualsT>
 class EquivalenceRelation {
  public:
-  // Merges the equivalence classes associated with |value1| and |value2|.
-  // If any of these values was not previously in the equivalence relation, it
-  // is added to the pool of values known to be in the relation.
+  // Requires that |value1| and |value2| are already registered in the
+  // equivalence relation.  Merges the equivalence classes associated with
+  // |value1| and |value2|.
   void MakeEquivalent(const T& value1, const T& value2) {
-    // Register each value if necessary.
-    for (auto value : {value1, value2}) {
-      if (!Exists(value)) {
-        // Register the value in the equivalence relation.
-        Register(value);
-      }
-    }
+    assert(Exists(value1) &&
+           "Precondition: value1 must already be registered.");
+    assert(Exists(value2) &&
+           "Precondition: value2 must already be registered.");
 
     // Look up canonical pointers to each of the values in the value pool.
     const T* value1_ptr = *value_set_.find(&value1);
@@ -105,7 +102,7 @@
   // Requires that |value| is not known to the equivalence relation. Registers
   // it in its own equivalence class and returns a pointer to the equivalence
   // class representative.
-  const T* Register(T& value) {
+  const T* Register(const T& value) {
     assert(!Exists(value));
 
     // This relies on T having a copy constructor.
diff --git a/source/fuzz/fact_manager.cpp b/source/fuzz/fact_manager.cpp
index 31d3b94..7901341 100644
--- a/source/fuzz/fact_manager.cpp
+++ b/source/fuzz/fact_manager.cpp
@@ -445,6 +445,15 @@
   // compute the closure only when a data synonym fact is *queried*.
   void ComputeClosureOfFacts(opt::IRContext* context) const;
 
+  // Records the fact that |dd1| and |dd2| are equivalent, and merges the sets
+  // of equations that are known about them.
+  //
+  // This is a const method, despite the fact that it mutates the (mutable)
+  // set of facts about data descriptors because it is invoked in a lazy fashion
+  // when querying facts.
+  void MakeEquivalent(const protobufs::DataDescriptor& dd1,
+                      const protobufs::DataDescriptor& dd2) const;
+
   // Returns true if and only if |dd1| and |dd2| are valid data descriptors
   // whose associated data have the same type (modulo integer signedness).
   bool DataDescriptorsAreWellFormedAndComparable(
@@ -452,10 +461,11 @@
       const protobufs::DataDescriptor& dd2) const;
 
   // Requires that |lhs_dd| and every element of |rhs_dds| is present in the
-  // |synonymous_| equivalence relation and is its own representative.  Records
-  // the fact that the equation "|lhs_dd| |opcode| |rhs_dds|" holds, and adds
-  // any corollaries, in the form of data synonym or equation facts, that
-  // follow from this and other known facts.
+  // |synonymous_| equivalence relation, but is not necessarily its own
+  // representative.  Records the fact that the equation
+  // "|lhs_dd| |opcode| |rhs_dds_non_canonical|" holds, and adds any
+  // corollaries, in the form of data synonym or equation facts, that follow
+  // from this and other known facts.
   void AddEquationFactRecursive(
       const protobufs::DataDescriptor& lhs_dd, SpvOp opcode,
       const std::vector<const protobufs::DataDescriptor*>& rhs_dds,
@@ -493,7 +503,12 @@
   // All data descriptors occurring in equations are required to be present in
   // the |synonymous_| equivalence relation, and to be their own representatives
   // in that relation.
-  std::unordered_map<
+  //
+  // It is mutable because a closure computation can be triggered from a const
+  // method, and when a closure computation detects that two data descriptors
+  // are equivalent it is necessary to merge the equation facts for those data
+  // descriptors.
+  mutable std::unordered_map<
       const protobufs::DataDescriptor*,
       std::unordered_set<Operation, OperationHash, OperationEquals>>
       id_equations_;
@@ -510,12 +525,10 @@
     const protobufs::FactIdEquation& fact, opt::IRContext* context) {
   protobufs::DataDescriptor lhs_dd = MakeDataDescriptor(fact.lhs_id(), {});
 
-  // Register the LHS in the equivalence relation if needed, and get a pointer
-  // to its representative.
+  // Register the LHS in the equivalence relation if needed.
   if (!synonymous_.Exists(lhs_dd)) {
     synonymous_.Register(lhs_dd);
   }
-  const protobufs::DataDescriptor* lhs_dd_ptr = synonymous_.Find(&lhs_dd);
 
   // Get equivalence class representatives for all ids used on the RHS of the
   // equation.
@@ -529,10 +542,9 @@
     }
     rhs_dd_ptrs.push_back(synonymous_.Find(&rhs_dd));
   }
-  // We now have the equation in a form where it refers exclusively to
-  // equivalence class representatives.  Add it to our set of facts and work
-  // out any follow-on facts.
-  AddEquationFactRecursive(*lhs_dd_ptr, static_cast<SpvOp>(fact.opcode()),
+
+  // Now add the fact.
+  AddEquationFactRecursive(lhs_dd, static_cast<SpvOp>(fact.opcode()),
                            rhs_dd_ptrs, context);
 }
 
@@ -540,27 +552,27 @@
     const protobufs::DataDescriptor& lhs_dd, SpvOp opcode,
     const std::vector<const protobufs::DataDescriptor*>& rhs_dds,
     opt::IRContext* context) {
-  // Precondition: all data descriptors referenced in this equation must be
-  // equivalence class representatives - i.e. the equation must be in canonical
-  // form.
-  assert(synonymous_.Exists(lhs_dd));
-  assert(synonymous_.Find(&lhs_dd) == &lhs_dd);
+  assert(synonymous_.Exists(lhs_dd) &&
+         "The LHS must be known to the equivalence relation.");
   for (auto rhs_dd : rhs_dds) {
-    (void)(rhs_dd);  // Keep compilers happy in release mode.
-    assert(synonymous_.Exists(*rhs_dd));
-    assert(synonymous_.Find(rhs_dd) == rhs_dd);
+    // Keep release compilers happy.
+    (void)(rhs_dd);
+    assert(synonymous_.Exists(*rhs_dd) &&
+           "The RHS operands must be known to the equivalence relation.");
   }
 
-  if (id_equations_.count(&lhs_dd) == 0) {
+  auto lhs_dd_representative = synonymous_.Find(&lhs_dd);
+
+  if (id_equations_.count(lhs_dd_representative) == 0) {
     // We have not seen an equation with this LHS before, so associate the LHS
     // with an initially empty set.
     id_equations_.insert(
-        {&lhs_dd,
+        {lhs_dd_representative,
          std::unordered_set<Operation, OperationHash, OperationEquals>()});
   }
 
   {
-    auto existing_equations = id_equations_.find(&lhs_dd);
+    auto existing_equations = id_equations_.find(lhs_dd_representative);
     assert(existing_equations != id_equations_.end() &&
            "A set of operations should be present, even if empty.");
 
@@ -584,13 +596,15 @@
           for (auto equation : existing_first_operand_equations->second) {
             if (equation.opcode == SpvOpISub) {
               // Equation form: "a = (d - e) + c"
-              if (equation.operands[1] == rhs_dds[1]) {
+              if (synonymous_.IsEquivalent(*equation.operands[1],
+                                           *rhs_dds[1])) {
                 // Equation form: "a = (d - c) + c"
                 // We can thus infer "a = d"
                 AddDataSynonymFactRecursive(lhs_dd, *equation.operands[0],
                                             context);
               }
-              if (equation.operands[0] == rhs_dds[1]) {
+              if (synonymous_.IsEquivalent(*equation.operands[0],
+                                           *rhs_dds[1])) {
                 // Equation form: "a = (c - e) + c"
                 // We can thus infer "a = -e"
                 AddEquationFactRecursive(lhs_dd, SpvOpSNegate,
@@ -606,7 +620,8 @@
           for (auto equation : existing_second_operand_equations->second) {
             if (equation.opcode == SpvOpISub) {
               // Equation form: "a = b + (d - e)"
-              if (equation.operands[1] == rhs_dds[0]) {
+              if (synonymous_.IsEquivalent(*equation.operands[1],
+                                           *rhs_dds[0])) {
                 // Equation form: "a = b + (d - b)"
                 // We can thus infer "a = d"
                 AddDataSynonymFactRecursive(lhs_dd, *equation.operands[0],
@@ -626,13 +641,15 @@
           for (auto equation : existing_first_operand_equations->second) {
             if (equation.opcode == SpvOpIAdd) {
               // Equation form: "a = (d + e) - c"
-              if (equation.operands[0] == rhs_dds[1]) {
+              if (synonymous_.IsEquivalent(*equation.operands[0],
+                                           *rhs_dds[1])) {
                 // Equation form: "a = (c + e) - c"
                 // We can thus infer "a = e"
                 AddDataSynonymFactRecursive(lhs_dd, *equation.operands[1],
                                             context);
               }
-              if (equation.operands[1] == rhs_dds[1]) {
+              if (synonymous_.IsEquivalent(*equation.operands[1],
+                                           *rhs_dds[1])) {
                 // Equation form: "a = (d + c) - c"
                 // We can thus infer "a = d"
                 AddDataSynonymFactRecursive(lhs_dd, *equation.operands[0],
@@ -642,7 +659,8 @@
 
             if (equation.opcode == SpvOpISub) {
               // Equation form: "a = (d - e) - c"
-              if (equation.operands[0] == rhs_dds[1]) {
+              if (synonymous_.IsEquivalent(*equation.operands[0],
+                                           *rhs_dds[1])) {
                 // Equation form: "a = (c - e) - c"
                 // We can thus infer "a = -e"
                 AddEquationFactRecursive(lhs_dd, SpvOpSNegate,
@@ -659,13 +677,15 @@
           for (auto equation : existing_second_operand_equations->second) {
             if (equation.opcode == SpvOpIAdd) {
               // Equation form: "a = b - (d + e)"
-              if (equation.operands[0] == rhs_dds[0]) {
+              if (synonymous_.IsEquivalent(*equation.operands[0],
+                                           *rhs_dds[0])) {
                 // Equation form: "a = b - (b + e)"
                 // We can thus infer "a = -e"
                 AddEquationFactRecursive(lhs_dd, SpvOpSNegate,
                                          {equation.operands[1]}, context);
               }
-              if (equation.operands[1] == rhs_dds[0]) {
+              if (synonymous_.IsEquivalent(*equation.operands[1],
+                                           *rhs_dds[0])) {
                 // Equation form: "a = b - (d + b)"
                 // We can thus infer "a = -d"
                 AddEquationFactRecursive(lhs_dd, SpvOpSNegate,
@@ -674,7 +694,8 @@
             }
             if (equation.opcode == SpvOpISub) {
               // Equation form: "a = b - (d - e)"
-              if (equation.operands[0] == rhs_dds[0]) {
+              if (synonymous_.IsEquivalent(*equation.operands[0],
+                                           *rhs_dds[0])) {
                 // Equation form: "a = b - (b - e)"
                 // We can thus infer "a = e"
                 AddDataSynonymFactRecursive(lhs_dd, *equation.operands[1],
@@ -712,12 +733,7 @@
   assert(DataDescriptorsAreWellFormedAndComparable(context, dd1, dd2));
 
   // Record that the data descriptors provided in the fact are equivalent.
-  synonymous_.MakeEquivalent(dd1, dd2);
-  // As we have updated the equivalence relation, we might be able to deduce
-  // more facts by performing a closure computation, so we record that such a
-  // computation is required; it will be performed next time a method answering
-  // a data synonym fact-related question is invoked.
-  closure_computation_required_ = true;
+  MakeEquivalent(dd1, dd2);
 
   // We now check whether this is a synonym about composite objects.  If it is,
   // we can recursively add synonym facts about their associated sub-components.
@@ -1029,10 +1045,7 @@
             // synonymous.
             assert(DataDescriptorsAreWellFormedAndComparable(
                 context, dd1_prefix, dd2_prefix));
-            synonymous_.MakeEquivalent(dd1_prefix, dd2_prefix);
-            // As we have added a new synonym fact, we might benefit from doing
-            // another pass over the equivalence relation.
-            closure_computation_required_ = true;
+            MakeEquivalent(dd1_prefix, dd2_prefix);
             // Now that we know this pair of data descriptors are synonymous,
             // there is no point recording how close they are to being
             // synonymous.
@@ -1044,6 +1057,84 @@
   }
 }
 
+void FactManager::DataSynonymAndIdEquationFacts::MakeEquivalent(
+    const protobufs::DataDescriptor& dd1,
+    const protobufs::DataDescriptor& dd2) const {
+  // Register the data descriptors if they are not already known to the
+  // equivalence relation.
+  for (const auto& dd : {dd1, dd2}) {
+    if (!synonymous_.Exists(dd)) {
+      synonymous_.Register(dd);
+    }
+  }
+
+  if (synonymous_.IsEquivalent(dd1, dd2)) {
+    // The data descriptors are already known to be equivalent, so there is
+    // nothing to do.
+    return;
+  }
+
+  // We must make the data descriptors equivalent, and also make sure any
+  // equation facts known about their representatives are merged.
+
+  // Record the original equivalence class representatives of the data
+  // descriptors.
+  auto dd1_original_representative = synonymous_.Find(&dd1);
+  auto dd2_original_representative = synonymous_.Find(&dd2);
+
+  // Make the data descriptors equivalent.
+  synonymous_.MakeEquivalent(dd1, dd2);
+  // As we have updated the equivalence relation, we might be able to deduce
+  // more facts by performing a closure computation, so we record that such a
+  // computation is required.
+  closure_computation_required_ = true;
+
+  // At this point, exactly one of |dd1_original_representative| and
+  // |dd2_original_representative| will be the representative of the combined
+  // equivalence class.  We work out which one of them is still the class
+  // representative and which one is no longer the class representative.
+
+  auto still_representative = synonymous_.Find(dd1_original_representative) ==
+                                      dd1_original_representative
+                                  ? dd1_original_representative
+                                  : dd2_original_representative;
+  auto no_longer_representative =
+      still_representative == dd1_original_representative
+          ? dd2_original_representative
+          : dd1_original_representative;
+
+  assert(no_longer_representative != still_representative &&
+         "The current and former representatives cannot be the same.");
+
+  // We now need to add all equations about |no_longer_representative| to the
+  // set of equations known about |still_representative|.
+
+  // Get the equations associated with |no_longer_representative|.
+  auto no_longer_representative_id_equations =
+      id_equations_.find(no_longer_representative);
+  if (no_longer_representative_id_equations != id_equations_.end()) {
+    // There are some equations to transfer.  There might not yet be any
+    // equations about |still_representative|; create an empty set of equations
+    // if this is the case.
+    if (!id_equations_.count(still_representative)) {
+      id_equations_.insert(
+          {still_representative,
+           std::unordered_set<Operation, OperationHash, OperationEquals>()});
+    }
+    auto still_representative_id_equations =
+        id_equations_.find(still_representative);
+    assert(still_representative_id_equations != id_equations_.end() &&
+           "At this point there must be a set of equations.");
+    // Add all the equations known about |no_longer_representative| to the set
+    // of equations known about |still_representative|.
+    still_representative_id_equations->second.insert(
+        no_longer_representative_id_equations->second.begin(),
+        no_longer_representative_id_equations->second.end());
+  }
+  // Delete the no longer-relevant equations about |no_longer_representative|.
+  id_equations_.erase(no_longer_representative);
+}
+
 bool FactManager::DataSynonymAndIdEquationFacts::
     DataDescriptorsAreWellFormedAndComparable(
         opt::IRContext* context, const protobufs::DataDescriptor& dd1,
diff --git a/test/fuzz/equivalence_relation_test.cpp b/test/fuzz/equivalence_relation_test.cpp
index 3f2ea58..280aa3a 100644
--- a/test/fuzz/equivalence_relation_test.cpp
+++ b/test/fuzz/equivalence_relation_test.cpp
@@ -47,6 +47,10 @@
   EquivalenceRelation<uint32_t, UInt32Hash, UInt32Equals> relation;
   ASSERT_TRUE(relation.GetAllKnownValues().empty());
 
+  for (uint32_t element = 0; element < 100; element++) {
+    relation.Register(element);
+  }
+
   for (uint32_t element = 2; element < 80; element += 2) {
     relation.MakeEquivalent(0, element);
     relation.MakeEquivalent(element - 1, element + 1);
@@ -123,6 +127,11 @@
   EquivalenceRelation<uint32_t, UInt32Hash, UInt32Equals> relation2;
 
   for (uint32_t i = 0; i < 1000; ++i) {
+    relation1.Register(i);
+    relation2.Register(i);
+  }
+
+  for (uint32_t i = 0; i < 1000; ++i) {
     if (i >= 10) {
       relation1.MakeEquivalent(i, i - 10);
       relation2.MakeEquivalent(i, i - 10);
diff --git a/test/fuzz/fact_manager_test.cpp b/test/fuzz/fact_manager_test.cpp
index 2c79f12..625eb72 100644
--- a/test/fuzz/fact_manager_test.cpp
+++ b/test/fuzz/fact_manager_test.cpp
@@ -1373,6 +1373,78 @@
       MakeDataDescriptor(23, {}), MakeDataDescriptor(16, {}), context.get()));
 }
 
+TEST(FactManagerTest, EquationAndEquivalenceFacts) {
+  std::string shader = R"(
+               OpCapability Shader
+          %1 = OpExtInstImport "GLSL.std.450"
+               OpMemoryModel Logical GLSL450
+               OpEntryPoint Fragment %12 "main"
+               OpExecutionMode %12 OriginUpperLeft
+               OpSource ESSL 310
+          %2 = OpTypeVoid
+          %3 = OpTypeFunction %2
+          %6 = OpTypeInt 32 1
+         %15 = OpConstant %6 24
+         %16 = OpConstant %6 37
+         %12 = OpFunction %2 None %3
+         %13 = OpLabel
+         %14 = OpISub %6 %15 %16
+        %114 = OpCopyObject %6 %14
+         %17 = OpIAdd %6 %114 %16 ; ==> synonymous(%17, %15)
+         %18 = OpIAdd %6 %16 %114 ; ==> synonymous(%17, %18, %15)
+         %19 = OpISub %6 %114 %15
+        %119 = OpCopyObject %6 %19
+         %20 = OpSNegate %6 %119 ; ==> synonymous(%20, %16)
+         %21 = OpISub %6 %14 %19 ; ==> synonymous(%21, %15)
+         %22 = OpISub %6 %14 %18
+        %220 = OpCopyObject %6 %22
+         %23 = OpSNegate %6 %220 ; ==> synonymous(%23, %16)
+               OpReturn
+               OpFunctionEnd
+  )";
+
+  const auto env = SPV_ENV_UNIVERSAL_1_3;
+  const auto consumer = nullptr;
+  const auto context = BuildModule(env, consumer, shader, kFuzzAssembleOption);
+  ASSERT_TRUE(IsValid(env, context.get()));
+
+  FactManager fact_manager;
+
+  fact_manager.AddFactIdEquation(14, SpvOpISub, {15, 16}, context.get());
+  fact_manager.AddFactDataSynonym(MakeDataDescriptor(114, {}),
+                                  MakeDataDescriptor(14, {}), context.get());
+  fact_manager.AddFactIdEquation(17, SpvOpIAdd, {114, 16}, context.get());
+
+  ASSERT_TRUE(fact_manager.IsSynonymous(
+      MakeDataDescriptor(17, {}), MakeDataDescriptor(15, {}), context.get()));
+
+  fact_manager.AddFactIdEquation(18, SpvOpIAdd, {16, 114}, context.get());
+
+  ASSERT_TRUE(fact_manager.IsSynonymous(
+      MakeDataDescriptor(18, {}), MakeDataDescriptor(15, {}), context.get()));
+  ASSERT_TRUE(fact_manager.IsSynonymous(
+      MakeDataDescriptor(17, {}), MakeDataDescriptor(18, {}), context.get()));
+
+  fact_manager.AddFactIdEquation(19, SpvOpISub, {14, 15}, context.get());
+  fact_manager.AddFactDataSynonym(MakeDataDescriptor(119, {}),
+                                  MakeDataDescriptor(19, {}), context.get());
+  fact_manager.AddFactIdEquation(20, SpvOpSNegate, {119}, context.get());
+
+  ASSERT_TRUE(fact_manager.IsSynonymous(
+      MakeDataDescriptor(20, {}), MakeDataDescriptor(16, {}), context.get()));
+
+  fact_manager.AddFactIdEquation(21, SpvOpISub, {14, 19}, context.get());
+  ASSERT_TRUE(fact_manager.IsSynonymous(
+      MakeDataDescriptor(21, {}), MakeDataDescriptor(15, {}), context.get()));
+
+  fact_manager.AddFactIdEquation(22, SpvOpISub, {14, 18}, context.get());
+  fact_manager.AddFactDataSynonym(MakeDataDescriptor(22, {}),
+                                  MakeDataDescriptor(220, {}), context.get());
+  fact_manager.AddFactIdEquation(23, SpvOpSNegate, {220}, context.get());
+  ASSERT_TRUE(fact_manager.IsSynonymous(
+      MakeDataDescriptor(23, {}), MakeDataDescriptor(16, {}), context.get()));
+}
+
 }  // namespace
 }  // namespace fuzz
 }  // namespace spvtools
diff --git a/test/fuzz/transformation_equation_instruction_test.cpp b/test/fuzz/transformation_equation_instruction_test.cpp
index be9024e..3155b18 100644
--- a/test/fuzz/transformation_equation_instruction_test.cpp
+++ b/test/fuzz/transformation_equation_instruction_test.cpp
@@ -486,6 +486,146 @@
   ASSERT_TRUE(IsEqual(env, after_transformation, context.get()));
 }
 
+TEST(TransformationEquationInstructionTest, Miscellaneous1) {
+  std::string shader = R"(
+               OpCapability Shader
+          %1 = OpExtInstImport "GLSL.std.450"
+               OpMemoryModel Logical GLSL450
+               OpEntryPoint Fragment %12 "main"
+               OpExecutionMode %12 OriginUpperLeft
+               OpSource ESSL 310
+          %2 = OpTypeVoid
+          %3 = OpTypeFunction %2
+          %6 = OpTypeInt 32 1
+        %113 = OpConstant %6 24
+         %12 = OpFunction %2 None %3
+         %13 = OpLabel
+               OpReturn
+               OpFunctionEnd
+  )";
+
+  const auto env = SPV_ENV_UNIVERSAL_1_3;
+  const auto consumer = nullptr;
+  const auto context = BuildModule(env, consumer, shader, kFuzzAssembleOption);
+  ASSERT_TRUE(IsValid(env, context.get()));
+
+  FactManager fact_manager;
+  spvtools::ValidatorOptions validator_options;
+  TransformationContext transformation_context(&fact_manager,
+                                               validator_options);
+
+  protobufs::InstructionDescriptor return_instruction =
+      MakeInstructionDescriptor(13, SpvOpReturn, 0);
+
+  auto transformation1 = TransformationEquationInstruction(
+      522, SpvOpISub, {113, 113}, return_instruction);
+  ASSERT_TRUE(
+      transformation1.IsApplicable(context.get(), transformation_context));
+  transformation1.Apply(context.get(), &transformation_context);
+  ASSERT_TRUE(IsValid(env, context.get()));
+
+  auto transformation2 = TransformationEquationInstruction(
+      570, SpvOpIAdd, {522, 113}, return_instruction);
+  ASSERT_TRUE(
+      transformation2.IsApplicable(context.get(), transformation_context));
+  transformation2.Apply(context.get(), &transformation_context);
+  ASSERT_TRUE(IsValid(env, context.get()));
+
+  std::string after_transformation = R"(
+               OpCapability Shader
+          %1 = OpExtInstImport "GLSL.std.450"
+               OpMemoryModel Logical GLSL450
+               OpEntryPoint Fragment %12 "main"
+               OpExecutionMode %12 OriginUpperLeft
+               OpSource ESSL 310
+          %2 = OpTypeVoid
+          %3 = OpTypeFunction %2
+          %6 = OpTypeInt 32 1
+        %113 = OpConstant %6 24
+         %12 = OpFunction %2 None %3
+         %13 = OpLabel
+        %522 = OpISub %6 %113 %113
+        %570 = OpIAdd %6 %522 %113
+               OpReturn
+               OpFunctionEnd
+  )";
+
+  ASSERT_TRUE(transformation_context.GetFactManager()->IsSynonymous(
+      MakeDataDescriptor(570, {}), MakeDataDescriptor(113, {}), context.get()));
+
+  ASSERT_TRUE(IsEqual(env, after_transformation, context.get()));
+}
+
+TEST(TransformationEquationInstructionTest, Miscellaneous2) {
+  std::string shader = R"(
+               OpCapability Shader
+          %1 = OpExtInstImport "GLSL.std.450"
+               OpMemoryModel Logical GLSL450
+               OpEntryPoint Fragment %12 "main"
+               OpExecutionMode %12 OriginUpperLeft
+               OpSource ESSL 310
+          %2 = OpTypeVoid
+          %3 = OpTypeFunction %2
+          %6 = OpTypeInt 32 1
+        %113 = OpConstant %6 24
+         %12 = OpFunction %2 None %3
+         %13 = OpLabel
+               OpReturn
+               OpFunctionEnd
+  )";
+
+  const auto env = SPV_ENV_UNIVERSAL_1_3;
+  const auto consumer = nullptr;
+  const auto context = BuildModule(env, consumer, shader, kFuzzAssembleOption);
+  ASSERT_TRUE(IsValid(env, context.get()));
+
+  FactManager fact_manager;
+  spvtools::ValidatorOptions validator_options;
+  TransformationContext transformation_context(&fact_manager,
+                                               validator_options);
+
+  protobufs::InstructionDescriptor return_instruction =
+      MakeInstructionDescriptor(13, SpvOpReturn, 0);
+
+  auto transformation1 = TransformationEquationInstruction(
+      522, SpvOpISub, {113, 113}, return_instruction);
+  ASSERT_TRUE(
+      transformation1.IsApplicable(context.get(), transformation_context));
+  transformation1.Apply(context.get(), &transformation_context);
+  ASSERT_TRUE(IsValid(env, context.get()));
+
+  auto transformation2 = TransformationEquationInstruction(
+      570, SpvOpIAdd, {522, 113}, return_instruction);
+  ASSERT_TRUE(
+      transformation2.IsApplicable(context.get(), transformation_context));
+  transformation2.Apply(context.get(), &transformation_context);
+  ASSERT_TRUE(IsValid(env, context.get()));
+
+  std::string after_transformation = R"(
+               OpCapability Shader
+          %1 = OpExtInstImport "GLSL.std.450"
+               OpMemoryModel Logical GLSL450
+               OpEntryPoint Fragment %12 "main"
+               OpExecutionMode %12 OriginUpperLeft
+               OpSource ESSL 310
+          %2 = OpTypeVoid
+          %3 = OpTypeFunction %2
+          %6 = OpTypeInt 32 1
+        %113 = OpConstant %6 24
+         %12 = OpFunction %2 None %3
+         %13 = OpLabel
+        %522 = OpISub %6 %113 %113
+        %570 = OpIAdd %6 %522 %113
+               OpReturn
+               OpFunctionEnd
+  )";
+
+  ASSERT_TRUE(transformation_context.GetFactManager()->IsSynonymous(
+      MakeDataDescriptor(570, {}), MakeDataDescriptor(113, {}), context.get()));
+
+  ASSERT_TRUE(IsEqual(env, after_transformation, context.get()));
+}
+
 }  // namespace
 }  // namespace fuzz
 }  // namespace spvtools