Valentyn Sobol

icon indicating an email [email protected]

icon location Happy tree saloed

Results 4 issues of Valentyn Sobol

Yices global lock in egraph final check

It seems like there are no reasons to acquire yices global lock during egraph final_check. https://github.com/SRI-CSL/yices2/blob/ecac3fd9d28ac3ed3de194613c36bb86115b4b3d/src/solvers/egraph/egraph.c#L6326

Thread safety

1 comment

Prepare KSMT for use in a multi-threaded environment: - [x] Use concurrent data structures in `KContext` - [ ] Guard solver native APIs with locks

enhancement

Value classes instead of Longs in Z3 API

Currently, we use `long` to represent all Z3 native objects: sorts, expressions, declarations. Also, all `Z3.Native` methods accept raw `longs` without any clarification whether it is sort, expr, or whatever...

enhancement

Fix unknown classes and ERS API improvement

5 comment

[jacodb-core] Specify identity for UnknownField, UnknownMethod, JcTypedFieldImpl [jacodb-core] Fix operations with map names in LmdbKeyValueStorage [jacodb-core] Avoid creation of named maps for R/O operations [jacodb-core] Force use of sortedSet by...