Sub-optimal optimize result. Model (still) doesn't match objectives.

[ehbarbian]

Hi,

Looks like this is still a problem. Changing just a little the input problem (basically swap A1 by B1, and A2 by B2 consts), bring back the wrong result:

problem.smt2

(set-option :opt.maxsat_engine maxres)
(declare-fun A1.N1 () Bool)
(declare-fun A1.N2 () Bool)
(declare-fun A2.N1 () Bool)
(declare-fun A2.N2 () Bool)
(declare-fun B1.N1 () Bool)
(declare-fun B1.N2 () Bool)
(declare-fun B2.N1 () Bool)
(declare-fun B2.N2 () Bool)

(declare-fun N1.max () Int)
(declare-fun N1.min () Int)
(declare-fun N2.max () Int)
(declare-fun N2.min () Int)

(declare-fun N1.used () Bool)
(declare-fun N2.used () Bool)

(assert (and ((_ at-least 1) A1.N2 A1.N1)
             ((_ at-least 1) A2.N2 A2.N1)
             ((_ at-least 1) B1.N2 B1.N1)
             ((_ at-least 1) B2.N2 B2.N1)
             ((_ at-most 1) A1.N2 A1.N1)
             ((_ at-most 1) A2.N2 A2.N1)
             ((_ at-most 1) B1.N2 B1.N1)
             ((_ at-most 1) B2.N2 B2.N1)))

(assert (and (= (+ (ite B1.N1 1 0) (ite B2.N1 1 0))
                (+ (ite A1.N1 1 0) (ite A2.N1 1 0)))
             (= (+ (ite B1.N2 1 0) (ite B2.N2 1 0))
                (+ (ite A1.N2 1 0) (ite A2.N2 1 0)))))

(assert (and (=> (not N1.used) (= N1.min N1.max))
             (=> (not N2.used) (= N2.min N2.max))))

(assert (and (= B2.N2 A1.N2)
             (= B2.N1 A1.N1)))

(assert (and (= N1.used (or A1.N1 A2.N1 B1.N1 B2.N1))
             (= N2.used (or A1.N2 A2.N2 B1.N2 B2.N2))))

(assert (and (=> A1.N2 (and (<= N2.min 5) (>= N2.max 5)))
             (=> A1.N1 (and (<= N1.min 5) (>= N1.max 5)))
             (=> A2.N2 (and (<= N2.min 9) (>= N2.max 9)))
             (=> A2.N1 (and (<= N1.min 9) (>= N1.max 9)))
             (=> B1.N2 (and (<= N2.min 1) (>= N2.max 1)))
             (=> B1.N1 (and (<= N1.min 1) (>= N1.max 1)))
             (=> B2.N2 (and (<= N2.min 5) (>= N2.max 5)))
             (=> B2.N1 (and (<= N1.min 5) (>= N1.max 5)))))

(minimize (+ (- N1.max N1.min)
             (- N2.max N2.min)))

(maximize (+ (ite N1.used 1 0)
             (ite N2.used 1 0)))

(check-sat)
(get-model)
(get-objectives)

Expected result (v4.8.8)

$ z3-4.8.8 smt.arith.solver=2 -smt2 problem.smt2

sat
(model 
  (define-fun A1.N1 () Bool false)
  (define-fun A1.N2 () Bool true)
  (define-fun A2.N1 () Bool true)
  (define-fun A2.N2 () Bool false)
  (define-fun B1.N1 () Bool true)
  (define-fun B1.N2 () Bool false)
  (define-fun B2.N1 () Bool false)
  (define-fun B2.N2 () Bool true)
  (define-fun N1.max () Int 9)
  (define-fun N1.min () Int 1)
  (define-fun N2.max () Int 5)
  (define-fun N2.min () Int 5)
  (define-fun N1.used () Bool true)
  (define-fun N2.used () Bool true)
)
(objectives
 ((+ (- N1.max N1.min) (- N2.max N2.min)) 8)
 ((+ (ite N1.used 1 0) (ite N2.used 1 0)) 2)
)

Result obtained (v4.8.12)

$ z3-4.8.12 smt.arith.solver=2 -smt2 problem.smt2

sat
(
  (define-fun A1.N1 () Bool false)
  (define-fun A1.N2 () Bool true)
  (define-fun A2.N1 () Bool false)
  (define-fun A2.N2 () Bool true)
  (define-fun B1.N1 () Bool false)
  (define-fun B1.N2 () Bool true)
  (define-fun B2.N1 () Bool false)
  (define-fun B2.N2 () Bool true)
  (define-fun N1.max () Int 10)
  (define-fun N1.min () Int 10)
  (define-fun N2.max () Int 9)
  (define-fun N2.min () Int 1)
  (define-fun N1.used () Bool false)
  (define-fun N2.used () Bool true)
)
(objectives
 ((+ (- N1.max N1.min) (- N2.max N2.min)) 8)
 ((+ (ite N1.used 1 0) (ite N2.used 1 0)) 2)
)

Originally posted by @ehbarbian in #5145 (comment)