Z3 issue: toStream gives different result as toInt conversion

z3bug.cc

#include <iostream>
#include <z3++.h>
 
int main() {
 
  z3::config config;
  z3::context context{config};
  z3::optimize optimizer{context};
 
  auto x = context.int_const("x");
 
  optimizer.add((x > 15) && (x < 20));
  optimizer.minimize(x);

  if (optimizer.check() != z3::sat)
    return -1;

  auto model = optimizer.get_model();

  for (unsigned i = 0; i < model.num_consts(); ++i) {
    z3::func_decl decl = model[i];

    std::cout << model.get_const_interp(decl) << std::endl;

    int x = model.get_const_interp(decl);
    std::cout << x << std::endl;
  }

}

// output is
//
// 16
// 1
//
// branch qsat @31643a8