Open
Description
With the "classic" heuristic, this works. Now, with the new default, it fails (with an exception about missing cases):
val foo_def = Define`
(foo 0 0 0 = 0) /\ (foo 0 0 1 = 1) /\ (foo 0 1 0 = 1) /\ (foo 0 1 1 = 0) /\
(foo 1 0 0 = 0) /\ (foo 1 0 1 = 1) /\ (foo 1 1 0 = 0) /\ (foo 1 1 1 = 0)`;
Thanks to Joseph Chan for the bug report.