[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