Better heuristics for marking congruent variables (#3677)

diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index 7b1b3491739ce5c7bc7d67d6b31738225a533717..755e6b4df2f56e7a3010920bba51ebd0642c51d2 100644 (file)
--- 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);
             }
           }
         }