Terms of facts entailed by the theory are not initialized

[Halbaroth]

Consider these two files (from issue #1008):

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

(declare-const e t)

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

and

(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)

After merging #1095, both are solved with the SAT-solver Tableaux but only the first test is solved with CDCL-Tableaux.

1. In SatML, before deciding a new atom A, we check whether the atom (or its negation) is already entailed by the theory tenv. If it is, we set the field timp to 1 in the function th_entailed.
2. During theory propagation (in the function theory_propagation), we do not assume facts with timp = 1 in the environment tenv, as it would be redundant to assume something that is already entailed by tenv.
3. If timp <> 1, terms are initialized in Th.assume. More precisely, when we call Th.assume on ((_ is B) (B .k)), we have the backtrace:

Th.assume > 
CC_X.assume_literals > 
CC_X.assume_inequalities > 
CC_X.norm_queue > 
CC_X.semantic_view > 
CC_X.add > 
CC_X.add_term > 
Uf.add > 
Uf.Env.init_term

For the first input file, we never call Th.assume with ((_ is B) (B .k)) because this atom is entailed by the record theory. Thus, we never send .k to the matching environment. In Tableaux, new terms are directly sent to the matching environment, which explains why we can prove this problem after merging #1095. Sending fresh terms in SatML helps to solve this problem but we got regressions, see #1262.

For the second input, ((_ is B) (B .k)) is not entailed by the theory and we assume it. As a result, .k is sent to the matching module.