Make `STRINGS_CTN_DECOMPOSE` an explicit conflict (#6663)

Fixes #6643. The STRINGS_CTN_DECOMPOSE inference is always a conflict
but we sometimes sent it as an inference. To make sure that the
inference manager actually recognizes the inference as a conflict, this
commit ensures that the conclusion is always false and modifies the
explanation accordingly.

1 files changed, 3 insertions, 1 deletions

diff --git a/src/theory/strings/extf_solver.cpp b/src/theory/strings/extf_solver.cpp
index 8b5e35023..fc8fb15b0 100644
--- a/src/theory/strings/extf_solver.cpp
+++ b/src/theory/strings/extf_solver.cpp
@@ -547,7 +547,9 @@ void ExtfSolver::checkExtfInference(Node n,
             if (d_state.areEqual(conc, d_false))
             {
               // we are in conflict
-              d_im.sendInference(in.d_exp, conc, InferenceId::STRINGS_CTN_DECOMPOSE);
+              d_im.addToExplanation(conc, d_false, in.d_exp);
+              d_im.sendInference(
+                  in.d_exp, d_false, InferenceId::STRINGS_CTN_DECOMPOSE);
               Assert(d_state.isInConflict());
               return;
             }