Incompleteness example for record theory (with quantifiers)

[Halbaroth]

Consider the input file:

(set-logic ALL)
(declare-datatype t ((box (unbox Int))))
(declare-const v t)
(assert (forall ((u Int)) (distinct v (box u))))
(check-sat)

Alt-Ergo answers unknown on next. We expect that Alt-Ergo solves this problem as follows:

1. Alt-Ergo realizes that t is of the form (box u) for some integer u.
2. One matches (box u) with the trigger of the axiom.
3. One encounters a contradiction after asserting (distinct v (box u)).

This reasoning fails both on next and on PR #1095 for slightly different reasons.

• On next, we never produce the equation v = (box (unbox v)) because v is a variable. These equations are only added into the context of X.make for record construction terms.
• On #1095, we never send v to CC(X) because the only assertion involving v is under a quantifier. In particular, Adt_rel cannot discover that the domain of v has to be singleton.

I tried to fix it with this patch https://github.com/OCamlPro/alt-ergo/commit/73740e62ca8a8473835294c00ab3ab517bfe33d3. I got +26-22 (after correction) on ae-format but the solver was slightly slower.

We don't expect completeness for the Record theory in the presence of quantifiers, but it is interesting to know why this test fails.