projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 79fb4d7) | patch
Check for higher-order variables in TheoryUF::ppRewrite (#7408)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Wed, 20 Oct 2021 22:01:01 +0000 (17:01 -0500)
committerGitHub <noreply@github.com>
Wed, 20 Oct 2021 22:01:01 +0000 (22:01 +0000)
commit57f8d6c04430277abdb98916b8ac407930abd215
tree085a7f4493cec54c12c685de46eeb6fb503284bctree
parent79fb4d7cb03b5fe254fb0c43f5dc6e885cfbf013commit | diff
Check for higher-order variables in TheoryUF::ppRewrite (#7408)

Fixes #7000. That sequence of API calls now throws a logic exception.
src/theory/uf/ho_extension.cpp diff | blob | history
src/theory/uf/theory_uf.cpp diff | blob | history
test/unit/api/solver_black.cpp diff | blob | history