projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: a7aba0c) | patch
Fix related to preregistering boolean term variables in strings (#5331)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Fri, 23 Oct 2020 18:03:17 +0000 (13:03 -0500)
committerGitHub <noreply@github.com>
Fri, 23 Oct 2020 18:03:17 +0000 (13:03 -0500)
commitf66e1fc33ee7549c90eabc808be5a6ef6196aaa0
treec099d4ae91b82b182adbedfc2201a25188e9ddfctree
parenta7aba0c8580d5153fee99b4d59345e33c39c893bcommit | diff
Fix related to preregistering boolean term variables in strings (#5331)

We should only add trigger predicates for string predicates, and not arbitrary Boolean terms (which can now occur since we are handling parametric sequences).

This avoids a debug assertion failure reported on as a followup to #4370. In that benchmark BOOLEAN_TERM_VARIABLE was being added as a trigger predicate.
src/theory/strings/term_registry.cpp diff | blob | history
src/theory/uf/equality_engine.cpp diff | blob | history
test/regress/CMakeLists.txt diff | blob | history
test/regress/regress0/seq/issue4370-bool-terms.smt2 [new file with mode: 0644] blob