unrecognized solver output: #<eof>

[SuzanneSoy]

When trying one of the basic examples from the docs, I get the following error:

.racket/snapshot/pkgs/rosette/rosette/solver/smt/cmd.rkt:60:0: solution: unrecognized solver output: #<eof>

Here's the program:

#lang rosette/safe

(define (poly x)
 (+ (* x x x x) (* 6 x x x) (* 11 x x) (* 6 x)))

(define-symbolic x y integer?)
(define sol
    (solve (begin (assert (not (= x y)))
                  (assert (< (abs x) 10))
                  (assert (< (abs y) 10))
                  (assert (not (= (poly x) 0)))
                  (assert (= (poly x) (poly y))))))
(evaluate x sol)
(evaluate y sol)
(evaluate (poly x) sol)
(evaluate (poly y) sol)

I'm using Z3 version 4.4.1, 64-bit version, on the NixOS Linux Distribution.

I tried adding (writeln (port->string (peeking-input-port port))) inside (read-solution) in smtlib2.rkt, and indeed, I get an empty string, but I don't know where to look further.

Is there anything I can do to debug this?

[SuzanneSoy]

Oh, my bad.

The issue is that regular Linux executables do not work out-of-the-box with NixOS, and rosette was using a custom, auto-downloaded version of z3, which therefore triggered an error as soon as it was run.

I'm closing this as this is more an issue with NixOS than with Rosette.

[emina]

You got to it before me :) My guess was going to be an OS-specific issue. (We've tested on Mac OS and Ubuntu.)

[SuzanneSoy]

For the future lurker (I know a couple of Racket users are on NixOS), here's the procedure I followed:

# Patch the NixOS recipe for Z3:

git clone https://github.com/nixos/nixpkgs.git nixpkgs-clone
nano nixpkgs-clone/pkgs/applications/science/logic/z3/default.nix
# Change:
#    rev    = "z3-${version}";                            # before
#    sha256 = "1ix100r1h00iph1bk5qx5963gpqaxmmx42r2vb5zglynchjif07c";
# To:
#    rev    = "d89c39cbe2bb862daff2c183a79361360f7e2dc1";  # git revision from rosette/private/install
#    sha256 = "1ljrx1r4mhm7i1189k5xkcs4k5nbhnx7sqvxps82d3i3hw7yykrm";

# Install it:

nix-env -f "$PWD/nixpkgs-clone" -iA z3

# replace Rosette's z3 executable by NixOS's one:

mv -i ~/.racket/VERSION/pkgs/rosette/bin/z3 ~/.racket/VERSION/pkgs/rosette/bin/z3.bak
ln -s ~/.nix-profile/bin/z3 ~/.racket/VERSION/pkgs/rosette/bin/z3

Then rosette works like a charm for me, on Racket 6.8 (be sure to re-run the file with F5 in DrRacket of course).

Don't forget to update the Nix recipe when Rosette updates the Z3 version it depends on, it is written in the get-z3-url function in ~/.racket/VERSION/pkgs/rosette/rosette/private/install.rkt.

Here is the full default.nix file for Z3 which I used, obtained after changing the Git revision and the SHA256 field: nixpkgs-pkgs-applications-science-logic-z3-default.nix.txt