This removes:

- `--solver-subprocess`
- `--solver-subprocess-command`
- `--solver-fresh` (was unused AFAICT)

This adds:

- `--solver-command` with no default (meaning we run z3 in-process)
- some prints about where SMT files are generated
- auto-dumping of SMT files when invoking an external solver
- a very crude way to determine if the external solver generated a valid model (instead of assuming it is valid, so that we still benefit from refinement)

Before:

```sh
$ halmos --root examples/simple --contract VaultTest --function check_mint -vvv --statistics
[...]
[FAIL] check_mint(uint256) (paths: 8, time: 282.15s (paths: 0.45s, models: 281.70s), bounds: [])
```

After:

```sh
$ halmos --root examples/simple --contract VaultTest --function check_mint -vvv --statistics --solver-command="bitwuzla -m"
[...]
[FAIL] check_mint(uint256) (paths: 8, time: 19.69s (paths: 0.46s, models: 19.22s), bounds: [])
```