Add TODO about duplicate precondition_loop_invariant entries

goblint · Feb 29, 2024 · 786affd · 786affd
1 parent 61f94d0
commit 786affd
Showing 1 changed file with 2 additions and 0 deletions.
diff --git 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`.