Optimization gives incorrect model

[JoD]

Running the following formula

(declare-fun local_parts () Bool)
(declare-fun nbparts () Int)
(declare-fun objective () Int)
(assert (and (< 1 nbparts) (= objective (+ (* (- nbparts) nbparts) nbparts (ite local_parts 9 0)))))
(maximize objective)
(check-sat)

on the command line via command

z3 -smt2 /tmp/file_with_above_formula -model

the returned solution is

sat
(
  (define-fun local_parts () Bool
    false)
  (define-fun nbparts () Int
    2)
  (define-fun objective () Int
    (- 2))
)

local_parts() should be true.

Z3 commit: 3c16edc

This is a distillation of https://gitlab.com/krr/IDP-Z3/-/issues/153

[JoD]

Thanks!