summaryrefslogtreecommitdiff
path: root/test/regress/regress0/fmf/bug-041417-set-options.cvc
blob: 16f59f78c71b968ea53ec41ae6da8319bbc5c83e (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
% EXPECT: invalid
OPTION "finite-model-find";
OPTION "fmf-fun";

DATATYPE
  Node = A | B
END;

link, reach: (Node,Node,INT) -> BOOLEAN;

ASSERT FORALL(x,y:Node, c:INT):
  link(x,y,c) => reach(x,y,c);

ASSERT link(A,B,1);

QUERY reach(A,B,5);
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback