From e3361a428a1b24369d782120de1f050874a8ac44 Mon Sep 17 00:00:00 2001
From: Andres Noetzli <andres.noetzli@gmail.com>
Date: Wed, 29 Jan 2020 18:29:15 -0800
Subject: [PATCH] Better heuristics for marking congruent variables (#3677)

---
 src/theory/strings/theory_strings.cpp | 21 +++++++++++++++++----
 1 file changed, 17 insertions(+), 4 deletions(-)

diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index 7b1b34917..755e6b4df 100644
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -1401,11 +1401,24 @@ void TheoryStrings::checkInit() {
           }
         }else{
           if( d_congruent.find( n )==d_congruent.end() ){
-            if( var.isNull() ){
+            // We mark all but the oldest variable in the equivalence class as
+            // congruent.
+            if (var.isNull())
+            {
               var = n;
-            }else{
-              Trace("strings-process-debug") << "  congruent variable : " << n << std::endl;
-              d_congruent.insert( n );
+            }
+            else if (var > n)
+            {
+              Trace("strings-process-debug")
+                  << "  congruent variable : " << var << std::endl;
+              d_congruent.insert(var);
+              var = n;
+            }
+            else
+            {
+              Trace("strings-process-debug")
+                  << "  congruent variable : " << n << std::endl;
+              d_congruent.insert(n);
             }
           }
         }
-- 
2.30.2