z3 - c++ apiを使用してSAT問題でモデル値を取得するには?

Question

satの問題を解決するためにz3のc++ APIを使用しています。問題が解決したら、すべての変数の満足できる割り当てを取得したいと考えています。次のコードが示すように、変数の値を簡単に出力できます。

context c;
solver s(c);
expr x=c.bool_const("x");
s.add(x);
if(s.check()==sat){
     model m=s.get_model();
      std::cout<<"x:"<<m.eval(x);
}

しかし問題は、'if' 条件ステートメントでそれを使用する必要があるということです。例えば：

if(m.eval(x)==true)
     std::cout<<"x is true";

誰もそれを行う方法を知っていますか? 前もって感謝します。