-
Notifications
You must be signed in to change notification settings - Fork 4
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
Symbooglix missing a bug #31
Comments
That is because symbooglix is timing out. Symbooglix is not claiming the program is bug free.
It looks that way. Symbooglix gets stuck in the implementation of If I use a very recent build of Z3, Symbooglix eventually gives up because Z3 returns unknown (due to the default 120 second query timeout per call) while trying to check one of the calls to
It is very likely that the problem here is the use of quantifiers. Attached is a log of the queries Symbooglix issued to Z3 |
Ok, I attempted to reproduce this, and here is what I get. The end of the output I get from symbooglix is as follows:
What does that actually mean? |
That's not what it means.
A speculative path is a path that Symbooglix could not prove is feasible. A path becomes "speculative" in Symbooglix at branch points ( The current implementation of Symbooglix immediately terminates paths marked as "speculative". So having speculative paths implies path exploration might be non-exhaustive. Therefore if
then we cannot conclude the program is bug free. |
It would be useful to have a more human-friendly message here, essentially informing users that paths, and thus bugs, might have been missed. |
@delcypher : Ok, got it, this makes sense now. Btw, could you send me the query on which Z3 times out? I am having trouble isolating it from the txt file you attached. Thx. |
We identified this as an example that it seems causes for Symbooglix to miss a bug:
array2_free_fail.zip
No bugs are reported when Symbooglix is executed on this bpl file like this:
On the other hand, Corral does report a bug as expected:
This is a fairly simple example, and I do have to wonder if this problem is due to our usage of quantifiers.
The text was updated successfully, but these errors were encountered: