From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Sat, 14 Apr 2018 00:38:17 +0000 (-0500)
Subject: Disable split for negative contains. (#1774)
X-Git-Tag: cvc5-1.0.0~5155
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=10c36f53033aadb6e2f3bf16f2d7305b793fd0e4;p=cvc5.git

Disable split for negative contains. (#1774)
---

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;
           }