From 05abf190098d8dea5f9bdc8957a049171bb99c0e Mon Sep 17 00:00:00 2001
From: Arie Gurfinkel <arie.gurfinkel@uwaterloo.ca>
Date: Thu, 14 Jun 2018 16:38:27 -0700
Subject: [PATCH] comment

---
 src/qe/qe_term_graph.cpp | 10 +++++++---
 1 file changed, 7 insertions(+), 3 deletions(-)

diff --git a/src/qe/qe_term_graph.cpp b/src/qe/qe_term_graph.cpp
index 4a08eeb89..6018d763a 100644
--- a/src/qe/qe_term_graph.cpp
+++ b/src/qe/qe_term_graph.cpp
@@ -767,11 +767,15 @@ namespace qe {
                     val2rep.insert(val, rep);
                 }
             }
-            // TBD: ignore distinct on Booleans
+
+            // TBD: optimize further based on implied values (e.g.,
+            // some literals are forced to be true/false) and based on
+            // unique_values (e.g., (x=1 & y=1) does not require
+            // (x!=y) to be added
             ptr_buffer<expr> reps;
             for (auto &kv : val2rep) {
-                expr *val = kv.m_value;
-                if (!m.is_unique_value(val))
+                expr *rep = kv.m_value;
+                if (!m.is_unique_value(rep))
                     reps.push_back(kv.m_value);
             }