diff options
Diffstat (limited to 'src/theory/strings/inference_manager.cpp')
| -rw-r--r-- | src/theory/strings/inference_manager.cpp | 3 |
1 files changed, 2 insertions, 1 deletions
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<const Node, bool>& prp : d_pendingReqPhase) |