Disable split for negative contains. (#1774)

diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index 59b2e8ea07d0ab9f521628fb3a8b37fe42ee9399..142695b9dd59e735199be35bc549d55725b9999b 100644 (file)
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -387,9 +387,6 @@ int TheoryStrings::getReduction( int effort, Node n, Node& nr ) {
               sendInference( lexp, xneqs, "NEG-CTN-EQL", true );
             }
             return 1;
-          }else if( !areDisequal( lenx, lens ) ){
-            //split on their lenths
-            sendSplit( lenx, lens, "NEG-CTN-SP" );
           }else{
             r_effort = 2;
           }