projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: fb7cc27) | patch
Only consider relevant terms in the array-inspired sequence solver (#8105)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Wed, 16 Feb 2022 00:59:33 +0000 (18:59 -0600)
committerGitHub <noreply@github.com>
Wed, 16 Feb 2022 00:59:33 +0000 (00:59 +0000)
commita657bb589acc5b994b911e6f48b413e85aee6bc1
treeb4daec5f1b057d091767ac1ca74648c7b3d06dc3tree
parentfb7cc27d4ae39d224c739c912ccd76563f374999commit | diff
Only consider relevant terms in the array-inspired sequence solver (#8105)

Avoids segfault in model construction due to asking for the value of irrelevant (non-shared) term.
src/theory/strings/array_solver.cpp diff | blob | history
src/theory/strings/array_solver.h diff | blob | history
src/theory/strings/term_registry.cpp diff | blob | history
src/theory/strings/term_registry.h diff | blob | history
src/theory/strings/theory_strings.cpp diff | blob | history
test/regress/CMakeLists.txt diff | blob | history
test/regress/regress0/seq/shared-term-registration.smt2 [new file with mode: 0644] blob