New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Warnings on `tests/everything/f1.ae` #1287

Open

Halbaroth opened this issue Feb 6, 2025 · 0 comments

Labels

frontend low-priority

Collaborator

Halbaroth commented Feb 6, 2025

We got the following warnings while running alt-ergo tests/everything/f1.ae:

[Warning] (sub) axiom #append_def#sub-1 replaced with #append_def#sub-1
[Warning] (sub) axiom #append_def#sub-1 replaced with #append_def#sub-1
[Warning] (sub) axiom #append_def#sub-1 replaced with #append_def#sub-1
[Warning] (sub) axiom #append_def#sub-1 replaced with #append_def#sub-1
[Warning] (sub) axiom #append_def#sub-1 replaced with #append_def#sub-1

A minimal example:

logic h : int, int -> int

axiom a :
  forall x:int [true].
  forall y:int.
  h(x, y) < 0

goal g : forall x:int. forall y:int. h(x, y) >= 0

The user-defined trigger seems to be important to trigger the warning.

The text was updated successfully, but these errors were encountered:

Halbaroth added frontend low-priority labels

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment