projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 4df14f1) | patch
Fix term registry for constant case, simplify. (#4538)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Thu, 28 May 2020 20:05:06 +0000 (15:05 -0500)
committerGitHub <noreply@github.com>
Thu, 28 May 2020 20:05:06 +0000 (15:05 -0500)
commitda165b9cbee366d4e77716617f2e2c794da9bd46
tree05535894356ff2d2c5bae66e6da6ab5a85b9e6f1tree
parent4df14f1e09549be607123c66b7dd206e8e244c89commit | diff
Fix term registry for constant case, simplify. (#4538)

We were getting an assertion failure (causing nightlies to fail) due to the recent optimization to the strings skolem cache (978f455). This ensures we ignore constant strings in TermRegistry::getRegisterTermAtomicLemma.

It also removes a deprecated option that is deleted in the proof-new branch.
src/options/strings_options.toml diff | blob | history
src/theory/strings/term_registry.cpp diff | blob | history