mc-imperial/jfs

jfs-opt removes relevant commands

shaobo-he opened this issue · 1 comments

Hello,

I'm using the docker image and noticed that commands like (check-sat) and (exit) are removed by jfs-opt. Is this behavior expected?

Hi @shaobo-he, sorry for the delayed response.
The issue here is that we use Z3's parser via its public API, which only seems to allow us to extract the constraints from the input file up to the first (check-sat) command.

One workaround would be to add options to jfs-opt to add the check-sat command.