fix a bug in contain

diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index e60e67ac1aa51c39183f71148d2b4e931341a637..e73cf5e9d609d6bac71aeabd1ca02bf53f1b82a3 100644 (file)
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -2846,12 +2846,16 @@ bool TheoryStrings::checkNegContains() {
             }
           } else if(!areDisequal(lenx, lens)) {
             if(d_neg_ctn_ulen.find(atom) == d_neg_ctn_ulen.end()) {
+              lenx = NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, x);
+              lens = NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, s);
               d_neg_ctn_ulen.insert( atom );
               sendSplit(lenx, lens, "NEG-CTN-SP");
               addedLemma = true;
             }
           } else {
             if(d_neg_ctn_cached.find(atom) == d_neg_ctn_cached.end()) {
+              lenx = NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, x);
+              lens = NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, s);
               Node b1 = NodeManager::currentNM()->mkBoundVar(NodeManager::currentNM()->integerType());
               Node b1v = NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST, b1);
               Node g1 = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::AND, NodeManager::currentNM()->mkNode( kind::GEQ, b1, d_zero ),

diff --git a/src/theory/strings/theory_strings_preprocess.cpp b/src/theory/strings/theory_strings_preprocess.cpp
index 0cccdf0ef7663341a0ca95091d085e476474e7fd..be419a36affea1c2d426ae72af9340c91da4d22f 100644 (file)
--- a/src/theory/strings/theory_strings_preprocess.cpp
+++ b/src/theory/strings/theory_strings_preprocess.cpp
@@ -482,9 +482,14 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) {
       Node cond = NodeManager::currentNM()->mkNode( kind::STRING_STRCTN, x, y );
       Node c1 = x.eqNode( NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, sk1, y, sk2 ) );
       Node c2 = skw.eqNode( NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, sk1, z, sk2 ) );
-      //Node c3 = NodeManager::currentNM()->mkNode( kind::STRING_STRCTN, sk1, y ).negate();
+      Node c3 = NodeManager::currentNM()->mkNode(kind::STRING_STRCTN,
+                  NodeManager::currentNM()->mkNode(kind::STRING_CONCAT, sk1,
+                     NodeManager::currentNM()->mkNode(kind::STRING_SUBSTR_TOTAL, y, d_zero,
+                        NodeManager::currentNM()->mkNode(kind::MINUS, 
+                          NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, y), 
+                          NodeManager::currentNM()->mkConst(::CVC4::Rational(1))))), y).negate();
       Node rr = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::ITE, cond,
-              NodeManager::currentNM()->mkNode( kind::AND, c1, c2), // c3 
+              NodeManager::currentNM()->mkNode( kind::AND, c1, c2, c3),
               skw.eqNode(x) ) );
       new_nodes.push_back( rr );
       rr = Rewriter::rewrite( NodeManager::currentNM()->mkNode(kind::GT, NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, y), d_zero) );