[YICES-HELP] Re: yices_mk_div, yices_mk_mod

[Bruno Dutertre]

Kai Trojahner wrote:
> Dear Bruno,
> 
> thanks for answering so quickly.
> Unfortunately, the solution does not work (at least on my Mac with yices 
> 1.0.14).
> yices_get_var_decl_from_name(ctx, "div") yields NULL and thus a 
> yices_mk_var_from_decl() quits with a bus error.
> 
> I modified function init() in your example to report what's wrong:
> 
> static void init(void) {
>  yices_var_decl div_decl, mod_decl;
> 
>  ctx = yices_mk_context();
>  div_decl = yices_get_var_decl_from_name(ctx, "div");
>  mod_decl = yices_get_var_decl_from_name(ctx, "mod");
>  if (div_decl == 0) printf("Declaration of div is NULL\n");
>  if (mod_decl == 0) printf("Declaration of mod is NULL\n");
> 
>  div = yices_mk_var_from_decl(ctx, div_decl);
>  mod = yices_mk_var_from_decl(ctx, mod_decl);
> }
> 
> and I get:
> 
>  > ./a.out
> Declaration of div is NULL
> Declaration of mod is NULL
> Bus error
> 
> Any ideas?
> Kai
> 
>

I cannot reproduce this. It works fine for me. What version
are you using? There are six variants for Mac OS.

Bruno