Fix for string disequality processing (#1679)

diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index 81b0118c5768743da6c648d0bfea68cef10afa1b..b5a4370d41c29c5e6d817e05a0f0bfbd2a6bcb50 100644 (file)
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -3142,13 +3142,25 @@ int TheoryStrings::processReverseDeq( std::vector< Node >& nfi, std::vector< Nod
 }
 
 int TheoryStrings::processSimpleDeq( std::vector< Node >& nfi, std::vector< Node >& nfj, Node ni, Node nj, unsigned& index, bool isRev ){
-  //see if one side is constant, if so, we can approximate as containment
-  for( unsigned i=0; i<2; i++ ){
-    Node c = getConstantEqc( i==0 ? ni : nj );
-    if( !c.isNull() ){
-      int findex, lindex;
-      if( !TheoryStringsRewriter::canConstantContainList( c, i==0 ? nfj : nfi, findex, lindex ) ){
-        return 1;
+  // See if one side is constant, if so, the disequality ni != nj is satisfied
+  // since ni does not contain nj or vice versa.
+  // This is only valid when isRev is false, since when isRev=true, the contents
+  // of normal form vectors nfi and nfj are reversed.
+  if (!isRev)
+  {
+    for (unsigned i = 0; i < 2; i++)
+    {
+      Node c = getConstantEqc(i == 0 ? ni : nj);
+      if (!c.isNull())
+      {
+        int findex, lindex;
+        if (!TheoryStringsRewriter::canConstantContainList(
+                c, i == 0 ? nfj : nfi, findex, lindex))
+        {
+          Trace("strings-solve-debug")
+              << "Disequality: constant cannot contain list" << std::endl;
+          return 1;
+        }
       }
     }
   }

diff --git a/test/regress/regress1/strings/Makefile.am b/test/regress/regress1/strings/Makefile.am
index f6326e0c6c2416d39c66d6a550243c573ab56bbc..7e9242e733ab005affe2786f68bf527af7913a65 100644 (file)
--- a/test/regress/regress1/strings/Makefile.am
+++ b/test/regress/regress1/strings/Makefile.am
@@ -73,7 +73,8 @@ TESTS =       \
        str007.smt2 \
        rew-020618.smt2 \
        double-replace.smt2 \
-       string-unsound-sem.smt2
+       string-unsound-sem.smt2 \
+       goodAI.smt2
 
 EXTRA_DIST = $(TESTS)
 

diff --git a/test/regress/regress1/strings/goodAI.smt2 b/test/regress/regress1/strings/goodAI.smt2
new file mode 100644 (file)
index 0000000..0dc5c8a
--- /dev/null
+++ b/test/regress/regress1/strings/goodAI.smt2
@@ -0,0 +1,8 @@
+(set-logic QF_S)
+(set-option :strings-exp true)
+(set-info :status sat)
+(declare-const input_0_1000 String)
+(assert (= (str.substr input_0_1000 0 4) "good"))
+(assert (= (str.substr input_0_1000 5 1) "I"))
+(assert (not (= input_0_1000 "goodAI")))
+(check-sat)