Added comment

SRI-CSL · May 24, 2024 · d644070 · d644070
1 parent ee37100
commit d644070
Showing 1 changed file with 4 additions and 1 deletion.
diff --git 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);