Unsound axiom not considered when domain not used
bruggerl opened this issue · 1 comments
bruggerl commented
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 commented
I don't have a strong opinion, but we should be careful not to let such corner cases prevent (in general important) optimisations.