`disjoint_witness_equalities` does not ensure disjoint lists

[mark-moir]

Hi

There is a bug in disjoint_witness_equalities, which results in not ensuring disjoint lists. The problem is that, when merging current with an overlapping list here, this may introduce a transitive equality with a list that we've already skipped and not merged.

The result is that verify fails, even though the given witnesses do meet all requirements.

A simple solution is to run the algorithm repeatedly until the number of lists does not change.

I'm not in a position to make a pull request, I'm afraid, but I can offer the following to aid with reproducing and testing a fix.

        let input_eqs =
              vec![
                  vec![(0, 1), (2, 0)],
                  vec![(0, 5), (1, 2)],
                  vec![(0, 5), (3, 0)],
                  vec![(1, 3), (5, 0)],
                  vec![(1, 2), (4, 0)],
              ];

        let current_result =
              vec![
                  vec![(0, 1), (2, 0)],
                  vec![(1, 3), (5, 0)],
                  vec![(0, 5), (1, 2), (4, 0)],  // NOTE: (0,5) is in both of the last
                  vec![(0, 5), (3, 0)]           // two, so these are not disjoint
              ];

        let one_correct_result =
              vec![
                vec![(0, 1), (2, 0)],
                vec![(0, 5), (1, 2), (3, 0), (4, 0)],
                vec![(1, 3), (5, 0)]
            ];

        // This passes
        check!(input_eqs.clone(), current_result);

        // This fails
        check!(input_eqs, one_correct_result);

[lovesh]

Hi.

Thanks a lot for reporting it with an example. Will fix it soon.

[lovesh]

Hi. Fixed the issuer here. Thanks again for reporting it.

[mark-moir]

Thanks!