Fix double conflict in extended string solver (#5435)

Fixes #5384.

Previously we were not breaking on conflict in all cases.

1 files changed, 5 insertions, 5 deletions

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;
 }