Carbon axiomatization of Map is better than Silicon

[tillarnold]

method test(m: Map[Int,Int])
    requires(range(m) == domain(m))
{
    assume forall i: Int, j: Int :: i in m && j in m ==> (i != j ==> (m[i] != m[j]))
    assert forall i: Int, j: Int :: i in m && j in m ==> (i != j ==> (m[i] != m[j]))
}

Fails to verify in Silicon but works fine in Carbon, removing the precondition makes it work also in Silicon. We were unable to find a combination of triggers to make it work in Silicon.

---

@marcoeilers remarked about this on zulip that

Silicon essentially runs into Z3 non-termination here after assuming i in m && j in m when evaluating the quantifier body. That step just doesn't happen in Carbon in the same way. So I think it's more likely that the map axiomatization of both has an issue that only shows up in Silicon here. This program essentially illustrates the step, and if you give this to Carbon, it also needs ca. 3 seconds to report an error, which is longer than it should, so there is likely a problem here:

method test(m: Map[Int,Int])
    requires(range(m) == domain(m))
{
    assume forall i: Int, j: Int :: {m[i], m[j]} i in m && j in m ==> (i != j ==> (m[i] != m[j]))
    var ip: Int
    var jp: Int

    assume ip in m && jp in m
    assert false
}