Skip to content

Issues: prove-rs/z3.rs

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

44 Open 66 Closed
44 Open 66 Closed
Author
Filter by author
Loading
Label
Filter by label
Loading
Use alt + click/return to exclude labels
or ⇧ + click/return for logical OR
Projects
Filter by project
Loading
Milestones
Filter by milestone
Loading
Assignee
Filter by who’s assigned
Sort
Sort by
Newest Oldest Most commented Least commented Recently updated Least recently updated Best match
Most reactions
👍 👎 😄 🎉 😕 ❤️ 🚀 👀

Issues list

Unexpected behavior when trying to minimize bitvector
#331 opened Dec 17, 2024 by danielrainer
Missing Exposure of Z3_context and Z3_sort in Recent Z3 Crate Versions
#327 opened Nov 29, 2024 by zhristophe
1
High-level bindings to create quantifiers with additional attributes
#325 opened Nov 28, 2024 by ole-thoeb
function set_global_param() could panick without pre-checking
#317 opened Oct 16, 2024 by cicilzx
Null pointers (and then UB) when creating two Sorts with the same name
#313 opened Oct 2, 2024 by shelvacu
Add consequences to solver
#302 opened Jul 17, 2024 by VadeveSi
New release
#294 opened May 21, 2024 by toolCHAINZ
14
Float binding issues
#291 opened May 5, 2024 by Dessix
5 tasks
1
About arrays equal
#288 opened Apr 1, 2024 by carbonium14
1
Build failure on Mac
#286 opened Mar 21, 2024 by GuanmingQiao
2
Max-SMT problem
#284 opened Feb 29, 2024 by FoxMakarov
5
Where are the examples
#282 opened Dec 24, 2023 by kallehed
1
About solver speed
#278 opened Nov 27, 2023 by carbonium14
2
get_unsat_core for Optimize
#268 opened Nov 4, 2023 by poscat0x04
5
Mark self as mut borrow in solver methods?
#266 opened Nov 2, 2023 by 108anup
4
[Help Wanted] Why incremental mode does not keep num of decisions down in this case?
#265 opened Nov 2, 2023 by aur3l14no
About Array
#263 opened Oct 29, 2023 by FoxMakarov
3
Use an "implicit" Context?
#261 opened Oct 26, 2023 by waywardmonkeys
Use logical shift right for BV '>>' operator
#243 opened Jul 18, 2023 by JPaja
2
Exposing application parameters
#238 opened May 2, 2023 by dp1
1
Symbol::as_z3_symbol can return Null Pointer
#235 opened Apr 12, 2023 by Pat-Lafon
1
Use NonNull in Z3 safe bindings
#227 opened Mar 13, 2023 by Pat-Lafon
1
Fails to Build in Linux
#224 opened Mar 2, 2023 by Wright4TheJob
6
Iterator for a solver
#221 opened Feb 12, 2023 by onthestairs
1
model value extraction
#219 opened Dec 21, 2022 by AdamGlass
3
ProTip! Find all open issues with in progress development work with linked:pr.