Bug in recursive symbolic constraints

[balasub]

The example below demonstrates a bug in how constraints are generated with recursive rules.

domain Graph
{
  Node ::= new (id: Integer).
  Edge ::= new (src: Integer, dst: Integer).

  edgeHasSrc ::= (src: Integer).
  edgeHasDst ::= (dst: Integer).

  path ::= (Integer, Integer).
  cycle ::= (Integer).

  badSrc ::= (src: Integer).
  badDst ::= (dst: Integer).

  edgeHasSrc(a) :- Edge(a, b), Node(a).
  edgeHasDst(b) :- Edge(a, b), Node(b).

  badSrc(a) :- Edge(a, b), no edgeHasSrc(a).
  badDst(b) :- Edge(a, b), no edgeHasDst(b).

  path(a, b) :- Edge(a, b).
  path(a, c) :- path(a, b), path(b, c).
  cycle(a) :- path(a, a).

  conforms no badSrc(_).
  conforms no badDst(_).

  enoughNodes :- count({ n | n is Node(_)}) > 1. 
  conforms enoughNodes.

  enoughEdges :- count({ e | e is Edge(_, _)}) = 1. 
  conforms enoughEdges.

  conforms cycle(x).
}

partial model pm of Graph
[solver_RecursionBound = 5]
{
  Node(t).
  Node(u).
  Node(v).
  Edge(l, m).
  Edge(n, o).
  Edge(p, q).
  Edge(r, s).
}

The (incorrect) solution returned is the following:

Node(6)
Node(5)
Edge(5, 6)

The bug is potentially related to the rule:

cycle(a) :- path(a, a).

where perhaps equality constraints are not correctly asserted across the first and second parameters to path.

[balasub]

Potential fix in e67da6595bc3d7d593d2de5891bffb416e8c52ea. Needs testing.