Ahmed Irfan

what about yices_model_set_yval? (e.g. yval is taken from some other model)

The example doesn't contain nonlinearity. If you set the logic to QF_LIA, Yices solves this immediately.

> At some point, we might consider prefixing all constants exposed as part of the API with YICES_, matching the function names. FWIW, > […](#) +1 That's a good point.

Thanks for reporting this. I can reproduce the issue.

A Sample Code to reproduce the bug (using simpler terms than the above pseudocode): ``` #include #include "yices.h" #include "assert.h" /* * Create an MCSAT context */ static context_t *make_mcsat_context(void)...

Thanks for reporting the issue. I am able to reproduce the issue. We will look into this soon.