Incorrect results using fresh_const in >=4.8

[djrenren]

I recently updated to z3 4.8.x and I've been having an issue with Z3_mk_fresh_const.

This example program highlights the issue:

#include <stdio.h>
#include <stdlib.h>
#include <string.h>
#include <z3.h>

int main(int argc, char** argv)
{
  Z3_config cfg = Z3_mk_config();
  Z3_context ctx = Z3_mk_context(cfg);

  Z3_ast x = Z3_mk_fresh_const(ctx, "x", Z3_mk_int_sort(ctx));
  //Z3_symbol x_name = Z3_mk_string_symbol(ctx, "x");
  //Z3_ast x = Z3_mk_const(ctx, x_name, Z3_mk_int_sort(ctx));
  Z3_ast zero = Z3_mk_int64(ctx, 0, Z3_mk_int_sort(ctx));

  Z3_solver solver = Z3_mk_solver(ctx);
  Z3_solver_inc_ref(ctx, solver);

  Z3_ast ast = Z3_mk_gt(ctx, x, zero);
  Z3_solver_assert(ctx, solver, ast);

  int result = Z3_solver_check(ctx, solver) == Z3_L_TRUE;
  printf("result: %d\n", result);
  if (!result) { return 127; }

  Z3_model model = Z3_solver_get_model(ctx, solver);
  Z3_model_inc_ref(ctx, model);

  Z3_ast out;
  result = Z3_model_eval(ctx, model, x, 1, &out) == Z3_L_TRUE;
  printf("result: %d\n", result);
  if (!result) { return 127; }

  int64_t tmp;
  result = Z3_get_numeral_int64(ctx, out, &tmp) == Z3_L_TRUE;
  printf("result: %d\n", result);
  if (!result) { return 127; }

  printf("tmp: %lld\n", tmp);

	return 0;
}

We simply create a variable "x" and assert that it's greater than 0. But evaluating the model produces the answer 0. If we comment out the Z3_mk_fresh_const and instead produce our variable through Z3_mk_const we get a correct answer of 1.

This program works fine on 4.7.1, and I can't find a documented reason it would break on 4.8.x.