From 9dca8d18ed9711ad14e12cb4176454c38bbbc355 Mon Sep 17 00:00:00 2001
From: JohnLyu2 <65240623+JohnLyu2@users.noreply.github.com>
Date: Fri, 2 Sep 2022 16:36:11 -0400
Subject: [PATCH] fix negative contains bug (#6312)

---
 src/smt/theory_str.cpp | 19 +++++++++++++------
 1 file changed, 13 insertions(+), 6 deletions(-)

diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp
index 8bd6c49aa..955241efd 100644
--- a/src/smt/theory_str.cpp
+++ b/src/smt/theory_str.cpp
@@ -8436,6 +8436,14 @@ namespace smt {
             }
         }
 
+        bool existNegativeContains = false;
+        expr_ref_vector assignments(m);
+        ctx.get_assignments(assignments);
+        for (expr * a : assignments) {
+            expr * subterm;
+            if (m.is_not(a, subterm) && u.str.is_contains(subterm)) existNegativeContains = true;
+        }
+
         if (!needToAssignFreeVars) {
 
             // check string-int terms
@@ -8506,9 +8514,11 @@ namespace smt {
             // we're not done if some variable in a regex membership predicate was unassigned
             if (regexOK) {
                 if (unused_internal_variables.empty()) {
-                    TRACE("str", tout << "All variables are assigned. Done!" << std::endl;);
-                    m_stats.m_solved_by = 2;
-                    return FC_DONE;
+                    if (!existNegativeContains) {
+                        TRACE("str", tout << "All variables are assigned. Done!" << std::endl;);
+                        m_stats.m_solved_by = 2;
+                        return FC_DONE;
+                    }
                 } else {
                     TRACE("str", tout << "Assigning decoy values to free internal variables." << std::endl;);
                     for (auto const &var : unused_internal_variables) {
@@ -8561,9 +8571,6 @@ namespace smt {
             }
             TRACE("str", tout << "arithmetic solver done in final check" << std::endl;);
 
-            expr_ref_vector assignments(m);
-            ctx.get_assignments(assignments);
-
             expr_ref_vector precondition(m);
             expr_ref_vector cex(m);
             lbool model_status = fixed_length_model_construction(assignments, precondition, free_variables, candidate_model, cex);