Returned output from Z3 not properly captured in Windows

[selenesal]

It seems that "unsat" is stored as "u" and "sat" is stored as "s", meaning that in smtlib2.rs::check_sat(), the call to &smt_proc.read() never seems to return "sat\n", and so all results from Z3 are marked as "Unsat".

This same code also doesn't account for an error returned from Z3, which isn't the same as "Unsat". This would be true for any environment.

[sushant94]

This same code also doesn't account for an error returned from Z3, which isn't the same as "Unsat". This would be true for any environment.

Yes, I agree, this is one of the todo features. Currently, unsat is used for unsat/errors. Perhaps I'll add this.

So you mean to say on windows Z3 returns s (for sat) and u (for unsat)? Sorry, I have tested this only on linux / OSX.

Edit: I just checked on windows, z3 does return sat/unsat

[selenesal]

Z3 performs correctly, but there seems to be some issue with the ChildStdOut::read() function on Windows; this seems like a known issue in Rust. A call to read will return only the first character of the standard output of the child process, and a second call to read will return the rest of the output (if any).

We're working on a workaround by telling Z3 to write its output to a file, and then reading from the file (no platform-specific issues encountered so far!)