z3-example.c

#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; }

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

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

	return 0;
}