Bug2 in Recursive Symbolic Constraints

[VeraZhang0311]

I tested Formula to find a solution with 3 cycles:

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(_, _)}) > 3. 
  conforms enoughEdges.

  enoughCycles :- count({ c | c is cycle(_)}) = 3.
  conforms enoughCycles.
}

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

The (incorrect) solution to the partial model is:

Node(7)
Node(8)
Node(9)
Edge(7, 7)
Edge(8, 8)
Edge(8, 7)
Edge(9, 7)

which shouldn't have a cycle(9) but Formula indicates it does.

[balasub]

Potential fix in e67da65. Needs testing. Note that setting [solver_RecursionBound = 10] is probably a bit high. It's faster to test with [solver_RecursionBound = 5].