Incorrect translation of choice rule with multiple elements #13

New Issue

patrick · 2018-04-21T19:20:08+02:00

patrick commented

2018-04-21 19:20:08 +02:00

anthem produces an incorrect result for the rule:

{p(a); p(b)}.

instead if saying that such rules are not supported.

anthem produces an incorrect result for the rule: {p(a); p(b)}. instead if saying that such rules are not supported.

patrick self-assigned this 2018-04-21 19:20:08 +02:00

patrick added the

bug

label 2018-04-21 19:20:08 +02:00

patrick changed title from ~~Incorrect translation~~ to Incorrect translation of choice rule with multiple elements

2018-04-21 19:20:24 +02:00

patrick added this to the anthem 0.1.9 milestone 2018-04-22 13:34:38 +02:00

patrick commented

2018-05-02 17:46:44 +02:00

In fact, the following output is generated:

forall V1 (p(V1) <-> ((V1 = a and V2 = b and p(V1)) or ( = a and V1 = b and p(V1))))

There seems to be a problem with a variable declaration in the ( = a and ... part.

I’m not sure whether this is the same or a separate issue.

In fact, the following output is generated: forall V1 (p(V1) <-> ((V1 = a and V2 = b and p(V1)) or ( = a and V1 = b and p(V1)))) There seems to be a problem with a variable declaration in the `( = a and ...` part. I’m not sure whether this is the same or a separate issue.

patrick commented

2018-05-04 15:22:03 +02:00

Fixed by e85807accb.

Fixed by e85807accbc676c7e1ffc3b4f8157f69dcb89133.

patrick closed this issue

2018-05-04 15:22:03 +02:00

Sign in to join this conversation.