bring back D-Norm

diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index f819d46fb32d762c7d4fb29a6673db3f4d1c7507..fd9605e59da61f908e46da89c3e1dfcd4c290a72 100644 (file)
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -1979,10 +1979,10 @@ void TheoryStrings::checkDeqNF() {
                        for( unsigned j=0; j<cols[i].size(); j++ ){
                                for( unsigned k=(j+1); k<cols[i].size(); k++ ){
                                        Assert( !d_conflict );
-                                       //if( !areDisequal( cols[i][j], cols[i][k] ) ){
-                                       //      sendSplit( cols[i][j], cols[i][k], "D-NORM", false );
-                                       //      return;
-                                       //}else{
+                                       if( !areDisequal( cols[i][j], cols[i][k] ) ){
+                                               sendSplit( cols[i][j], cols[i][k], "D-NORM", false );
+                                               return;
+                                       }else{
                                                Trace("strings-solve") << "- Compare ";
                                                printConcat( d_normal_forms[cols[i][j]], "strings-solve" );
                                                Trace("strings-solve") << " against ";
@@ -1991,7 +1991,7 @@ void TheoryStrings::checkDeqNF() {
                                                if( processDeq( cols[i][j], cols[i][k] ) ){
                                                        return;
                                                }
-                                       //}
+                                       }
                                }
                        }
                }