projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: f12af39) | patch
Fix model construction for higher order involving irrelevant function terms (#7526)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Fri, 29 Oct 2021 17:50:59 +0000 (12:50 -0500)
committerGitHub <noreply@github.com>
Fri, 29 Oct 2021 17:50:59 +0000 (17:50 +0000)
commitd7bcc389882cd6e13e9d330c57640d50f4d90d45
treeb59586a60ac3165eef5961f88a4173c539609b8ctree
parentf12af39c6ac5f19913b9e9996eb9453eb7b30034commit | diff
Fix model construction for higher order involving irrelevant function terms (#7526)

This fixes a bug in HO model construction where we were communicating information about irrelevant function terms to the model, leading to incorrect models.
src/theory/uf/ho_extension.cpp diff | blob | history
test/regress/CMakeLists.txt diff | blob | history
test/regress/regress0/ho/qgu-fuzz-ho-2-dd-no-ext.smt2 [new file with mode: 0644] blob