En Z3, lo siguiente se evalúa claramente a un máximo de 2, con el modelo x = verdadero e y = verdadero.

(declare-const x Bool)
(declare-const y Bool)
(declare-const z Bool)
(assert(= z false))
(maximize(
  +  
    (ite (= x true) 1 0) 
    (ite (= y true) 1 0) 
    (ite (= z true) 1 0)
  )
)
(check-sat)
(get-model)

¿Cómo podría implementar esto usando las API de C / C ++? He intentado simplemente analizar usando esto:

Z3_ast parsed = Z3_parse_smtlib2_string(c,<The above Z3>,0,0,0,0,0,0);
z3::expr simpleExample(c, parsed);
s.add(simpleExample);

Pero imprime "unsupported \n ;maximize".

No me importaría construir la expresión manualmente, en lugar de usar un archivo construido. Simplemente no sabía qué funciones u operadores expr usar para "maximize".

ADENDA: A la luz de algunas respuestas y discusiones recientes, parece claro que lo que solicito no es una funcionalidad normal en este momento. Entonces, alteré la pregunta para pedir los detalles específicos de una manera de hacer que esto funcione como están las cosas en este momento.