ethereum
SMTChecker: Use Z3 through the SMT-LIB interface
Instead of using Z3 as a library, we use Z3 as an external solver, the same way as we already use Eldarica and cvc5.
After discussion with @ekpyron, we decided that emscripten build of solc will be an exception.
The rationale is that switching also the javascript binary of the compiler would require changes in solc-js and would put additional burden on users who would like to use SMTChecker.
Fortunately, Z3 exposes an API method Z3_eval_smtlib2_string (from C interface of Z3), which seems to behave exactly as calling the solver on the given SMT-LIB2 script.
Thus, we can reuse the same infrastructure we have for processing answers in both cases (calling external process, or calling this API method).
Did something change in the model checker engine settings here? I just quickly checked the emscripten binary on remix and was surprised to only get CHC responses - and then also checked the static ubuntu binary, which also only seems to run CHC no matter what I pass in as --model-checker-engine. We could change the behaviour of all this, but what I just saw seemed a bit odd at least :-).
That should not be the case. I will investigate. What exactly have you been trying? What examples?
I just checked again: my mistake was mainly that (since that's easier for remix) using the old experimental smtchecker pragma, which seems to override the CLI settings. And also forgot that for some cases if CHC solves it, we won't even query BMC anymore. With some more care in testing all seems to indeed work as expected! Sorry for the false alarm :-).
I should squash everything to a single commit?
That's usually how we do it. But if you want/feel the need to separate things, maybe group everything in 2 or 3 major commits.
The comments here actually look perfectly fine to me.
It's not really about the number. What we don't want is messy history where things are changed and then changed back within the same PR, making it hard to follow. If that's the case then squashing into a single commit is a simple way out. But each commit being one logical, atomic change with a good description is actually superior if we can get it.
So just make sure there are no separate commits for review corrections (they should all be squashed into the original commits they fix) and it's fine. The one commit called "Fixup" sounded like something like that, but it seems that it's actually just normal fix so it's fine.
I tried to keep the commits logically compact. I think I can improve some of the commit messages and squash some of the commits together, but I would prefer to keep at least some commits separate, because they address different issues.