Unexpected assertion failure when using --setAxiomatizationFile without axioms and variables
dnezam opened this issue · 0 comments
dnezam commented
This issue is similar to #777 with the main difference being that we assign the result to a variable first.
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() {
var empty: Set[Int]
empty := EmptySet()
assert empty == 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
}