diff --git a/src/mcsat/ff/ff_plugin.c b/src/mcsat/ff/ff_plugin.c index 0578a3406..ee1952dbb 100644 --- a/src/mcsat/ff/ff_plugin.c +++ b/src/mcsat/ff/ff_plugin.c @@ -261,8 +261,11 @@ void ff_plugin_set_lp_data(ff_plugin_t *ff, term_t t) { if (ff->lp_data) { assert(ff->constraint_db); - if (!lp_data_is_order(ff->lp_data, order)) + if (!lp_data_is_order(ff->lp_data, order)) { + // currently only one finite field type is supported in MCSat + // an error is reported when two different finite field types are presented longjmp(*ff->ctx->exception, MCSAT_EXCEPTION_UNSUPPORTED_THEORY); + } } else { ff->lp_data = lp_data_new(order, ff->ctx); ff->constraint_db = poly_constraint_db_new(ff->lp_data);