From d6440702262be2c6e1a27f4c43a151e6c60667e0 Mon Sep 17 00:00:00 2001
From: Thomas Hader <tom@hader.email>
Date: Fri, 24 May 2024 15:43:18 +0200
Subject: [PATCH] Added comment

---
 src/mcsat/ff/ff_plugin.c | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

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);