From 32c9af5e5a4b119dc09eaae2bd05acf5ec7859db Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 27 Mar 2018 16:16:25 -0700 Subject: [PATCH] fix use of Z3_bool -> Z3_lbool Signed-off-by: Nikolaj Bjorner --- examples/c/test_capi.c | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/examples/c/test_capi.c b/examples/c/test_capi.c index b947928a7..c2b1f0af9 100644 --- a/examples/c/test_capi.c +++ b/examples/c/test_capi.c @@ -2452,7 +2452,6 @@ Z3_lbool ext_check(Z3_ext_context ctx) { } printf("\n"); } - return result; } @@ -2464,7 +2463,7 @@ void incremental_example1() { Z3_context ctx = ext_ctx->m_context; Z3_ast x, y, z, two, one; unsigned c1, c2, c3, c4; - Z3_bool result; + Z3_lbool result; printf("\nincremental_example1\n"); LOG_MSG("incremental_example1"); @@ -2485,7 +2484,7 @@ void incremental_example1() { c4 = assert_retractable_cnstr(ext_ctx, Z3_mk_lt(ctx, y, one)); result = ext_check(ext_ctx); - if (result != Z3_L_FALSE) + if (result != Z3_L_FALSE) exitf("bug in Z3"); printf("unsat\n");