From 831e0b783f6f99c8ee6e7bac5f131e1cfedbe0ae Mon Sep 17 00:00:00 2001
From: Thomas Sewell <Thomas.Sewell@cl.cam.ac.uk>
Date: Tue, 5 Sep 2023 17:30:43 +0100
Subject: [PATCH] CN: more diagnostic messages on failures

---
 backend/cn/check.ml | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/backend/cn/check.ml b/backend/cn/check.ml
index 5fe8243e6..746e44113 100644
--- a/backend/cn/check.ml
+++ b/backend/cn/check.ml
@@ -613,6 +613,8 @@ let rec check_pexpr (pe : 'bty mu_pexpr) ~(expect:BT.t)
               else (warn_uf loc "mod_uf"; IT.mod_no_smt_ (v1, v2)))
         | `False ->
            let@ model = model () in
+           Pp.debug 1 (lazy (Pp.item "rem_t applied to (possibly) negative arguments"
+               (Pp.list IT.pp [v1; v2])));
            let err = !^"Unsupported: rem_t applied to negative arguments" in
            fail (fun ctxt ->
                let msg = Generic_with_model {err; model; ctxt} in