From: Tianyi Liang <tianyi-liang@uiowa.edu>
Date: Wed, 8 Jan 2014 01:18:55 +0000 (-0600)
Subject: minor fix, bring back the assertion.
X-Git-Tag: cvc5-1.0.0~7165
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=0c91ca68da84414dd49262ce244084ff2bdec34c;p=cvc5.git

minor fix, bring back the assertion.
---

diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index bb5e3718a..99d64270b 100644
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -51,6 +51,7 @@ TheoryStrings::TheoryStrings(context::Context* c, context::UserContext* u, Outpu
     //d_equalityEngine.addFunctionKind(kind::STRING_IN_REGEXP);
     d_equalityEngine.addFunctionKind(kind::STRING_LENGTH);
     d_equalityEngine.addFunctionKind(kind::STRING_CONCAT);
+    d_equalityEngine.addFunctionKind(kind::STRING_STRCTN);
 
     d_zero = NodeManager::currentNM()->mkConst( Rational( 0 ) );
     d_emptyString = NodeManager::currentNM()->mkConst( ::CVC4::String("") );
diff --git a/src/theory/uf/equality_engine.cpp b/src/theory/uf/equality_engine.cpp
index 0d6c93719..df1d2ebde 100644
--- a/src/theory/uf/equality_engine.cpp
+++ b/src/theory/uf/equality_engine.cpp
@@ -1152,7 +1152,7 @@ void EqualityEngine::addTriggerEquality(TNode eq) {
 
 void EqualityEngine::addTriggerPredicate(TNode predicate) {
   Assert(predicate.getKind() != kind::NOT && predicate.getKind() != kind::EQUAL);
-  //Assert(d_congruenceKinds.tst(predicate.getKind()), "No point in adding non-congruence predicates");
+  Assert(d_congruenceKinds.tst(predicate.getKind()), "No point in adding non-congruence predicates");
 
   if (d_done) {
     return;