From: Tianyi Liang <tianyi-liang@uiowa.edu>
Date: Mon, 21 Oct 2013 17:29:48 +0000 (-0500)
Subject: string fix
X-Git-Tag: cvc5-1.0.0~7275^2~6
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=730e88ecb2b3ae6fdb9148c096820516c61356f3;p=cvc5.git

string fix
---

diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index 435be2ba4..910447589 100644
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -548,8 +548,13 @@ void TheoryStrings::doPendingFacts() {
       bool polarity = fact.getKind() != kind::NOT;
       TNode atom = polarity ? fact : fact[0];
       if (atom.getKind() == kind::EQUAL) {
-		Assert( d_equalityEngine.hasTerm( atom[0] ) );
-		Assert( d_equalityEngine.hasTerm( atom[1] ) );
+		//Assert( d_equalityEngine.hasTerm( atom[0] ) );
+		//Assert( d_equalityEngine.hasTerm( atom[1] ) );
+		for( unsigned j=0; j<2; j++ ){
+			if( !d_equalityEngine.hasTerm( atom[j] ) ){
+				d_equalityEngine.addTerm( atom[j] );
+			}
+		}
 		d_equalityEngine.assertEquality( atom, polarity, exp );
       }else{
         d_equalityEngine.assertPredicate( atom, polarity, exp );
@@ -797,7 +802,7 @@ bool TheoryStrings::normalizeEquivalenceClass( Node eqc, std::vector< Node > & v
 										}
 										Node eq = NodeManager::currentNM()->mkNode( kind::EQUAL, d_emptyString, normal_forms[k][index_k] );
 										Trace("strings-lemma") << "Strings : Infer " << eq << " from " << eq_exp << std::endl;
-										Assert( !d_equalityEngine.areEqual( d_emptyString, normal_forms[k][index_k] ) );
+										Assert( !areEqual( d_emptyString, normal_forms[k][index_k] ) );
 										d_pending.push_back( eq );
 										d_pending_exp[eq] = eq_exp;
 										d_infer.push_back(eq);