Fix related to preregistering boolean term variables in strings (#5331)

We should only add trigger predicates for string predicates, and not arbitrary Boolean terms (which can now occur since we are handling parametric sequences).

This avoids a debug assertion failure reported on as a followup to #4370. In that benchmark BOOLEAN_TERM_VARIABLE was being added as a trigger predicate.

2 files changed, 7 insertions, 3 deletions

diff --git a/src/theory/strings/term_registry.cpp b/src/theory/strings/term_registry.cpp
index b5b2a5a13..2b5daa476 100644
--- a/src/theory/strings/term_registry.cpp
+++ b/src/theory/strings/term_registry.cpp
@@ -203,8 +203,12 @@ void TermRegistry::preRegisterTerm(TNode n)
   }
   else if (tn.isBoolean())
   {
-    // Get triggered for both equal and dis-equal
-    ee->addTriggerPredicate(n);
+    // All kinds that we do congruence over that may return a Boolean go here
+    if (k==STRING_STRCTN || k == STRING_LEQ || k == SEQ_NTH)
+    {
+      // Get triggered for both equal and dis-equal
+      ee->addTriggerPredicate(n);
+    }
   }
   else
   {
diff --git a/src/theory/uf/equality_engine.cpp b/src/theory/uf/equality_engine.cpp
index e48e91cd0..fdb80e878 100644
--- a/src/theory/uf/equality_engine.cpp
+++ b/src/theory/uf/equality_engine.cpp
@@ -1739,7 +1739,7 @@ void EqualityEngine::addTriggerPredicate(TNode predicate) {
     return addTriggerEquality(predicate);
   }
   Assert(d_congruenceKinds.tst(predicate.getKind()))
-      << "No point in adding non-congruence predicates";
+      << "No point in adding non-congruence predicates, kind is " << predicate.getKind();
 
   if (d_done) {
     return;