diff --git a/clang/test/Analysis/exploded-graph-rewriter/checker_messages.dot b/clang/test/Analysis/exploded-graph-rewriter/checker_messages.dot
--- a/clang/test/Analysis/exploded-graph-rewriter/checker_messages.dot
+++ b/clang/test/Analysis/exploded-graph-rewriter/checker_messages.dot
@@ -22,6 +22,8 @@
       "program_state": {
         "store": null,
         "constraints": null,
+        "equivalence_classes": null,
+        "disequality_info": null,
         "dynamic_types": null,
         "constructing_objects": null,
         "environment": null,
diff --git a/clang/test/Analysis/exploded-graph-rewriter/checker_messages_diff.dot b/clang/test/Analysis/exploded-graph-rewriter/checker_messages_diff.dot
--- a/clang/test/Analysis/exploded-graph-rewriter/checker_messages_diff.dot
+++ b/clang/test/Analysis/exploded-graph-rewriter/checker_messages_diff.dot
@@ -15,6 +15,10 @@
         "environment": null,
         "store": null,
         "constraints": null,
+        "equivalence_classes": null,
+        "disequality_info": null,
+        "equivalence_classes": null,
+        "disequality_info": null,
         "dynamic_types": null,
         "constructing_objects": null,
         "checker_messages": [
@@ -73,6 +77,8 @@
         "environment": null,
         "store": null,
         "constraints": null,
+        "equivalence_classes": null,
+        "disequality_info": null,
         "dynamic_types": null,
         "constructing_objects": null,
         "checker_messages": [
diff --git a/clang/test/Analysis/exploded-graph-rewriter/constraints.dot b/clang/test/Analysis/exploded-graph-rewriter/constraints.dot
--- a/clang/test/Analysis/exploded-graph-rewriter/constraints.dot
+++ b/clang/test/Analysis/exploded-graph-rewriter/constraints.dot
@@ -27,7 +27,9 @@
         "checker_messages": null,
         "constraints": [
           { "symbol": "reg_$0<x>", "range": "{ [0, 0] }" }
-        ]
+        ],
+        "equivalence_classes": null,
+        "disequality_info": null
       }
     }
 \l}"];
diff --git a/clang/test/Analysis/exploded-graph-rewriter/constraints_diff.dot b/clang/test/Analysis/exploded-graph-rewriter/constraints_diff.dot
--- a/clang/test/Analysis/exploded-graph-rewriter/constraints_diff.dot
+++ b/clang/test/Analysis/exploded-graph-rewriter/constraints_diff.dot
@@ -20,7 +20,9 @@
         "checker_messages": null,
         "constraints": [
           { "symbol": "reg_$0<x>", "range": "{ [0, 10] }" }
-        ]
+        ],
+        "equivalence_classes": null,
+        "disequality_info": null
       }
     }
 \l}"];
@@ -58,7 +60,9 @@
         "checker_messages": null,
         "constraints": [
           { "symbol": "reg_$0<x>", "range": "{ [0, 5] }" }
-        ]
+        ],
+        "equivalence_classes": null,
+        "disequality_info": null
       }
     }
 \l}"];
@@ -81,6 +85,8 @@
         "store": null,
         "environment": null,
         "constraints": null,
+        "equivalence_classes": null,
+        "disequality_info": null,
         "dynamic_types": null,
         "constructing_objects": null,
         "checker_messages": null
