diff options
-rw-r--r-- | src/theory/strings/theory_strings.cpp | 21 |
1 files 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); } } } |