-
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
Soundness bug in QF_S with str.indexof #4036
Comments
NikolajBjorner
added a commit
to NikolajBjorner/z3
that referenced
this issue
Apr 22, 2020
NikolajBjorner
added a commit
that referenced
this issue
Apr 22, 2020
* na Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * fix #4037 * nicer output for skolem functions * more overhaul of seq, some bug fixes * na * added offset_eq file * na * fix #4044 * fix #4040 * fix #4045 * updated ignore * new rewrites for indexof based on #4036 * add shortcuts * updated ne solver for seq, fix #4025 * use pair vectors for equalities that are reduced by seq_rewriter * use erase_and_swap * remove unit-walk * na * add check for #3200 * nits Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * name a type Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * remove fp check Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * remove unsound axiom instantiation for non-contains Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * fix rewrites Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * fix #4053 Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * fix #4052 Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
fixed. |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
OS: Ubuntu 18.04
Commit: dd064a5
The text was updated successfully, but these errors were encountered: