Add maximize/minimize terms for matching

src/lib/reasoners/theory.ml

@@ -927,12 +927,14 @@ module Main_Default : S = struct
 
   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 aren't part of
+       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
+    (* We also have to 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 }
+    { env with objectives; terms }
 
   let reinit_cpt () =
     Debug.reinit_cpt ()

tests/issues/1163.models.expected

@@ -0,0 +1,8 @@
+
+unknown
+(
+  (define-fun x () Int (- 9999))
+)
+(objectives 
+  ((myabs x) 9999)
+)

tests/issues/1163.models.smt2

@@ -0,0 +1,11 @@
+(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)