Развернуть / свернуть Z3 SMT C ++ API

Как я могу использовать API C ++, чтобы получить оптимизацию для данной символьной переменной SymVar_0?

я видел эта почта но не понимает, как его использовать.

(set-logic QF_AUFBV)(declare-fun SymVar_0 () (_ BitVec 32))(declare-fun SymVar_1 () (_ BitVec 8))(declare-fun SymVar_2 () (_ BitVec 8))(declare-fun SymVar_3 () (_ BitVec 8))(declare-fun SymVar_4 () (_ BitVec 8))(declare-fun SymVar_5 () (_ BitVec 8))(declare-fun SymVar_6 () (_ BitVec 8))(declare-fun SymVar_7 () (_ BitVec 8))(declare-fun SymVar_8 () (_ BitVec 8))(declare-fun SymVar_9 () (_ BitVec 8))(declare-fun SymVar_10 () (_ BitVec 8))(declare-fun SymVar_11 () (_ BitVec 8))(declare-fun SymVar_12 () (_ BitVec 8))(declare-fun SymVar_13 () (_ BitVec 8))(declare-fun SymVar_14 () (_ BitVec 8))(declare-fun SymVar_15 () (_ BitVec 8))(declare-fun SymVar_16 () (_ BitVec 8))(declare-fun SymVar_17 () (_ BitVec 8))(assert (= (ite (= ((_ extract 0 0) (ite (= ((_ extract 31 0) (bvsub (concat ((_ extract 7 0) ((_ extract 31 24) SymVar_0)) ((_ extract 7 0) ((_ extract 23 16) SymVar_0)) ((_ extract 7 0) ((_ extract 15 8) SymVar_0)) ((_ extract 7 0) ((_ extract 7 0) SymVar_0))) ((_ sign_extend 0) (_ bv2 32)))) (_ bv0 32)) (_ bv1 1) (_ bv0 1))) (_ bv1 1)) (_ bv4198495 32) (_ bv4198490 32)) (_ bv4198495 32)))(assert (bvsge SymVar_0 (_ bv1 32)))(minimize SymVar_0)

Давайте посмотрим, я хочу оптимизировать предыдущую формулу.

Спасибо