mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 13:28:47 +00:00
Code Activity

Update api.cpp

Browse source 
fix test
This commit is contained in:
Nikolaj Bjorner 2023-02-18 18:43:20 -08:00
parent cb81473260
commit a6eed9f00c
1 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/test/api.cpp
View file

@ -88,7 +88,7 @@ void test_bvneg() {
static bool cb_called = false; static bool cb_called = false;
static void my_cb(Z3_context, Z3_error_code) { static void my_cb(Z3_context, Z3_error_code) {
cb_called = true; cb_called = true;
} }
static void test_mk_distinct() { static void test_mk_distinct() {
@ -100,8 +100,8 @@ static void test_mk_distinct() {
Z3_sort bv32 = Z3_mk_bv_sort(ctx, 32); Z3_sort bv32 = Z3_mk_bv_sort(ctx, 32);
Z3_ast args[] = { Z3_mk_int64(ctx, 0, bv8), Z3_mk_int64(ctx, 0, bv32) }; Z3_ast args[] = { Z3_mk_int64(ctx, 0, bv8), Z3_mk_int64(ctx, 0, bv32) };
Z3_ast d = Z3_mk_distinct(ctx, 2, args); Z3_ast d = Z3_mk_distinct(ctx, 2, args);
VERIFY(d);
ENSURE(cb_called); ENSURE(cb_called);
VERIFY(!d);
Z3_del_config(cfg); Z3_del_config(cfg);
Z3_del_context(ctx); Z3_del_context(ctx);