View difference between Paste ID: rGB6jX2a and hLJ8hFf1

 /*
 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) 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
+  (forall ((i Int)) (= (cu_a i) 0.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))))
+
 #include<stdarg.h>
 #include<memory.h>
 #include<z3.h>
 
 typedef struct _nopTheoryData {
 	int dummy;
 } nopTheoryData;
 
 static void Th_delete(Z3_theory t)
 {
-  (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))))
+
 }
-cu_a_sum -> 1
+
-cu_a_0 -> 0
+
-cu_a_1 -> 0
+
-cu_a_3 -> 0
+
-cu_a_2 -> 1
+
-cu_d -> 4
+
 static void Th_init_search(Z3_theory t) {
-  2 -> 1
+
-  else -> 0
+
 static void Th_push(Z3_theory t) {
-cu_n -> {
+
 }
 static void Th_pop(Z3_theory t) {
-cu_v -> {
+
-  0 -> 0
+
-  1 -> 1
+
-  2 -> 1
+
-  3 -> 1
+
-  else -> (cu_a #0)
+
 	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
 
 	{
 		Z3_sort      cu_a_dom  = Z3_mk_int_sort(ctx);
 		Z3_symbol    cu_a_sym  = Z3_mk_string_symbol(ctx, "cu_a");
 		Z3_func_decl cu_a_decl;
 
 		cu_a_decl = Z3_mk_func_decl(ctx,cu_a_sym,1,&cu_a_dom,Z3_mk_real_sort(ctx));
 
 		a = Z3_parse_smtlib2_string(ctx,
 		  "(assert (forall ((i Int)) (= (cu_a i) 0.0)))",
 			0,0,0,
 		  1,&cu_a_sym,&cu_a_decl);
 		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;
 }