projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 2493601) | patch
Fix collect model info for higher-order (#3409)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Sun, 27 Oct 2019 22:47:56 +0000 (17:47 -0500)
committerAndres Noetzli <andres.noetzli@gmail.com>
Sun, 27 Oct 2019 22:47:56 +0000 (15:47 -0700)
commit3af2dfea22aae0d527fcfa93600c451b323c15b7
tree046c84f5f05ca2900d1e8484a45fbf1cba7b91cbtree
parent24936010e7d0dc644bd2bf1f533ac0abee678f6bcommit | diff
Fix collect model info for higher-order (#3409)

This ensures we add lemmas when collect model info fails for the higher order extension of UF. This fixes #3405 (that benchmark now answers unknown).
src/theory/theory_model_builder.cpp diff | blob | history
src/theory/uf/ho_extension.cpp diff | blob | history
src/theory/uf/theory_uf.cpp diff | blob | history