[SMT-LIB] set-info and :status

cok@frontiernet.net cok at frontiernet.net
Wed Nov 3 03:45:27 EDT 2010


Cesare, Aaron, Clark, et al.

Since you are about to put out another version, I'll raise one more issue.

The :status info-item, obtained with (get-info :status) is supposed to return the most recent result of a check-sat command.
- I presume, that is the most recent check-sat command, regardless of intervening commands.
- Or is it reset (to what?) by an assertion-set command, just as getting values, assignments, etc. are invalidated by assertion-set commands.
- In either case, what is the value of :status before any check-sat commands are issued? unknown? unsupported?
- What is the utility of being able to apply set-info to :status.  It is the only predefined infoflag that is settable?  I'd suggest not having set-info at all.

David


More information about the SMT-LIB mailing list