Terms from optimization not added to matching

[bclement-ocp]

It looks like terms that are used only inside an optimize statement are not added to the matching environment. Consider:

; issue.smt2
(set-logic ALL)
(set-option :produce-models true)
(declare-const x Int)
(define-fun myabs ((x Int)) Int (ite (< x 0) (- x) x))
(maximize (myabs x))
(assert (< x 0))
(assert (> x (- 10000)))
; (assert (or (>= (myabs x) 0) (<= (myabs x) 0)))
(check-sat)
(get-model)
(get-objectives)

We have:

$ alt-ergo issue.smt2 2>/dev/null

unknown
(
  (define-fun x () Int (- 1))
)
(objectives 
  ((myabs x) (+ oo))
)

This is incorrect. Uncommenting the tautology (or (>= (myabs x) 0) (<= (myabs x) 0)) gives the following instead:

$ alt-ergo issue.smt2 2>/dev/null

unknown
(
  (define-fun x () Int (- 9999))
)
(objectives 
  ((myabs x) 9999)
)

Unsure whether this was always the case or if it is a regression introduced by #921.

[Halbaroth]

This patch in Theory seems to work:

  let add_objective env fn value =
    (* We have to add the term [fn] and its subterms as the MaxSMT
       syntax allows to optimize expressions that are not part of
       the current context. *)
    let expr = fn.Objective.Function.e in
    let env = add_term env ~add_in_cs:false expr in
    (* Add the term for matching. *)
    let terms = Expr.Set.add expr env.terms in
    let objectives = Objective.Model.add fn value env.objectives in
    { env with objectives; terms }

I don't think we introduce regressions while merging OptimAE as in the original PR, terms weren't added to CC(X).