search

sushant94 / libsmt.rs

Rust Bindings to interact with SMTLIB2 compliant solvers
Apache License 2.0
16 stars 12 forks source link

Returned output from Z3 not properly captured in Windows #13

Open selenesal opened 8 years ago

selenesal commented 8 years ago

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 commented 8 years ago

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 commented 8 years ago

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!)