Fix test_predtest's idea of what weak refutation means. I'd initially supposed that predicate_refuted_by(..., true) ought to say that "A refutes B" means "non-falsity of A implies non-truth of B". But it seems better to define it as "truth of A implies non-truth of B". This is more useful in the current system, slightly easier to prove, and in closer correspondence to the existing code behavior.
With this change, test_predtest no longer claims that any existing test cases show false proof reports, though there still are cases where we could prove something and fail to. Discussion: https://postgr.es/m/5983.1520487...@sss.pgh.pa.us Branch ------ master Details ------- https://git.postgresql.org/pg/commitdiff/a63c3274a68832182f84ca5d2b8cc5a7462bdacb Modified Files -------------- src/test/modules/test_predtest/expected/test_predtest.out | 12 +++++------- src/test/modules/test_predtest/test_predtest.c | 8 ++++++-- 2 files changed, 11 insertions(+), 9 deletions(-)
