mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-23 04:38:53 +00:00
Code Activity

add failing test for issue #62 (mk_distinct doesnt type check)

Browse source 
Signed-off-by: Nuno Lopes <nlopes@MSRC-3617536.europe.corp.microsoft.com>
This commit is contained in:
Nuno Lopes 2015-04-27 17:44:38 +01:00
parent abe73db702
commit f7d9438e7b
1 changed files with 18 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

18
src/test/api.cpp
View file

@ -447,9 +447,27 @@ void test_bvneg() {
Z3_del_context(ctx); Z3_del_context(ctx);
} }
static bool cb_called = false;
static void my_cb(Z3_context, Z3_error_code) {
cb_called = true;
}
static void test_mk_distinct() {
Z3_config cfg = Z3_mk_config();
Z3_context ctx = Z3_mk_context(cfg);
Z3_set_error_handler(ctx, my_cb);
Z3_sort bv8 = Z3_mk_bv_sort(ctx, 8);
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_mk_distinct(ctx, 2, args);
SASSERT(cb_called);
}
void tst_api() { void tst_api() {
test_apps(); test_apps();
test_bvneg(); test_bvneg();
test_mk_distinct();
// bv_invariant(); // bv_invariant();
} }
#else #else