projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 8e21ca2) | patch
Disable fact vs lemma optimization in datatypes for now (#5521)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Thu, 26 Nov 2020 02:37:23 +0000 (20:37 -0600)
committerGitHub <noreply@github.com>
Thu, 26 Nov 2020 02:37:23 +0000 (20:37 -0600)
commit084518db641e0648164bbe4461cd98b10e937dc0
treec229d107f9ccc0b6188b9114ddf834cb20e2f8d4tree
parent8e21ca2de274f82ded4429d21a34741fc1501b1bcommit | diff
Disable fact vs lemma optimization in datatypes for now (#5521)

This optimization needs more work to determine its correctness. It is currently leading to incorrect candidate models on Facebook benchmarks.
src/theory/datatypes/theory_datatypes.cpp diff | blob | history
test/regress/CMakeLists.txt diff | blob | history