From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Sat, 14 Nov 2020 14:57:39 +0000 (-0600)
Subject: Fix double conflict in extended string solver (#5435)
X-Git-Tag: cvc5-1.0.0~2597
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=a71274b992ea5ddfb930b754f1b705f417f7b4e5;p=cvc5.git

Fix double conflict in extended string solver (#5435)

Fixes #5384.

Previously we were not breaking on conflict in all cases.
---

diff --git a/src/theory/strings/extf_solver.cpp b/src/theory/strings/extf_solver.cpp
index 531b281a7..7e416d132 100644
--- a/src/theory/strings/extf_solver.cpp
+++ b/src/theory/strings/extf_solver.cpp
@@ -392,11 +392,6 @@ void ExtfSolver::checkExtfEval(int effort)
             Inference inf = effort == 0 ? Inference::EXTF : Inference::EXTF_N;
             d_im.sendInference(einfo.d_exp, conc, inf, false, true);
             d_statistics.d_cdSimplifications << n.getKind();
-            if (d_state.isInConflict())
-            {
-              Trace("strings-extf-debug") << "  conflict, return." << std::endl;
-              return;
-            }
           }
         }
         else
@@ -474,6 +469,11 @@ void ExtfSolver::checkExtfEval(int effort)
         has_nreduce = true;
       }
     }
+    if (d_state.isInConflict())
+    {
+      Trace("strings-extf-debug") << "  conflict, return." << std::endl;
+      return;
+    }
   }
   d_hasExtf = has_nreduce;
 }
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index ac6d91e7c..5104b07b8 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -1010,6 +1010,7 @@ set(regress_0_tests
   regress0/strings/issue4820.smt2
   regress0/strings/issue4915.smt2
   regress0/strings/issue5090.smt2
+  regress0/strings/issue5384-double-conflict.smt2
   regress0/strings/issue5428-re-diff-assoc.smt2
   regress0/strings/itos-entail.smt2
   regress0/strings/large-model.smt2
diff --git a/test/regress/regress0/strings/issue5384-double-conflict.smt2 b/test/regress/regress0/strings/issue5384-double-conflict.smt2
new file mode 100644
index 000000000..bde9726bb
--- /dev/null
+++ b/test/regress/regress0/strings/issue5384-double-conflict.smt2
@@ -0,0 +1,13 @@
+(set-logic QF_S)
+(set-option :strings-exp true)
+(set-info :status sat)
+(declare-fun _substvar_130_ () Bool)
+(declare-fun _substvar_156_ () Bool)
+(declare-fun _substvar_166_ () Bool)
+(declare-fun str0 () String)
+(declare-fun str8 () String)
+(declare-fun str19 () String)
+(assert (distinct "" str0))
+(assert (xor _substvar_166_ _substvar_130_ (str.prefixof (str.++ "" "" "" "" "\u2c6b\u0153\u0180\u16c50\u16b5\u16cd\u16c3\u0182\u16c0\xec\u01ae\u016f\u024bf") (str.++ "" str0 "\u0179\u0144\u0247")) true true))
+(assert (=> (str.contains str8 str19) _substvar_156_))
+(check-sat)