-
Notifications
You must be signed in to change notification settings - Fork 1.5k
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
Invalid model for string index when symbolic string is not contained in the other string #875
Comments
If I add an extra line that constrains c2 to be greater than or equal to zero:
Then Z3 times out. (Maybe that is just generally a hard query, though.) |
NikolajBjorner
added a commit
that referenced
this issue
Jan 26, 2017
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
My axiomatization had some things left to be desired. Perhaps still have, but it now addresses the issues you report. |
this is fixed. |
nunoplopes
added a commit
that referenced
this issue
Jan 3, 2023
hgvk94
pushed a commit
to hgvk94/z3
that referenced
this issue
Mar 27, 2023
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Hi again, I have another invalid model with strings. Here I am checking that whenever one string does not contain the other, there is no index at which the other string appears as a substring of the first string:
Z3 returns a negative index, then recognizes that it is an invalid model:
I know that str.at is undefined with negative offset -- here it looks like Z3 is generating a negative offset for string.index. Is this defined? The line that fails with that model is:
Should I be constraining c2 to always be greater than or equal to zero myself?
Thanks again!
Talia
The text was updated successfully, but these errors were encountered: