From b57f04e2d2c74d124d72765964cae95475287f3b Mon Sep 17 00:00:00 2001
From: Murphy Berzish <murphy.berzish@gmail.com>
Date: Tue, 6 Dec 2016 12:59:40 -0500
Subject: [PATCH] optimize generate_mutual_exclusion in theory_str to make only
 half as many subterms

---
 src/smt/theory_str.cpp | 7 +------
 1 file changed, 1 insertion(+), 6 deletions(-)

diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp
index 3d22427d5..4b38d02d3 100644
--- a/src/smt/theory_str.cpp
+++ b/src/smt/theory_str.cpp
@@ -2449,13 +2449,8 @@ expr_ref theory_str::generate_mutual_exclusion(expr_ref_vector & terms) {
 
     expr_ref_vector result(m);
 
-    // TODO this can probably be made more efficient
-
     for (unsigned int majorIndex = 0; majorIndex < terms.size(); ++majorIndex) {
-        for (unsigned int minorIndex = 0; minorIndex < terms.size(); ++minorIndex) {
-            if (majorIndex == minorIndex) {
-                continue;
-            }
+        for (unsigned int minorIndex = majorIndex + 1; minorIndex < terms.size(); ++minorIndex) {
             // generate an expression of the form
             // terms[majorIndex] --> NOT(terms[minorIndex])
             expr_ref ex(rewrite_implication(terms.get(majorIndex), m.mk_not(terms.get(minorIndex))), m);