search

angr / claripy

An abstraction layer for constraint solvers.
BSD 2-Clause "Simplified" License
275 stars 90 forks source link

Fix Z3 StringV abstraction #317

Closed zwimer closed 1 year ago

zwimer commented 1 year ago

Fixes: https://github.com/angr/claripy/issues/298

zwimer commented 1 year ago

Requesting review from @ltfish because git blame shows him as the last to touch this code.

zwimer commented 1 year ago

@ltfish I think the new python API handles the encoding issues (though there is a bug: https://github.com/Z3Prover/z3/issues/6442 )

github-actions[bot] commented 1 year ago

Unit Test Results

     94 files  +     84       94 suites  +84   1h 13m 8s :stopwatch: + 1h 12m 37s 1 401 tests +1 095  1 311 :heavy_check_mark: +1 065  90 :zzz: +30  0 :x: ±0  1 407 runs  +1 101  1 317 :heavy_check_mark: +1 071  90 :zzz: +30  0 :x: ±0 

Results for commit e5556e9d. ± Comparison against base commit b279b77f.

:recycle: This comment has been updated with latest results.

zwimer commented 1 year ago

Ping @ltfish

zwimer commented 1 year ago

I'm going to merge this since it was approved; if it causes issues we can always revert.