projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 971a6ac) | patch
Simplify and fix care graph for ufHo (#4924)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Fri, 21 Aug 2020 14:48:01 +0000 (09:48 -0500)
committerGitHub <noreply@github.com>
Fri, 21 Aug 2020 14:48:01 +0000 (09:48 -0500)
commit905dc2b51fd0145e0bb69a166c06a1731ef4c44b
tree715852790389f830365004bbf06e3528a4da5d1dtree
parent971a6ac1ccdeb52572565b6b47afedb9eccb7833commit | diff
Simplify and fix care graph for ufHo (#4924)

We now separate APPLY_UF and HO_APPLY. We do not generate care pairs based on comparing APPLY_UF terms with HO_APPLY terms, which led to type errors previously.

Fixes #4990.
src/theory/uf/theory_uf.cpp diff | blob | history
src/theory/uf/theory_uf.h diff | blob | history
test/regress/CMakeLists.txt diff | blob | history
test/regress/regress0/ho/issue4990-care-graph.smt2 [new file with mode: 0644] blob