This test uses QF_LIA instead of the usual QF_NIA, therefore I have
removed the check for compilation withmcsat. Let me know if this is wrong,
or if the theory should be kept to QF_NIA for these tests.
Additional coverage:
api/yices_api.c:yices_arith_geq_atom()
terms/term_utils.c:finite_domain_is_nonpos(), exiting via return false
term_has_nonpos_finite_domain()
arith_term_is_nonpos(), case ITE_SPECIAL
This test uses
QF_LIA
instead of the usualQF_NIA
, therefore I have removed the check for compilation withmcsat
. Let me know if this is wrong, or if the theory should be kept toQF_NIA
for these tests.Additional coverage: api/yices_api.c:yices_arith_geq_atom() terms/term_utils.c:finite_domain_is_nonpos(), exiting via
return false
term_has_nonpos_finite_domain() arith_term_is_nonpos(), caseITE_SPECIAL