LeeYoungJoon
Thanks for your advice. I got a different error, as shown below, when trying with the latest version of Z3 (https://github.com/Z3Prover/z3/releases/tag/z3-4.13.0). ``` Transformation doesn't verify! (not unsound) ERROR: SMT Error:...
[z3_log.txt.zip](https://github.com/AliveToolkit/alive2/files/15328993/z3_log.txt.zip) Please confirm the log of z3. I tried to running `z3 -v:5 -log z3_log.txt` and the log is [z3_log_log.txt.zip](https://github.com/AliveToolkit/alive2/files/15329024/z3_log_log.txt.zip) And i tried to run `z3 -v:10000 -log z3_log.txt` and...
No, I am running on a 64-bit machine. Here is the kernel information of my machine. ``` Darwin YoungJunui-MacBookPro.local 23.4.0 Darwin Kernel Version 23.4.0: Wed Feb 21 21:45:49 PST 2024;...
Attached are the Z3 logs, which were created by their respective versions of Z3. [z3_log_4.12.2.txt.zip](https://github.com/AliveToolkit/alive2/files/15343715/z3_log_4.12.2.txt.zip) [z3_log_4.13.0.txt.zip](https://github.com/AliveToolkit/alive2/files/15343716/z3_log_4.13.0.txt.zip)
Following your guide, I am trying to reduce the size of the log. How is the fixed printing stats problem(https://github.com/Z3Prover/z3/commit/18a95d89c6b16994ff07d31e5059e79b007f6c4e) related to this issue? And I am not sure which...
I have confirmed normal operation under the following conditions. * z3 version : 4.13.0 * llvm-project : [main branch](https://github.com/llvm/llvm-project/commit/b06f97b039b3a4f2397281609069b2aaad86dd59) (Latest version as of May 14) * alive2 : [master branch](https://github.com/AliveToolkit/alive2/commit/1a42db1b094c8a2dbd13d999d09b3044712e269a)...
@nikic @nunoplopes I would like to try to fix this problem. Could I get some help to do so?
@nunoplopes Hi Nuno, I know you’re busy, but I’d like to follow up on this draft PR. I’m having trouble with some parts of the implementation, so if you have...
Thank you for the feedback. (#1239) When `allocsize` is missing in the `myalloc` function, should it return null or allocate a fresh block if it’s non-null? Since allockind("alloc") implies returning...
Thanks for the advice. I’ve started working on this.