From 855143cfa1e4cf38f67ff99eba5d59e5a2786120 Mon Sep 17 00:00:00 2001 From: Andres Noetzli Date: Wed, 22 Apr 2020 17:55:33 -0700 Subject: [PATCH] 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. --- src/theory/strings/inference_manager.cpp | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/theory/strings/inference_manager.cpp b/src/theory/strings/inference_manager.cpp index 42dc975fa..9fb1011ee 100644 --- 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& prp : d_pendingReqPhase) -- 2.30.2