Term gen not generating terms/unable to prove quantified assumption

[siddharth-krishna]

Example that cannot be proven:

struct Node {}

datatype Interface =
  int(inf: Map<Node, FlowDom>,
      dom: Set<Node>,
      fm: Map<Node, Map<Node, FlowDom>>)

datatype FlowDom = fd(pc: Int);

pure predicate fdEq(p1: FlowDom, p2:FlowDom) { p1.pc == p2.pc }

procedure test(hd: Node, I: Interface)
  requires (forall y: Node ::
    !(y in dom(I)) ==> fdEq(I.fm[hd][y], fd(0)))
  ensures (forall y: Node ::
    !(y in dom(I)) ==> fdEq(I.fm[hd][y], fd(0)))
{}

A term generator for fdEq(..) -> known(fdEq(..)) is automatically added (but why?), but it appears not to generate the needed known term.

[siddharth-krishna]

A related issue: here's an example where we don't have a known term for an fdLeq term that comes from an instantiation of a quantifier.

struct Node {
  var intf: Interface
}

datatype Interface =
  int(inf: Map<Node, FlowDom>,
      dom: Set<Node>,
      fm: Map<Node, Map<Node, FlowDom>>)

datatype FlowDom = fd(pc: Int);

pure predicate fdLeq(p1: FlowDom, p2:FlowDom) { p1.pc <= p2.pc }

procedure test(hd: Node, I: Interface, x: Node, X: Set<Node>)
  requires x in X
{
  pure assume forall x: Node ::
    x in X ==> fdLeq(I.inf[x], x.intf.inf[x]);

  pure assert fdLeq(I.inf[x], x.intf.inf[x]);
}

Even adding the following term gen to the pure assume statement doesn't help:

@(matching fdLeq(I.inf[x], x.intf.inf[x]) yields known(fdLeq(I.inf[x], x.intf.inf[x])))

Worryingly, that term gen ends up using different versions of the variable x in the pre-instantiation VC:

(forall x^5: Loc<Node> ::
   (fdLeq(I.inf[x^5], x^5.intf.inf[x^5])) ||
   (x^5 !in X)
 @(matching fdLeq(I.inf[x^4], x^4.intf.inf[x^4]) without intf and x^4 without
    null yields known(fdLeq(I.inf[x^4], x^4.intf.inf[x^4]))))

[wies]

You need to run it with option -abspreds, otherwise the negated ground occurrences of predicates are going to be expanded in the VC (without keeping the original predicate instance around). I'll keep the issue open since this should be cleaned up at some point.

[siddharth-krishna]

Ah yes, sorry I forgot about that option. Thanks!