[YICES-HELP] yices_max_sat() returning l_undef

[Mark Liffiton]

Hi,

yices_max_sat() is returning l_undef on some instances I'm running, and 
I'd like to avoid that, if possible.  Is there any more information on 
this than is available in the C API documentation?  I'm already calling

yices_set_max_num_iterations_in_maxsat(numeric_limits<unsigned>::max());

before calling yices_max_sat().  It's not clear if increasing the "maximum 
number of conflicts that are allowed in a maxsat iteration" would help as 
well, or if that would simply result in a drawn out "iteration" that does 
not find a solution.  It's not clear to me what these terms mean, exactly, 
so any clarification or advice would be helpful.

Thank you.

--Mark