minor fix

diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index fa3f77e9fd0e3fa26538ad059833acae19571ffc..125c1292a45ba157fb19431068be7bce31ec4c0a 100644 (file)
--- 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 ) );