Prefer old variable heuristicoldVarHeuristic

1 files changed, 9 insertions, 1 deletions

diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index 35868fb69..331e9f0ff 100644
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -1405,7 +1405,15 @@ void TheoryStrings::checkInit() {
               var = n;
             }else{
               Trace("strings-process-debug") << "  congruent variable : " << n << std::endl;
-              d_congruent.insert( n );
+              if (var > n)
+              {
+                d_congruent.insert(var);
+                var = n;
+              }
+              else
+              {
+                d_congruent.insert(n);
+              }
             }
           }
         }