projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 0029550) | patch
Fix datatypes compute ground value (#5671)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Tue, 15 Dec 2020 20:49:33 +0000 (14:49 -0600)
committerGitHub <noreply@github.com>
Tue, 15 Dec 2020 20:49:33 +0000 (14:49 -0600)
commit35f58d81fb57608d52884f560ff281fe52c7b18f
tree99eb88c7ae2b436272e079d23d55c8f59c5fd7d4tree
parent002955063ecf1b4b190717a7a0b2aec79ac7b6d9commit | diff
Fix datatypes compute ground value (#5671)

We were using the wrong cache on one call, leading to non-constant values being enumerated.

Fixes #5659, for that benchmark, CVC4 now answers "unknown".
src/expr/dtype.cpp diff | blob | history
src/expr/dtype_cons.cpp diff | blob | history
src/theory/type_enumerator.h diff | blob | history