projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 5e714e3) | patch
Make seq.nth a trigger kind (#5314)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Tue, 20 Oct 2020 16:58:37 +0000 (11:58 -0500)
committerGitHub <noreply@github.com>
Tue, 20 Oct 2020 16:58:37 +0000 (11:58 -0500)
commit0e6e153a78843b134d943f5d1ec33e254d0fb2fe
tree1c203b1d780b7a3592647960ba99333420d0258etree
parent5e714e365dbbd51bbf04305867c4bcdc3d5a4d83commit | diff
Make seq.nth a trigger kind (#5314)

This makes seq.nth a trigger kind, analogous to select in arrays.

This fixes a timeout in seq-unsolved-ematch.smt2, fixing the nightlies.
src/theory/quantifiers/ematching/trigger.cpp diff | blob | history
src/theory/quantifiers/term_database.cpp diff | blob | history