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 531b281a75b394ee2dc2090973d51ebd804e602a..7e416d1320f0930c051a2f0389a162b67e35bb7a 100644 (file)
--- 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 ac6d91e7cdd690f10eb17b7cbae04b96d3b90b61..5104b07b89cb8068c439ca04133744c60cff15f7 100644 (file)
--- 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 (file)
index 0000000..bde9726
--- /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)