projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: bd0cf32) | patch
Set incomplete if not applying ho extensionality (#6281)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Wed, 7 Apr 2021 20:45:39 +0000 (15:45 -0500)
committerGitHub <noreply@github.com>
Wed, 7 Apr 2021 20:45:39 +0000 (20:45 +0000)
commit8f9f8a79a55a7c478f8d26894f4d2e7023c5a39c
tree8ccad126d323167ea5e6615f8163fa7998f19626tree
parentbd0cf32db7d115e52e243b165a26edb319e91316commit | diff
Set incomplete if not applying ho extensionality (#6281)

If the user manually disables ho-extensionality via expert option --no-uf-ho-ext, we should answer "unknown" instead of "sat" when applicable.

Fixes #4318.
src/theory/uf/ho_extension.cpp diff | blob | history