Problem with inequality of sequences

[PBHTasche]

Silicon seems to not be able to prove inequality of sequences if the first elements are equal. If I first reason about the elements individually, then the reasoning about the sequences passes as well. This is similar to issue #601, but still seems to be a problem. Like with that issue, Carbon does verify the example.

// This passes
method test_seq_unequal()
{
  assert Seq(false, false) != Seq(true, true)
}

// This fails
method test_seq_semiequal()
{
  assert Seq(true, false) != Seq(true, true)
}

// This passes
method test_seq_elemwise()
{
  var s1: Seq[Bool] := Seq(true, true)
  var s2: Seq[Bool] := Seq(true, false)

  assert s1[0] != s2[0] || s1[1] != s2[1]
  assert s1 != s2
}

The Silicon version I use is Silicon 1.1-SNAPSHOT (4c705143).

Update: From what we can tell, it seems to be an issue with the axiomatisation of sequence equality, specifically the triggers in the extensional_seq_equality axiom. Accessing the unequal item in one of the sequences allows verification to pass:

// This passes
method test_seq_semiequal()
{
  var b: Bool
  b := Seq(true, false)[1]
  assert Seq(true, false) != Seq(true, true)
}

[mschwerhoff]

I won't have time to look at this any time soon. If you can see a difference between the axiom triggers used by Carbon and Silicon, you could adjust the latter to see if this resolves the incompleteness. I would be much obliged :-)

[marcoeilers]

This example verifies since we integrated Carbon's sequence axiomatization into Silicon (PR #642).