From 8f0aae827e16f4dfcebb8dad2cc528649d40b16a Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Wed, 21 Mar 2018 08:03:48 -0500
Subject: [PATCH] Fix for string disequality processing (#1679)

---
 src/theory/strings/theory_strings.cpp     | 26 +++++++++++++++++------
 test/regress/regress1/strings/Makefile.am |  3 ++-
 test/regress/regress1/strings/goodAI.smt2 |  8 +++++++
 3 files changed, 29 insertions(+), 8 deletions(-)
 create mode 100644 test/regress/regress1/strings/goodAI.smt2

diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index 81b0118c5..b5a4370d4 100644
--- 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 f6326e0c6..7e9242e73 100644
--- 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
index 000000000..0dc5c8ab1
--- /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)
-- 
2.30.2