Do not process conjunctions as facts in strings (#6065)

This changes things so we process inferences with AND conclusions as lemmas always.

This fixes #6056, that benchmark times out.

diff --git a/src/theory/strings/infer_info.cpp b/src/theory/strings/infer_info.cpp
index 6d87aa94490fa1ca35341901a6a3a2499221ead2..dc0cc0cfddafc419b70245ee41b7d553057451af 100644 (file)
--- a/src/theory/strings/infer_info.cpp
+++ b/src/theory/strings/infer_info.cpp
@@ -56,7 +56,11 @@ bool InferInfo::isFact() const
 {
   Assert(!d_conc.isNull());
   TNode atom = d_conc.getKind() == kind::NOT ? d_conc[0] : d_conc;
-  return !atom.isConst() && atom.getKind() != kind::OR && d_noExplain.empty();
+  // we could process inferences with conjunctive conclusions as facts, where
+  // the explanation is copied. However, for simplicity, we always send these
+  // as lemmas. This case happens very infrequently.
+  return !atom.isConst() && atom.getKind() != kind::OR
+         && atom.getKind() != kind::AND && d_noExplain.empty();
 }
 
 Node InferInfo::getPremises() const