I found it very useful to use ddSMT to minimize the input SMT-LIB2 script when my solver was producing invalid model.
However, the current version does not recognize (get-model) command, so I had to add the support myself.
Would you consider adding support for this command? I have my own solution which I could submit as a pull request if needed.
I found it very useful to use ddSMT to minimize the input SMT-LIB2 script when my solver was producing invalid model. However, the current version does not recognize (get-model) command, so I had to add the support myself.
Would you consider adding support for this command? I have my own solution which I could submit as a pull request if needed.