From 786affd4a0135df7a3221b31ceafed1f3fc8f12b Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Thu, 29 Feb 2024 17:24:37 +0200 Subject: [PATCH] Add TODO about duplicate precondition_loop_invariant entries --- tests/regression/56-witness/05-prec-problem.t | 2 ++ 1 file changed, 2 insertions(+) diff --git a/tests/regression/56-witness/05-prec-problem.t b/tests/regression/56-witness/05-prec-problem.t index 25a3fc619f..4c7dd02fa9 100644 --- a/tests/regression/56-witness/05-prec-problem.t +++ b/tests/regression/56-witness/05-prec-problem.t @@ -8,6 +8,8 @@ [Info][Witness] witness generation summary: total generation entries: 6 +TODO: Don't generate duplicate entries from each context: should have generated just 3. + Witness shouldn't contain two unsound precondition_loop_invariant-s with precondition `*ptr1 == 5 && *ptr2 == 5`, and separately invariants `result == 0` and `result == 1`. The sound invariant is `result == 1 || result == 0`.