% TESTED FEATURES: Horn Clauses
% EXPECTED OUTCOME: Unsafe
specification Horn_Unsafe
channel_model CCM
entity Environment
{
  symbols
    a(nat) : fact;
    b(nat,nat) : fact;
  clauses
   %h2     : forall N. b(N,0)   :- a(N);  % would be flagged as an error
   %h3(N)  : forall M. b(N,0)   :- a(N);  % would be flagged as an error
   %h4     : forall N. b(0,0)   :- a(N);  % would be flagged as an error
   %h5(N,M):           b(N,0)   :- a(N);  % would be flagged as an error
    h(N)   : forall M. b(N,M) :- a(N); %% OFMC cannot handle this universal quantification
% misleading error message: ofmc-core: The Hornclauses may have run into a non-termination---giving up.
  body
       a(0);
  goals
    trouble: %         !b(0,1) & 
             %[](forall Y . b(0,Y));
             [](!exists Y. b(0,Y));
}