smbc returns model with empty type even though a val of this type was declared

[samuelgruetter]

Description of problem: see here.

[c-cube]

I'll take a look, thank you.

[c-cube]

Empty types will always be completed now. It never hurts to do that.

[samuelgruetter]

Empty types will always be completed now. It never hurts to do that.

Even if I have axiom forall (v: MyEmptyType). false. ?

[c-cube]

Hmmm I'd consider that as unsat, but that's an interesting point. I suppose exists (v:foo). true would be used to make a type non empty? I'm not used to reasoning with possibly empty types, tbh.

(cc @blanchette for opinions on the topic)

[blanchette]

Hi Simon, Nunchaku and (to the best of my knowledge and *hope*, SMBC) are based on simple type theory, in which all types are inhabited. Cheers, Jasmin

…

On 14. Oct 2018, at 01:29, Simon Cruanes ***@***.***> wrote: Hmmm I'd consider that as unsat, but that's an interesting point. I suppose exists (v:foo). true would be used to make a type non empty? I'm not used to reasoning with possibly empty types, tbh. (cc @blanchette <https://github.com/blanchette> for opinions on the topic) — You are receiving this because you were mentioned. Reply to this email directly, view it on GitHub <#5 (comment)>, or mute the thread <https://github.com/notifications/unsubscribe-auth/AAuZ4z26NDa-GeMLk_nBS5SC_HUaa1xbks5ukndrgaJpZM4Xa0pb>.

[c-cube]

@blanchette yes, datatypes are always inhabited. Uninterpreted types are, too, but this bug occurs in the case where a type is never touched (no value in it is ever used), so the printed model was empty :-)
I guess that's the way things should continue to be, then. Thank you.