Under certain conditions the SMT2 frontend does not flush the output after reporting the command results. This greatly frustrates interacting with yices from another program. These errors can be observed by running yices-smt2 | cat. Piping the output through cat is essential as it disables the default line-buffering of the terminal.
So far I have observed this with the following commands:
check-sat-assuming with default options in non-incremental mode
check-sat with produce-unsat-cores in non-incremental mode
Looking at the code some, check_delayed_assertions (used by check-sat in non-incremental no-unsat-cores mode) ends with a flush_out() while check_delayed_assertions_assuming (used by check-sat-assuming in the same mode) does not. Perhaps rather than finding all the places that print a result without calling flush_out afterwards it would be better to add a flush_out() call to report_status or show_status and other mid-level output routines as appropriate.
Under certain conditions the SMT2 frontend does not flush the output after reporting the command results. This greatly frustrates interacting with yices from another program. These errors can be observed by running
yices-smt2 | cat
. Piping the output through cat is essential as it disables the default line-buffering of the terminal.So far I have observed this with the following commands:
Looking at the code some,
check_delayed_assertions
(used by check-sat in non-incremental no-unsat-cores mode) ends with aflush_out()
whilecheck_delayed_assertions_assuming
(used by check-sat-assuming in the same mode) does not. Perhaps rather than finding all the places that print a result without calling flush_out afterwards it would be better to add aflush_out()
call to report_status or show_status and other mid-level output routines as appropriate.