When a "default" context is created with the following:

let ctx = Context.create ~config:(Context.Config.create ()) ()

Any function on non-bit values (e.g., Type.is_int) that come after the context initialization will trigger the exception YicesError(38,_) (error named BVTYPE_REQUIRED).

I think this issue is linked to how the garbage collection happens. The context* pointer in the yices library is part of the problem.

In theory, _oy_config_finalize should be called as soon as the ctx is out of scope so that the context* pointer is cleared and so that the next function calls have no side-effects.

I tried to change the values used and max in caml_alloc_custom(_,_,used,max) in src/contexts.c, l.58:

#define caml_alloc_config() caml_alloc_custom(&_oy_ctx_config_ops, sizeof (ctx_config_t*), 0, 1)

The integers 0,1 mean that the garbage collector will choose itself when it should garbage collect.

I tried the values 1,1 which means that every 1 allocation, the garbage collection will occur. But the first allocation will only be cleared when a new allocation is done...

The expected behavior is: whenever we get out of scope of Config or Context ocaml variables, the garbage collection should happen immediately and shouldn't wait the next call of caml_alloc_custom().

I didn't find any way of forcing the _oy_config_finalize to be called as soon as the variable is out of scope.

Edit: the exact order of tests for reproducing the error:

checkoverflow
bitsize
type_consistency

Workaround: we should create the ocaml functions Config.reset so that we can reset the config
after having used Config.create. This way, we manually do what the GC should do for us.