diff --git a/clang/test/Analysis/exploded-graph-rewriter/disequality_info.dot b/clang/test/Analysis/exploded-graph-rewriter/disequality_info.dot
new file mode 100644
--- /dev/null
+++ b/clang/test/Analysis/exploded-graph-rewriter/disequality_info.dot
@@ -0,0 +1,83 @@
+// RUN: %exploded_graph_rewriter %s | FileCheck %s
+
+// CHECK:        <tr>
+// CHECK-SAME:      <td align="left"><b>Disequality Info: </b></td>
+// CHECK-SAME:   </tr>
+// CHECK-SAME:   <tr>
+// CHECK-SAME:      <td align="left">
+// CHECK-SAME:         <table border="1">
+// CHECK-SAME:            <tr>
+// CHECK-SAME:               <td></td>
+// CHECK-SAME:               <td align="left">
+// CHECK-SAME:                  reg_$0<int a>
+// CHECK-SAME:               </td>
+// CHECK-SAME:               <td align="left">
+// CHECK-SAME:                  <table border='1'>
+// CHECK-SAME:                     <tr>
+// CHECK-SAME:                        <td>
+// CHECK-SAME:                           (reg_$1<int b>) - 2
+// CHECK-SAME:                        </td>
+// CHECK-SAME:                     </tr>
+// CHECK-SAME:                     <tr>
+// CHECK-SAME:                        <td>
+// CHECK-SAME:                           reg_$2<int c>
+// CHECK-SAME:                        </td>
+// CHECK-SAME:                     </tr>
+// CHECK-SAME:                  </table>
+// CHECK-SAME:               </td>
+// CHECK-SAME:            </tr>
+// CHECK-SAME:            <tr>
+// CHECK-SAME:               <td></td>
+// CHECK-SAME:               <td align="left">
+// CHECK-SAME:                  reg_$4<int d>
+// CHECK-SAME:               </td>
+// CHECK-SAME:               <td align="left">
+// CHECK-SAME:                  <table border='1'>
+// CHECK-SAME:                     <tr>
+// CHECK-SAME:                        <td>
+// CHECK-SAME:                           reg_$5<int e>
+// CHECK-SAME:                        </td>
+// CHECK-SAME:                     </tr>
+// CHECK-SAME:                  </table>
+// CHECK-SAME:               </td>
+// CHECK-SAME:            </tr>
+// CHECK-SAME:         </table>
+// CHECK-SAME:      </td>
+// CHECK-SAME:   </tr>
+
+Node0x1 [shape=record,label=
+ "{
+    {
+      "state_id": 2,
+      "program_points": [
+        {
+          "kind": "BlockEntrance", "block_id": 1,
+          "terminator": null, "term_kind": null,
+          "tag": null, "node_id": 1,
+          "has_report": 0, "is_sink": 0
+        }
+      ],
+      "program_state": {
+        "store": null,
+        "environment": null,
+        "dynamic_types": null,
+        "constructing_objects": null,
+        "checker_messages": null,
+        "constraints": null,
+        "equivalence_classes": null,
+        "disequality_info": [
+          {
+            "class": [ "reg_$0<int a>" ],
+            "disequal_to": [
+              [ "(reg_$1<int b>) - 2" ],
+              [ "reg_$2<int c>" ]]
+          },
+          {
+            "class": [ "reg_$4<int d>" ],
+            "disequal_to": [
+              [ "reg_$5<int e>" ]]
+          }
+        ]
+      }
+    }
+\l}"];
diff --git a/clang/test/Analysis/exploded-graph-rewriter/disequality_info_diff.dot b/clang/test/Analysis/exploded-graph-rewriter/disequality_info_diff.dot
new file mode 100644
--- /dev/null
+++ b/clang/test/Analysis/exploded-graph-rewriter/disequality_info_diff.dot
@@ -0,0 +1,138 @@
+// RUN: %exploded_graph_rewriter -d %s | FileCheck %s
+
+Node0x1 [shape=record,label=
+ "{
+    {
+      "state_id": 2,
+      "program_points": [
+        {
+          "kind": "BlockEntrance", "block_id": 1,
+          "terminator": null, "term_kind": null,
+          "tag": null, "node_id": 1,
+          "has_report": 0, "is_sink": 0
+        }
+      ],
+      "program_state": {
+        "store": null,
+        "environment": null,
+        "dynamic_types": null,
+        "constructing_objects": null,
+        "checker_messages": null,
+        "constraints": null,
+        "equivalence_classes": null,
+        "disequality_info": [
+          {
+            "class": [ "reg_$0<int a>" ],
+            "disequal_to": [
+              [ "(reg_$1<int b>) - 2" ],
+              [ "reg_$2<int c>" ]]
+          },
+          {
+            "class": [ "reg_$4<int d>" ],
+            "disequal_to": [
+              [ "reg_$5<int e>" ]]
+          }
+        ]
+      }
+    }
+\l}"];
+
+Node0x1 -> Node0x3;
+
+
+// CHECK: Node0x3 [
+// CHECK-SAME: <tr>
+// CHECK-SAME:    <td><font color="red">-</font></td>
+// CHECK-SAME:    <td align="left">
+// CHECK-SAME:       reg_$4
+// CHECK-SAME:       <int d>
+// CHECK-SAME:    </td>
+// CHECK-SAME:    <td align="left">
+// CHECK-SAME:       <table border='1'>
+// CHECK-SAME:          <tr>
+// CHECK-SAME:             <td>
+// CHECK-SAME:                reg_$5<int e>
+// CHECK-SAME:             </td>
+// CHECK-SAME:          </tr>
+// CHECK-SAME:       </table>
+// CHECK-SAME:    </td>
+// CHECK-SAME: </tr>
+// CHECK-SAME: <tr>
+// CHECK-SAME:    <td><font color="forestgreen">+</font></td>
+// CHECK-SAME:    <td align="left">
+// CHECK-SAME:       reg_$4
+// CHECK-SAME:       <int d>
+// CHECK-SAME:    </td>
+// CHECK-SAME:    <td align="left">
+// CHECK-SAME:       <table border='1'>
+// CHECK-SAME:          <tr>
+// CHECK-SAME:             <td>
+// CHECK-SAME:                reg_$6<int f>
+// CHECK-SAME:             </td>
+// CHECK-SAME:          </tr>
+// CHECK-SAME:       </table>
+// CHECK-SAME:    </td>
+// CHECK-SAME: </tr>
+Node0x3 [shape=record,label=
+ "{
+    {
+      "state_id": 4,
+      "program_points": [
+        {
+          "kind": "BlockEntrance", "block_id": 1,
+          "terminator": null, "term_kind": null,
+          "tag": null, "node_id": 1,
+          "has_report": 0, "is_sink": 0
+        }
+      ],
+      "program_state": {
+        "store": null,
+        "environment": null,
+        "dynamic_types": null,
+        "constructing_objects": null,
+        "checker_messages": null,
+        "constraints": null,
+        "equivalence_classes": null,
+        "disequality_info": [
+          {
+            "class": [ "reg_$0<int a>" ],
+            "disequal_to": [
+              [ "(reg_$1<int b>) - 2" ],
+              [ "reg_$2<int c>" ]]
+          },
+          {
+            "class": [ "reg_$4<int d>" ],
+            "disequal_to": [
+              [ "reg_$6<int f>" ]]
+          }
+        ]
+      }
+    }
+\l}"];
+
+Node0x3 -> Node0x5;
+
+Node0x5 [shape=record,label=
+ "{
+    {
+      "state_id": 6,
+      "program_points": [
+        {
+          "kind": "BlockEntrance", "block_id": 1,
+          "terminator": null, "term_kind": null,
+          "tag": null, "node_id": 1,
+          "has_report": 0, "is_sink": 0
+        }
+      ],
+      "program_state": {
+        "store": null,
+        "environment": null,
+        "constraints": null,
+        "equivalence_classes": null,
+        "disequality_info": null,
+        "dynamic_types": null,
+        "constructing_objects": null,
+        "checker_messages": null
+      }
+    }
+\l}"];
diff --git a/clang/test/Analysis/exploded-graph-rewriter/environment.dot b/clang/test/Analysis/exploded-graph-rewriter/environment.dot
--- a/clang/test/Analysis/exploded-graph-rewriter/environment.dot
+++ b/clang/test/Analysis/exploded-graph-rewriter/environment.dot
@@ -44,6 +44,8 @@
       "program_state": {
         "store": null,
         "constraints": null,
+        "equivalence_classes": null,
+        "disequality_info": null,
         "dynamic_types": null,
         "constructing_objects": null,
         "checker_messages": null,
diff --git a/clang/test/Analysis/exploded-graph-rewriter/environment_diff.dot b/clang/test/Analysis/exploded-graph-rewriter/environment_diff.dot
--- a/clang/test/Analysis/exploded-graph-rewriter/environment_diff.dot
+++ b/clang/test/Analysis/exploded-graph-rewriter/environment_diff.dot
@@ -16,6 +16,8 @@
       "program_state": {
         "store": null,
         "constraints": null,
+        "equivalence_classes": null,
+        "disequality_info": null,
         "dynamic_types": null,
         "constructing_objects": null,
         "checker_messages": null,
@@ -71,6 +73,8 @@
       "program_state": {
         "store": null,
         "constraints": null,
+        "equivalence_classes": null,
+        "disequality_info": null,
         "dynamic_types": null,
         "constructing_objects": null,
         "checker_messages": null,
@@ -120,6 +124,8 @@
       "program_state": {
         "store": null,
         "constraints": null,
+        "equivalence_classes": null,
+        "disequality_info": null,
         "dynamic_types": null,
         "constructing_objects": null,
         "checker_messages": null,
diff --git a/clang/test/Analysis/exploded-graph-rewriter/equivalence_classes.dot b/clang/test/Analysis/exploded-graph-rewriter/equivalence_classes.dot
new file mode 100644
--- /dev/null
+++ b/clang/test/Analysis/exploded-graph-rewriter/equivalence_classes.dot
@@ -0,0 +1,53 @@
+// RUN: %exploded_graph_rewriter %s | FileCheck %s
+
+// CHECK:         <tr>
+// CHECK-SAME:       <td align="left"><b>Equivalence Classes: </b></td>
+// CHECK-SAME:    </tr>
+// CHECK-SAME:    <tr>
+// CHECK-SAME:       <td align="left">
+// CHECK-SAME:          <table border="0">
+// CHECK-SAME:             <tr>
+// CHECK-SAME:                <td></td>
+// CHECK-SAME:                <td align="left">0</td>
+// CHECK-SAME:                <td align="left">
+// CHECK-SAME:                   reg_$0<int a>, reg_$1<int b>
+// CHECK-SAME:                </td>
+// CHECK-SAME:             </tr>
+// CHECK-SAME:             <tr>
+// CHECK-SAME:                <td></td>
+// CHECK-SAME:                <td align="left">1</td>
+// CHECK-SAME:                <td align="left">
+// CHECK-SAME:                   reg_$2<int c>, reg_$3<int d>
+// CHECK-SAME:                </td>
+// CHECK-SAME:             </tr>
+// CHECK-SAME:          </table>
+// CHECK-SAME:       </td>
+// CHECK-SAME:    </tr>
+
+Node0x1 [shape=record,label=
+ "{
+    {
+      "state_id": 2,
+      "program_points": [
+        {
+          "kind": "BlockEntrance", "block_id": 1,
+          "terminator": null, "term_kind": null,
+          "tag": null, "node_id": 1,
+          "has_report": 0, "is_sink": 0
+        }
+      ],
+      "program_state": {
+        "store": null,
+        "environment": null,
+        "dynamic_types": null,
+        "constructing_objects": null,
+        "checker_messages": null,
+        "constraints": null,
+        "equivalence_classes": [
+          [ "reg_$0<int a>", "reg_$1<int b>" ],
+          [ "reg_$2<int c>", "reg_$3<int d>" ]
+        ],
+        "disequality_info": null
+      }
+    }
+\l}"];
diff --git a/clang/test/Analysis/exploded-graph-rewriter/constraints_diff.dot b/clang/test/Analysis/exploded-graph-rewriter/equivalence_classes_diff.dot
copy from clang/test/Analysis/exploded-graph-rewriter/constraints_diff.dot
copy to clang/test/Analysis/exploded-graph-rewriter/equivalence_classes_diff.dot
--- a/clang/test/Analysis/exploded-graph-rewriter/constraints_diff.dot
+++ b/clang/test/Analysis/exploded-graph-rewriter/equivalence_classes_diff.dot
@@ -18,9 +18,12 @@
         "dynamic_types": null,
         "constructing_objects": null,
         "checker_messages": null,
-        "constraints": [
-          { "symbol": "reg_$0<x>", "range": "{ [0, 10] }" }
-        ]
+        "constraints": null,
+        "equivalence_classes": [
+          [ "reg_$0<int a>", "reg_$1<int b>" ],
+          [ "reg_$2<int c>", "reg_$3<int d>" ]
+        ],
+        "disequality_info": null
       }
     }
 \l}"];
@@ -29,14 +32,34 @@
 
 // CHECK: Node0x3 [
 // CHECK-SAME: <tr>
-// CHECK-SAME:   <td><font color="red">-</font></td>
-// CHECK-SAME:   <td align="left">reg_$0<x></td>
-// CHECK-SAME:   <td align="left">\{ [0, 10] \}</td>
+// CHECK-SAME:    <td><font color="red">-</font></td>
+// CHECK-SAME:    <td align="left">0</td>
+// CHECK-SAME:    <td align="left">
+// CHECK-SAME:       reg_$0
+// CHECK-SAME:       <int a>
+// CHECK-SAME:       , reg_$1
+// CHECK-SAME:       <int b>
+// CHECK-SAME:    </td>
+// CHECK-SAME: </tr>
+// CHECK-SAME: <tr>
+// CHECK-SAME:    <td><font color="red">-</font></td>
+// CHECK-SAME:    <td align="left">1</td>
+// CHECK-SAME:    <td align="left">
+// CHECK-SAME:       reg_$2
+// CHECK-SAME:       <int c>
+// CHECK-SAME:       , reg_$3
+// CHECK-SAME:       <int d>
+// CHECK-SAME:    </td>
 // CHECK-SAME: </tr>
 // CHECK-SAME: <tr>
-// CHECK-SAME:   <td><font color="forestgreen">+</font></td>
-// CHECK-SAME:   <td align="left">reg_$0<x></td>
-// CHECK-SAME:   <td align="left">\{ [0, 5] \}</td>
+// CHECK-SAME:    <td><font color="forestgreen">+</font></td>
+// CHECK-SAME:    <td align="left">0</td>
+// CHECK-SAME:    <td align="left">
+// CHECK-SAME:       reg_$2
+// CHECK-SAME:       <int e>
+// CHECK-SAME:       , reg_$3
+// CHECK-SAME:       <int f>
+// CHECK-SAME:    </td>
 // CHECK-SAME: </tr>
 Node0x3 [shape=record,label=
  "{
@@ -56,9 +79,11 @@
         "dynamic_types": null,
         "constructing_objects": null,
         "checker_messages": null,
-        "constraints": [
-          { "symbol": "reg_$0<x>", "range": "{ [0, 5] }" }
-        ]
+        "constraints": null,
+        "equivalence_classes": [
+          [ "reg_$2<int e>", "reg_$3<int f>" ]
+        ],
+        "disequality_info": null
       }
     }
 \l}"];
