sig bad.
kind i type.
type a,b1,b2,c i.
type p i -> i -> o.
----
module bad.
%:pab1:
p a b1.
%:pb2c:
p b2 c.
%:trans:
p X Z :- p X Y, p Y Z.
----
Specification "bad".
Theorem foo : {p a c}.
unfold trans. search. search.
The issue is that after the unfold we get two subgoals, one with {p a ?1} and the other with {p ?1 c}. Since logic variables in different subgoals have nothing to do with each other, each subgoal is individually proved.
The expected result of the unfold is exists L, {p a L} /\ {p L c}.
Consider this input:
The issue is that after the
unfoldwe get two subgoals, one with{p a ?1}and the other with{p ?1 c}. Since logic variables in different subgoals have nothing to do with each other, each subgoal is individually proved.The expected result of the
unfoldisexists L, {p a L} /\ {p L c}.This bug is reported by Claudio Sacerdoti Coen.