projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 3710728) | patch
Sort inference does not handle APPLY_UF when higher-order is enabled (#4138)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Sun, 22 Mar 2020 14:23:57 +0000 (09:23 -0500)
committerGitHub <noreply@github.com>
Sun, 22 Mar 2020 14:23:57 +0000 (09:23 -0500)
commitc98ba7775ecb8a192e2a93735885163234546be3
treefbfef218b03aeb1aa762da05785fe1d59ef43625tree
parent37107284adaad3d24da0ad15cac8c88af444aeefcommit | diff
Sort inference does not handle APPLY_UF when higher-order is enabled (#4138)

Fixes #4092 and fixes #4134.

Typically, APPLY_UF has special treatment in sort inference. It is significantly more complicated when higher-order logic is enabled. This disables special handling when ufHo() is enabled.
src/theory/sort_inference.cpp diff | blob | history
src/theory/sort_inference.h diff | blob | history
test/regress/CMakeLists.txt diff | blob | history
test/regress/regress1/ho/issue4092-sinf.smt2 [new file with mode: 0644] blob
test/regress/regress1/ho/issue4134-sinf.smt2 [new file with mode: 0644] blob