summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--src/theory/strings/theory_strings.cpp10
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);
+ }
}
}
}
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback