From: Tianyi Liang <tianyi-liang@uiowa.edu>
Date: Thu, 23 Jan 2014 08:48:41 +0000 (-0600)
Subject: minor fix
X-Git-Tag: cvc5-1.0.0~7131
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=f439febe8aa7940da136e6e6a87758ec3a669612;p=cvc5.git

minor fix
---

diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index fa3f77e9f..125c1292a 100644
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -1365,11 +1365,11 @@ bool TheoryStrings::normalizeDisequality( Node ni, Node nj ) {
 							Node sk1 = NodeManager::currentNM()->mkSkolem( "x_dsplit_$$", ni.getType(), "created for disequality normalization" );
 							Node sk2 = NodeManager::currentNM()->mkSkolem( "y_dsplit_$$", ni.getType(), "created for disequality normalization" );
 							Node sk3 = NodeManager::currentNM()->mkSkolem( "z_dsplit_$$", ni.getType(), "created for disequality normalization" );
-							Node nemp = sk1.eqNode(d_emptyString).negate();
-							conc.push_back(nemp);
-							nemp = sk2.eqNode(d_emptyString).negate();
-							conc.push_back(nemp);
-							nemp = sk3.eqNode(d_emptyString).negate();
+							//Node nemp = sk1.eqNode(d_emptyString).negate();
+							//conc.push_back(nemp);
+							//nemp = sk2.eqNode(d_emptyString).negate();
+							//conc.push_back(nemp);
+							Node nemp = sk3.eqNode(d_emptyString).negate();
 							conc.push_back(nemp);
 							Node lsk1 = getLength( sk1 );
 							conc.push_back( lsk1.eqNode( li ) );