[SMT-LIB] set-info and :status

[Cesare Tinelli]

Hi David,

On 3 Nov 2010, at 02:45, cok at frontiernet.net wrote:

> Cesare, Aaron, Clark, et al.
> 
> Since you are about to put out another version, I'll raise one more issue.
> 

It would be probably better to discuss this issue too in the SMT-API group first. I invite you to bring it up there.

Thanks,


Cesare



> 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