Termination axioms not instantiated for all necessary sorts

[mschwerhoff]

Silicon fails to verify the following program:

import <decreases/set.vpr>

method test() {
  var c: Set[Ref]

  while (c != Set[Ref]())
    decreases c
  {
    var n: Ref
    assume n in c
    c := c setminus Set(n)
  }
}

The program above is basically transformed into:

domain WellFoundedOrder[T] {
  function decreasing(arg1: T, arg2: T): Bool
  function bounded(arg1: T): Bool
}

domain SetWellFoundedOrder[S] {
  axiom set_ax_dec {
    forall set1: Set[S], set2: Set[S] ::
        { decreasing(set1, set2) }
      |set1| < |set2| ==> decreasing(set1, set2)
  }

  axiom set_ax_bound {
    forall set1: Set[S] :: { bounded(set1) } bounded(set1)
  }
}

method mark() {
  var c: Set[Ref]

  // decreases c
  while (c != Set[Ref]()) {
    var old_W1_T0: Set[Ref]
    old_W1_T0 := c

    var n: Ref
    inhale n in c
    c := c setminus Set(n)

    if (true && c != Set[Ref]()) {
      assert decreasing(c, old_W1_T0) && bounded(old_W1_T0) // FAILS
      // assert |c| < |old_W1_T0| // HOLDS
    }
  }
}

Inspecting the SMT encoding reveals that the axioms from domain SetWellFoundedOrder are instantiated for S being int, but not Ref. That looks like a problem caused by the code for computing necessary domain instantiations.

[marcoeilers]

Fixed in viperproject/silver#742.