projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 3d49a44) | patch
Ensure uninterpreted sort owner is UF if uf-ho or finite-model-find is enabled. ...
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Mon, 12 Oct 2020 13:33:32 +0000 (08:33 -0500)
committerGitHub <noreply@github.com>
Mon, 12 Oct 2020 13:33:32 +0000 (08:33 -0500)
commite93c443a0bfb1a66909e8467b24da399be3d01ac
treeabe0e2d365f01541f32835d44e68ce0a9dde79f3tree
parent3d49a4413c819f6dee337ac7c53b6f6c6b510377commit | diff
Ensure uninterpreted sort owner is UF if uf-ho or finite-model-find is enabled. (#5248)

This ensures that arrays is not the owner of uninterpreted sorts if uf-ho or finite-model-find are enabled. In these cases, the UF solver implements special techniques (cardinality, ho reasoning) that should take priority.

Fixes #5233.
src/smt/set_defaults.cpp diff | blob | history
test/regress/CMakeLists.txt diff | blob | history
test/regress/regress0/ho/issue5233-part1-usort-owner.smt2 [new file with mode: 0644] blob