/* Error with nop theory plugin: $ gcc -o error error.c -lz3 $ ./error Z3 version 4.0.0.0 Context: (solver (forall ((i Int)) (>= (cu_a i) 0.0)) (forall ((i Int)) (<= (+ (cu_a i) (* (- 1.0) (cu_v i))) 0.0)) (= cu_d 4) (= (cu_n 0) 0) (= (cu_n 1) 0) (= (cu_n 2) 0) (= (cu_n 3) 0) (= (cu_a 0) cu_a_0) (= (cu_a 1) cu_a_1) (= (cu_a 2) cu_a_2) (= (cu_a 3) cu_a_3) (= (+ cu_a_0 cu_a_1 cu_a_2 cu_a_3 (* (- 1.0) cu_a_sum)) 0.0) (= (cu_v 0) 0.0) (= (cu_v 1) 1.0) (= (cu_v 2) 1.0) (= (cu_v 3) 1.0) (forall ((i Int)) (or (<= (cu_a i) 0.0) (= (cu_a i) 1.0)))) Final check Z3 check_and_get_model error: Z3 exception The mk_fresh_ext_data callback was not set for user theory, you must use Z3_theory_set_mk_fresh_ext_data_callback No error without the plugin: $ gcc -o error error.c -lz3 -DNO_THEORY $ ./error Z3 version 4.0.0.0 Context: (solver (forall ((i Int)) (>= (cu_a i) 0.0)) (forall ((i Int)) (<= (+ (cu_a i) (* (- 1.0) (cu_v i))) 0.0)) (= cu_d 4) (= (cu_n 0) 0) (= (cu_n 1) 0) (= (cu_n 2) 0) (= (cu_n 3) 0) (= (cu_a 0) cu_a_0) (= (cu_a 1) cu_a_1) (= (cu_a 2) cu_a_2) (= (cu_a 3) cu_a_3) (= (+ cu_a_0 cu_a_1 cu_a_2 cu_a_3 (* (- 1.0) cu_a_sum)) 0.0) (= (cu_v 0) 0.0) (= (cu_v 1) 1.0) (= (cu_v 2) 1.0) (= (cu_v 3) 1.0) (forall ((i Int)) (or (<= (cu_a i) 0.0) (= (cu_a i) 1.0)))) sat: cu_a_sum -> 1 cu_a_0 -> 0 cu_a_1 -> 0 cu_a_3 -> 0 cu_a_2 -> 1 cu_d -> 4 cu_a -> { 2 -> 1 else -> 0 } cu_n -> { 0 } cu_v -> { 0 -> 0 1 -> 1 2 -> 1 3 -> 1 else -> (cu_a #0) } */ #include #include #include #include #include #include typedef struct _nopTheoryData { int dummy; } nopTheoryData; static void Th_delete(Z3_theory t) { nopTheoryData * td = (nopTheoryData *)Z3_theory_get_ext_data(t); free(td); return; } static Z3_bool Th_reduce_app(Z3_theory t, Z3_func_decl d, unsigned n, Z3_ast const args[], Z3_ast * result) { return Z3_FALSE; } static Z3_bool Th_reduce_eq(Z3_theory t, Z3_ast a, Z3_ast b, Z3_ast *r) { return Z3_FALSE; } static Z3_bool Th_reduce_distinct(Z3_theory t, unsigned int n, const Z3_ast x[], Z3_ast *y) { return Z3_FALSE; } static void Th_new_app(Z3_theory t, Z3_ast n) { return; } static void Th_new_elem(Z3_theory t, Z3_ast n) { return; } static void Th_init_search(Z3_theory t) { return; } static void Th_push(Z3_theory t) { return; } static void Th_pop(Z3_theory t) { return; } static void Th_restart(Z3_theory t) { return; } static void Th_reset(Z3_theory t) { return; } static Z3_bool Th_final_check(Z3_theory t) { fprintf(stderr, "Final check\n"); fflush(stderr); return Z3_TRUE; } static void Th_new_eq(Z3_theory t, Z3_ast n1, Z3_ast n2) { return; } static void Th_new_diseq(Z3_theory t, Z3_ast n1, Z3_ast n2) { return; } static void Th_new_relevant(Z3_theory t, Z3_ast n) { return; } static void Th_new_assignment(Z3_theory t, Z3_ast n, Z3_bool v) { return; } static Z3_theory mk_simple_theory(Z3_context ctx) { nopTheoryData *td = (nopTheoryData*)malloc(sizeof(nopTheoryData)); Z3_theory Th = Z3_mk_theory(ctx, "simple_th", td); Z3_set_delete_callback(Th, Th_delete); Z3_set_reduce_app_callback(Th, Th_reduce_app); Z3_set_reduce_eq_callback(Th, Th_reduce_eq); Z3_set_reduce_distinct_callback(Th, Th_reduce_distinct); Z3_set_new_app_callback(Th, Th_new_app); Z3_set_new_elem_callback(Th, Th_new_elem); Z3_set_init_search_callback(Th, Th_init_search); Z3_set_push_callback(Th, Th_push); Z3_set_pop_callback(Th, Th_pop); Z3_set_restart_callback(Th, Th_restart); Z3_set_reset_callback(Th, Th_reset); Z3_set_final_check_callback(Th, Th_final_check); Z3_set_new_eq_callback(Th, Th_new_eq); Z3_set_new_diseq_callback(Th, Th_new_diseq); Z3_set_new_assignment_callback(Th, Th_new_assignment); Z3_set_new_relevant_callback(Th, Th_new_relevant); return Th; } /* end simple theory */ static int z3_error = 0; static void throw_z3_error(Z3_context ctx, Z3_error_code e) { z3_error = e; } static void nop_example() { Z3_ast a; Z3_context ctx; Z3_theory Th; Z3_config conf = Z3_mk_config(); Z3_lbool result; Z3_model m; unsigned major, minor, build, revision; Z3_get_version(&major, &minor, &build, &revision); fprintf(stderr, "Z3 version %d.%d.%d.%d\n", major, minor, build, revision); fflush(stderr); ctx = Z3_mk_context(conf); Z3_del_config(conf); Z3_set_error_handler(ctx, throw_z3_error); #ifndef NO_THEORY Th = mk_simple_theory(ctx); #endif a = Z3_parse_smtlib2_string(ctx, "(declare-const cu_d Int)(declare-const cu_a_sum Real)(declare-fun cu_v (Int) Real)(declare-fun cu_a (Int) Real)(declare-fun cu_n (Int) Int)(assert (forall ((i Int)) (>= (cu_a i) 0.0)))(assert (forall ((i Int)) (<= (cu_a i) (cu_v i))))(assert (= cu_d 4))(assert (= (cu_n 0) 0))(assert (= (cu_n 1) 0))(assert (= (cu_n 2) 0))(assert (= (cu_n 3) 0))(declare-const cu_a_0 Real)(assert (= (cu_a 0) cu_a_0))(declare-const cu_a_1 Real)(assert (= (cu_a 1) cu_a_1))(declare-const cu_a_2 Real)(assert (= (cu_a 2) cu_a_2))(declare-const cu_a_3 Real)(assert (= (cu_a 3) cu_a_3))(assert (= cu_a_sum (+ cu_a_0 (+ cu_a_1 (+ cu_a_2 (+ cu_a_3 0.0))))))(assert (= (cu_v 0) 0.0))(assert (= (cu_v 1) 1.000000))(assert (= (cu_v 2) 1.000000))(assert (= (cu_v 3) 1.000000))(assert (forall ((i Int))(=> (> (cu_a i) 0.0)(= (cu_a i) 1.0))))", 0,0,0,0,0,0); Z3_assert_cnstr(ctx, a); printf("Context:\n%s\n", Z3_context_to_string(ctx)); result = Z3_check_and_get_model(ctx, &m); if (z3_error != 0) { fprintf(stderr, "Z3 check_and_get_model error: %s\n", Z3_get_error_msg((Z3_error_code)z3_error)); if (z3_error == Z3_EXCEPTION) { fprintf(stderr, "\t%s\n", Z3_get_error_msg_ex(ctx, z3_error)); } fflush(stderr); return; } switch (result) { case Z3_L_FALSE: fprintf(stderr, "unsat\n"); fflush(stderr); break; case Z3_L_UNDEF: fprintf(stderr, "unknown: potential model:\n %s\n", Z3_model_to_string(ctx,m)); fflush(stderr); break; case Z3_L_TRUE: fprintf(stderr, "sat:\n%s\n", Z3_model_to_string(ctx, m)); fflush(stderr); break; } Z3_del_context(ctx); } int main() { nop_example(); return 0; }