Unexpected assertion failure when using --setAxiomatizationFile without axioms and variables

[dnezam]

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
}