Basile Clément
Basile Clément
> Indeed, and this is actually saving us from a key issue: in Why3 empty types must be inhabited. I assume you mean all types must be inhabited, but `?`...
> The expected answer is unsat. If we remove the second constructor cons2, Alt-Ergo will promote the ADT Data to a record and we got the correct answer. Is this...
> Why we shouldn't support this before model generation? > is it a bad idea because it will generate too much casesplits In the current architecture (where case splits use...
Ah yes of course nobody is doing case splits for the boolean theory. Hm. Not sure what the proper fix is but at least we understand the issue now :)
We need to do case-splits for booleans in a way that doesn't negatively impact the existing solver, that's the tricky part (in particular doing case-splits for just any boolean term...
Closing in favor of #1156 now that we have identified the underlying cause.
Rebased on #1108
@Halbaroth what is the status of this PR?
(Superseded by #1206 )
Rebased with the new Intervals module from #1108