926     Z3_sort int_sort;  in prove_example2()  local
941     int_sort    = Z3_mk_int_sort(ctx);  in prove_example2()
943     g_domain[0] = int_sort;  in prove_example2()
944     g           = Z3_mk_func_decl(ctx, g_name, 1, g_domain, int_sort);  in prove_example2()
1004     Z3_sort int_sort;  in push_pop_example1()  local
1016     int_sort   = Z3_mk_int_sort(ctx);  in push_pop_example1()
1017 …g_number = Z3_mk_numeral(ctx, "1000000000000000000000000000000000000000000000000000000", int_sort);  in push_pop_example1()
1020     three      = Z3_mk_numeral(ctx, "3", int_sort);  in push_pop_example1()
1024     x          = Z3_mk_const(ctx, x_sym, int_sort);  in push_pop_example1()
1060     y          = Z3_mk_const(ctx, y_sym, int_sort);  in push_pop_example1()
1085     Z3_sort       int_sort;  in quantifier_example1()  local
1110     int_sort    = Z3_mk_int_sort(ctx);  in quantifier_example1()
1112     f_domain[0] = int_sort;  in quantifier_example1()
1113     f_domain[1] = int_sort;  in quantifier_example1()
1114     f           = Z3_mk_func_decl(ctx, f_name, 2, f_domain, int_sort);  in quantifier_example1()
1160     Z3_sort int_sort, array_sort;  in array_example1()  local
1171     int_sort    = Z3_mk_int_sort(ctx);  in array_example1()
1172     array_sort  = Z3_mk_array_sort(ctx, int_sort, int_sort);  in array_example1()
1176     i1          = mk_var(ctx, "i1", int_sort);  in array_example1()
1177     i2          = mk_var(ctx, "i2", int_sort);  in array_example1()
1178     i3          = mk_var(ctx, "i3", int_sort);  in array_example1()
1179     v1          = mk_var(ctx, "v1", int_sort);  in array_example1()
1180     v2          = mk_var(ctx, "v2", int_sort);  in array_example1()
1260     Z3_sort bool_sort, int_sort, array_sort;  in array_example3()  local
1267     int_sort   = Z3_mk_int_sort(ctx);  in array_example3()
1268     array_sort = Z3_mk_array_sort(ctx, int_sort, bool_sort);  in array_example3()
1284     if (int_sort != domain || bool_sort != range) {  in array_example3()
1690     Z3_sort       int_sort;  in parser_example3()  local
1707     int_sort    = Z3_mk_int_sort(ctx);  in parser_example3()
1709     g_domain[0] = int_sort;  in parser_example3()
1710     g_domain[1] = int_sort;  in parser_example3()
1711     g           = Z3_mk_func_decl(ctx, g_name, 2, g_domain, int_sort);  in parser_example3()