From 10c36f53033aadb6e2f3bf16f2d7305b793fd0e4 Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Fri, 13 Apr 2018 19:38:17 -0500
Subject: [PATCH] Disable split for negative contains. (#1774)

---
 src/theory/strings/theory_strings.cpp | 3 ---
 1 file changed, 3 deletions(-)

diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index 59b2e8ea0..142695b9d 100644
--- 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;
           }
-- 
2.30.2