projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: d64143f) | patch
Strings: Register skolems before sending lemma (#4381)
authorAndres Noetzli <andres.noetzli@gmail.com>
Thu, 23 Apr 2020 00:55:33 +0000 (17:55 -0700)
committerGitHub <noreply@github.com>
Thu, 23 Apr 2020 00:55:33 +0000 (19:55 -0500)
commit855143cfa1e4cf38f67ff99eba5d59e5a2786120
tree4e955b1cd63826fd1f8334f1566e6546dd7363b2tree
parentd64143f8aec229a673db1ec7b38d94890134d3f5commit | diff
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 diff | blob | history