Unrecognized solver output

[natebragg]

I'm running into this issue on v4.1, racket v8.6 (also tested on v8.1), z3 v4.9.0 on aarch64:

> (define-symbolic b boolean?)
> (solve b)
; read-solution: unrecognized solver output: #<eof> [,bt for context]
> ,bt
; read-solution: unrecognized solver output: #<eof>
;   context...:
;    /home/nate/.local/share/racket/8.6/pkgs/rosette/rosette/solver/smt/base-solver.rkt:133:0: read-solution
;    /home/nate/.local/share/racket/8.6/pkgs/rosette/rosette/solver/smt/base-solver.rkt:92:0: solver-check
;    /home/nate/.local/share/racket/8.6/pkgs/rosette/rosette/query/core.rkt:27:0: body of top-level
;    /home/nate/.local/share/racket/pkgs/xrepl-lib/xrepl/xrepl.rkt:1573:0
;    /home/nate/.local/share/racket/collects/racket/repl.rkt:11:26

This seems to work fine with rosette v4.1, racket v8.5, z3 v4.9.0 on x64:

> (define-symbolic b boolean?)
> (solve b)
(model)

Since I doubt it's the version of racket, presumably something is going awry between rosette and z3 that's aarch64 specific.

[jamesbornholt]

Did you build Z3 yourself? As far as I know, Z3 only distributes aarch64 binaries for macOS. Can you make sure that you can execute the Z3 binary you installed?

Our default Z3 installer isn't architecture-aware right now and will blindly try to install an x86 version of Z3, which will actually work on ARM Macs via Rosetta, but obviously won't work on Linux. That's something we need to fix up, but since it sounds like you're using your own build of Z3, that won't help here.

[natebragg]

z3 is also distributed for Arch (and Manjaro, which I'm using), and is available from their community repository (although this appears to be incorrectly listed in their packages list, it's definitely available through the package manager).

The z3 binary executes just fine:

nate@hassipura-plyn-frie:~$ z3
Error: input file was not specified.
For usage information: z3 -h
nate@hassipura-plyn-frie:~$ which z3
/usr/bin/z3
nate@hassipura-plyn-frie:~$ pacman -Qo /bin/z3
/usr/bin/z3 is owned by z3 4.9.0-1

[natebragg]

I see this also (the path is because I had to build racket myself):

nate@hassipura-plyn-frie:~$ .local/share/racket/8.6/pkgs/rosette/bin/z3 
-bash: .local/share/racket/8.6/pkgs/rosette/bin/z3: cannot execute binary file: Exec format error

Presumably this is the file you're talking about. If I rename it then suddenly rosette works. Is there a way to check to see if a system install of z3 is available before trying to install one that comes with rosette?

[emina]

Rosette won’t look for existing installations of Z3. But you can ask it to use a specific installation by providing a path to that installation when you create the solver. Here is the documentation.

Edited to add: you may also want to change the current-solver parameter to use your custom solver instance.

[natebragg]

Well, for now I'm happy to just delete rosette's copy of z3. I hope at some point you decide to officially support arm.