Currently this project is using Z3 4.8.8, that is released 5 years ago. And it has a bug that not appears in the latest version.
The bug can be reproduced with this file: advent of code 2025 day 10 solution and this input file: day10.txt
Use this command at the 2025 directory using Racket 9.0, advent-of-code package and rosette:
racket aoc.rkt 10 -t < day10.txt
The answer at the second line is a result produced by Z3. Currently the code uses a custom installed Z3 4.15.1. It produces a correct answer 19857. But the bundled one would produce a slight higher answer 19864.
Currently this project is using Z3 4.8.8, that is released 5 years ago. And it has a bug that not appears in the latest version.
The bug can be reproduced with this file: advent of code 2025 day 10 solution and this input file: day10.txt
Use this command at the
2025directory using Racket 9.0,advent-of-codepackage androsette:racket aoc.rkt 10 -t < day10.txtThe answer at the second line is a result produced by Z3. Currently the code uses a custom installed Z3 4.15.1. It produces a correct answer
19857. But the bundled one would produce a slight higher answer19864.