issues
search
prove-rs
/
z3.rs
Rust bindings for the Z3 solver.
337
stars
105
forks
source link
issues
Newest
Newest
Most commented
Recently updated
Oldest
Least commented
Least recently updated
ci: Enable vcpkg build on macOS and Linux
#258
waywardmonkeys
closed
10 months ago
3
Can't link application that depends on z3-sys built with feature vcpkg on Linux
#257
hermanventer
closed
10 months ago
4
Always use `num`, remove `arbitrary-size-numeral` feature.
#256
waywardmonkeys
closed
10 months ago
1
Improve CI speed.
#255
waywardmonkeys
closed
10 months ago
0
ci: Run clippy on macOS against brew z3.
#254
waywardmonkeys
closed
10 months ago
0
z3: Update to Rust edition 2018. Collapse some imports.
#253
waywardmonkeys
closed
10 months ago
0
Implement `ast::Float::as_f64`
#252
waywardmonkeys
closed
10 months ago
4
Add vcpkg support and corresponding CI.
#251
TheVeryDarkness
closed
10 months ago
4
is_const_array and Distinct with &[impl Borrow<Self>]
#250
Pat-Lafon
closed
11 months ago
2
Use downloaded Z3 binary by default when `static-link-z3` flag is active
#249
yasuo-ozu
opened
1 year ago
8
Use system-shipped z3 libraries by pkg_config
#248
wtdcode
closed
9 months ago
10
Check Kind for optimize maximize
#247
Pat-Lafon
closed
1 year ago
0
Use Borrow in varop arrays
#246
Pat-Lafon
closed
1 year ago
0
z3 0.12.0 built failed on aarch64 musl
#245
Xuanwo
closed
1 year ago
3
ci: Add formatting check.
#244
waywardmonkeys
closed
1 year ago
0
Use logical shift right for BV '>>' operator
#243
JPaja
opened
1 year ago
2
Add bindings for global params
#242
Shatur
closed
1 year ago
12
New release?
#241
skyf0l
closed
1 year ago
2
Have Int::power return Real
#240
Pat-Lafon
closed
1 year ago
0
z3-sys: Fix return type of Z3_parse_smtlib2_string and Z3_parse_smtlib2_file
#239
dp1
closed
1 year ago
2
Exposing application parameters
#238
dp1
opened
1 year ago
1
future-incompatibilities raised by z3-sys
#237
Xuanwo
closed
1 year ago
5
Fix smt based tests
#236
Pat-Lafon
closed
1 year ago
1
Symbol::as_z3_symbol can return Null Pointer
#235
Pat-Lafon
opened
1 year ago
1
Aligning `apply` methods of FuncDecl and RecFuncDecl
#234
Pat-Lafon
closed
1 year ago
3
factor out get_assertions from Clone
#233
Pat-Lafon
closed
1 year ago
0
Implement Iterator over a Model
#232
Pat-Lafon
closed
1 year ago
1
Move clippy into CI
#231
Pat-Lafon
closed
1 year ago
1
Expensive copy of a solver
#230
TomMD
closed
1 year ago
3
implementing FuncInterp & FuncEntry
#229
Pat-Lafon
closed
1 year ago
2
Update dependencies and appease Clippy
#228
genos
closed
1 year ago
1
Use NonNull in Z3 safe bindings
#227
Pat-Lafon
opened
1 year ago
1
Z3 from string
#226
Pat-Lafon
closed
1 year ago
3
ref ast conversion into Dynamic
#225
Pat-Lafon
closed
1 year ago
0
Fails to Build in Linux
#224
Wright4TheJob
opened
1 year ago
6
add regexp support
#223
laszlo-nodebee
closed
1 year ago
1
rename context args to ctx
#222
Pat-Lafon
closed
1 year ago
1
Iterator for a solver
#221
onthestairs
opened
1 year ago
1
`Int::power(&Int)` returns `Int` but it is `Real`
#220
HKalbasi
closed
1 year ago
0
model value extraction
#219
AdamGlass
opened
1 year ago
3
Fix ci for wasm build
#218
HKalbasi
closed
1 year ago
1
Add clippy allow Attribute
#217
Pat-Lafon
closed
1 year ago
1
Make it buildable for wasm with emscripten
#216
HKalbasi
closed
1 year ago
1
Wasm build
#215
HKalbasi
closed
1 year ago
2
Bizarre and inconsistent results
#214
shriphani
closed
1 year ago
1
[Feature Request] Reading AST of uninterpreted functions from models.
#213
daemontus
opened
1 year ago
2
How to avoid long time compilation?
#212
syheliel
opened
2 years ago
1
Remove Z3_MUTEX.
#211
waywardmonkeys
closed
2 years ago
0
Stop ignoring `test_solver_unknown`
#210
SeeSpring
opened
2 years ago
1
Fix clippy errors
#209
SeeSpring
closed
2 years ago
1
Previous
Next