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 Remove the Record theory #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 73740e6. 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.

[bclement-ocp]

What about initializing the variables in CC(X) even if they only appear below quantifiers (we probably don't want to initialize variables that are truly unused)? It's a bit weird that we don't actually create the variable in this case.