projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: b536a5f) | patch
(proof-new) Separating optimizations for strings skolem caching (#6064)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Mon, 8 Mar 2021 17:32:43 +0000 (11:32 -0600)
committerGitHub <noreply@github.com>
Mon, 8 Mar 2021 17:32:43 +0000 (17:32 +0000)
commit4395b6d728d2a25bff3a56801f7218d79834f423
tree09effe93f7cc5d115b4975692bc2bd450d7ca073tree
parentb536a5fefb654439d6a0dee65b91ece12419fc0bcommit | diff
(proof-new) Separating optimizations for strings skolem caching (#6064)

This PR ensures that several optimizations are not performed in the reference implementation of skolem sharing (d_useOpts=false). This is to ensure that the many of the rules in the strings proof checker do not depend on the rewriter.

These errors were caught by the LFSC proof checker.
src/theory/strings/skolem_cache.cpp diff | blob | history
src/theory/strings/theory_strings_preprocess.cpp diff | blob | history