diff options
| author | Tianyi Liang <tianyi-liang@uiowa.edu> | 2014-01-23 02:48:41 -0600 |
|---|---|---|
| committer | Tianyi Liang <tianyi-liang@uiowa.edu> | 2014-01-23 02:48:41 -0600 |
| commit | f439febe8aa7940da136e6e6a87758ec3a669612 (patch) | |
| tree | 2f4558467f62594eeeac10650944d53bd0ae78bc /src/theory/strings | |
| parent | 13e030f775f7916e89ad576222d45068777f2d2e (diff) | |
minor fix
Diffstat (limited to 'src/theory/strings')
| -rw-r--r-- | src/theory/strings/theory_strings.cpp | 10 |
1 files 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 ) ); |