@@ -81,6 +106,8 @@
         "store": null,
         "environment": null,
         "constraints": null,
+        "equivalence_classes": null,
+        "disequality_info": null,
         "dynamic_types": null,
         "constructing_objects": null,
         "checker_messages": null
diff --git a/clang/test/Analysis/exploded-graph-rewriter/store.dot b/clang/test/Analysis/exploded-graph-rewriter/store.dot
--- a/clang/test/Analysis/exploded-graph-rewriter/store.dot
+++ b/clang/test/Analysis/exploded-graph-rewriter/store.dot
@@ -32,6 +32,8 @@
       "program_state": {
         "environment": null,
         "constraints": null,
+        "equivalence_classes": null,
+        "disequality_info": null,
         "dynamic_types": null,
         "constructing_objects": null,
         "checker_messages": null,
diff --git a/clang/test/Analysis/exploded-graph-rewriter/store_diff.dot b/clang/test/Analysis/exploded-graph-rewriter/store_diff.dot
--- a/clang/test/Analysis/exploded-graph-rewriter/store_diff.dot
+++ b/clang/test/Analysis/exploded-graph-rewriter/store_diff.dot
@@ -18,6 +18,8 @@
       "program_state": {
         "environment": null,
         "constraints": null,
+        "equivalence_classes": null,
+        "disequality_info": null,
         "dynamic_types": null,
         "constructing_objects": null,
         "checker_messages": null,
@@ -72,6 +74,8 @@
       "program_state": {
         "environment": null,
         "constraints": null,
+        "equivalence_classes": null,
+        "disequality_info": null,
         "dynamic_types": null,
         "constructing_objects": null,
         "checker_messages": null,
diff --git a/clang/test/Analysis/exploded-graph-rewriter/topology.dot b/clang/test/Analysis/exploded-graph-rewriter/topology.dot
--- a/clang/test/Analysis/exploded-graph-rewriter/topology.dot
+++ b/clang/test/Analysis/exploded-graph-rewriter/topology.dot
@@ -22,6 +22,8 @@
       "program_state": {
         "environment": null,
         "constraints": null,
+        "equivalence_classes": null,
+        "disequality_info": null,
         "dynamic_types": null,
         "constructing_objects": null,
         "checker_messages": [
diff --git a/clang/utils/analyzer/exploded-graph-rewriter.py b/clang/utils/analyzer/exploded-graph-rewriter.py
--- a/clang/utils/analyzer/exploded-graph-rewriter.py
+++ b/clang/utils/analyzer/exploded-graph-rewriter.py
@@ -267,6 +267,8 @@
                 'store': None,
                 'environment': None,
                 'constraints': None,
+                'equivalence_classes': None,
+                'disequality_info': None,
                 'dynamic_types': None,
                 'constructing_objects': None,
                 'checker_messages': None
@@ -285,6 +287,43 @@
             (c['symbol'], c['range']) for c in json_ps['constraints']
         ]) if json_ps['constraints'] is not None else None
 
+        # Each equivalence_class is represented as List[Str].
+        # json_ps['equivalence_classes']: List[List[Str]]
+        # Sort by the first element of each equivalence_class.
+        eq_classes = (
+            json_ps['equivalence_classes']
+            if json_ps['equivalence_classes']
+            else None
+        )
+        self.equivalence_classes = (
+            GenericMap({i: ", ".join(eq_classes[i]) for i in range(0, len(eq_classes))})
+            if eq_classes
+            else None
+        )
+
+        # Each equivalence_class is represented as List[Str].
+        # Disequality info is a mapping from an equivalence class to many
+        # equivalence classes:
+        # json_ps['disequality_info']: Dict[List[Str], List[List[Str]]]
+        def get_diseq_classes(classes):
+            """ Flatten List[List[Str]] to Str """
+            return (
+                "<table border='1'><tr><td>"
+                + "</td></tr><tr><td>".join([", ".join(cl) for cl in classes])
+                + "</td></tr></table>"
+            )
+
+        self.disequality_info = (
+            GenericMap(
+                {
+                    ", ".join(c["class"]): get_diseq_classes(c["disequal_to"])
+                    for c in json_ps["disequality_info"]
+                }
+            )
+            if json_ps["disequality_info"]
+            else None
+        )
+
         self.dynamic_types = GenericMap([
                 (t['region'], '%s%s' % (t['dyn_type'],
                                         ' (or a sub-class)'
@@ -682,8 +721,8 @@
                 self.visit_store(st)
         self._dump('</td></tr>')
 
-    def visit_generic_map(self, m, prev_m=None):
-        self._dump('<table border="0">')
+    def visit_generic_map(self, m, prev_m=None, border=0):
+        self._dump('<table border="%s">' % (border))
 
         def dump_pair(m, k, is_added=None):
             self._dump('<tr><td>%s</td>'
@@ -704,7 +743,7 @@
 
         self._dump('</table>')
 
-    def visit_generic_map_in_state(self, selector, title, s, prev_s=None):
+    def visit_generic_map_in_state(self, selector, title, s, prev_s=None, border=0):
         m = getattr(s, selector)
         prev_m = getattr(prev_s, selector) if prev_s is not None else None
         if m is None and prev_m is None:
@@ -719,12 +758,12 @@
             if prev_m is not None:
                 if m.is_different(prev_m):
                     self._dump('</td></tr><tr><td align="left">')
-                    self.visit_generic_map(m, prev_m)
+                    self.visit_generic_map(m, prev_m, border)
                 else:
                     self._dump('<i> No changes!</i>')
             else:
                 self._dump('</td></tr><tr><td align="left">')
-                self.visit_generic_map(m)
+                self.visit_generic_map(m, prev_m=None, border=border)
 
         self._dump('</td></tr>')
 
@@ -791,6 +830,12 @@
                                         s, prev_s)
         self.visit_generic_map_in_state('constraints', 'Ranges',
                                         s, prev_s)
+        self.visit_generic_map_in_state('equivalence_classes',
+                                        'Equivalence Classes',
+                                        s, prev_s)
+        self.visit_generic_map_in_state('disequality_info',
+                                        'Disequality Info',
+                                        s, prev_s, border=1)
         self.visit_generic_map_in_state('dynamic_types', 'Dynamic Types',
                                         s, prev_s)
         self.visit_environment_in_state('constructing_objects',