Add test from issue 1008

[Halbaroth]

This commit adds a test suggested by Basile in issue #1008.

[bclement-ocp]

I think we should also add the failing:

(set-logic ALL)
(declare-datatype t ((B (i Int))))

(declare-const e t)

(assert ((_ is B) e))
(assert (forall ((n Int)) (distinct e (B n))))
(check-sat)

And we would expect it to get fixed in #1211.

[bclement-ocp]

Expected files seem to be empty but OK to merge with the correct expected files.

[bclement-ocp]

I think we should add a note somewhere that "this currently returns unknown but we want it to return unsat once #1008 is fixed", to avoid thinking there is a soundness issue with the fix.

[Halbaroth]

I will add the note in #1008.

[bclement-ocp]

The rationale for adding a note in the test itself is that if a test fails, the test file is the first place we are going to look.

[Halbaroth]

Rofl, I forgot to call make promote.