Skip to content
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.

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

Hash_table_eq2 on --vac mode takes long (forever?) to execute. #122

Open
achenchen1 opened this issue Dec 11, 2021 · 2 comments
Open

Hash_table_eq2 on --vac mode takes long (forever?) to execute. #122

achenchen1 opened this issue Dec 11, 2021 · 2 comments

Comments

@achenchen1
Copy link

achenchen1 commented Dec 11, 2021

Related to PR #121.

Running on --vac seems to loop on the following two lines:

Info: vacuity passed (sat) seahorn/lib/utils.c:107]
Info: assertion passed (unsat) seahorn/lib/utils.c:107]
Info: vacuity passed (sat) seahorn/lib/utils.c:108]
Info: assertion passed (unsat) seahorn/lib/utils.c:108]
@achenchen1
Copy link
Author

Some relevant insight from Liam Metke:

I don't think it's endless, it's just that it takes a really long time. It seems to be calling nondet_compare from utils.c to compare elements from each hash table, but the number of elements is capped to be 8 in the tables (I think, I'm just going off a line from the CMakeLists.txt file). So it probably would return given enough time, but it seems like it chews up memory so it gets slower as it runs. I think you should probably leave this until we can get input from @siddharth because the hash_table_eq job from the jobs directory suffers from the same problem when run in --vac mode, so I feel like it's a problem with something from the hash_table testing suite and doesn't really have anything to do with the sea_tracking stuff.

@priyasiddharth
Copy link
Collaborator

On my machine
>time ./verify --vac seahorn/jobs2/hash_table_eq2/

real 109m5.066s
user 109m1.671s
sys 0m2.418s

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

2 participants