ddsmt / ddSMT

A delta debugger for SMT benchmarks in SMT-LIB v2.
https://ddsmt.readthedocs.io
Other
50 stars 17 forks source link

Adding support for (get-model) command #18

Closed blishko closed 4 years ago

blishko commented 4 years ago

In my application I needed to make sure that ddSMT does not eliminate the (get-model) command during simplification, hence the change in _substitute_cmds method. I am not sure if there is a better way to do that or if it interacts with other ways of using ddSMT.

mpreiner commented 4 years ago

You can use a wrapper script to check the existence of a (get-model) command in the input. I'd not prohibit ddSMT from eliminating (get-model) in general.

blishko commented 4 years ago

You can use a wrapper script to check the existence of a (get-model) command in the input.

That's a good point. Thanks!

I can remove the commit. What do you prefer revert or rewriting with push force?

mpreiner commented 4 years ago

Both is fine, we'll squash and merge the PR anyways :-)