Unsound axiom not considered when domain not used

[bruggerl]

This should successfully verify (in Carbon, it does), but verification fails:

domain Foo {
  axiom unsound {
    false
  }
}

method test()
{
  assert false
}

Silicon reports that the assertion might not hold.

When declaring a variable of type Foo in the method test, verification succeeds:

domain Foo {
  axiom unsound {
    false
  }
}

method test()
{
  var x: Foo
  assert false
}

[mschwerhoff]

I don't have a strong opinion, but we should be careful not to let such corner cases prevent (in general important) optimisations.