From f439febe8aa7940da136e6e6a87758ec3a669612 Mon Sep 17 00:00:00 2001 From: Tianyi Liang Date: Thu, 23 Jan 2014 02:48:41 -0600 Subject: [PATCH] minor fix --- src/theory/strings/theory_strings.cpp | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) 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 ) ); -- 2.30.2