viperproject/silicon

Difficulty proving sequence inequality

bobismijnnaam opened this issue · 1 comments

bobismijnnaam commented

Silicon has a hard time proving inequality of two sequences:

method m() {
	// assert Seq(1)[0] != Seq(2)[0]
	assert Seq(1) != Seq(2)
}

If the first assert is uncommented, the second assert verifies. Carbon does verify the second assert, without the first. The silicon version used is: Silicon 1.1-SNAPSHOT (60494602@(detached)). Is this some trigger/axiom incompleteness?