Strings: Register skolems before sending lemma (#4381)

This commit fixes a performance regression introduced by commit 6255c03. The issue seems to be that registering terms manually after sending the lemma on the output channel is too late because the output channel processes the lemma eagerly.

diff --git a/src/theory/strings/inference_manager.cpp b/src/theory/strings/inference_manager.cpp
index 42dc975fae602a066a4312b579d51ea337266f7f..9fb1011ee23ee366198b16a00e472dfeafa62925 100644 (file)
--- a/src/theory/strings/inference_manager.cpp
+++ b/src/theory/strings/inference_manager.cpp
@@ -359,7 +359,6 @@ void InferenceManager::doPendingLemmas()
     // only keep stats if we process it here
     d_statistics.d_inferences << ii.d_id;
     ++(d_statistics.d_lemmasInfer);
-    d_out.lemma(lem);
 
     // Process the side effects of the inference info.
     // Register the new skolems from this inference. We register them here
@@ -373,6 +372,8 @@ void InferenceManager::doPendingLemmas()
         d_termReg.registerTermAtomic(n, sks.first);
       }
     }
+
+    d_out.lemma(lem);
   }
   // process the pending require phase calls
   for (const std::pair<const Node, bool>& prp : d_pendingReqPhase)