Unexpected assertion failure when using --setAxiomatizationFile without axioms
dnezam opened this issue · 0 comments
dnezam commented
Silicon fails to verify fail.vpr when passing a custom set axiomatization file without axioms to it. Uncommenting the body makes verification go through.
Command: run --setAxiomatizationFile sets.vpr fail.vpr
fail.vpr:
function EmptySet(): Set[Int]
ensures result == Set[Int]()
//{
// Set[Int]()
//}
method main() {
assert EmptySet() == Set[Int]()
}
sets.vpr:
domain $Set[E] {
function Set_in(e: E, s: $Set[E]): Bool
function Set_card(s: $Set[E]): Int
function Set_empty(): $Set[E]
function Set_singleton(e: E): $Set[E]
function Set_unionone(s: $Set[E], e: E): $Set[E]
function Set_union(s1: $Set[E], s2: $Set[E]): $Set[E]
function Set_disjoint(s1: $Set[E], s2: $Set[E]): Bool
function Set_difference(s1: $Set[E], s2: $Set[E]): $Set[E]
function Set_intersection(s1: $Set[E], s2: $Set[E]): $Set[E]
function Set_subset(s1: $Set[E], s2: $Set[E]): Bool
function Set_equal(s1: $Set[E], s2: $Set[E]): Bool
}