From a2a4fa2be47c1f2fc2f3eff167c9e57db9e346ee Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Mon, 30 Oct 2023 17:11:28 +0200
Subject: [PATCH] Don't output trivial congruence invariant (closes #1218)

---
 src/cdomains/intDomain.ml | 1 +
 1 file changed, 1 insertion(+)

diff --git a/src/cdomains/intDomain.ml b/src/cdomains/intDomain.ml
index 748df62300..3bc84ae676 100644
--- a/src/cdomains/intDomain.ml
+++ b/src/cdomains/intDomain.ml
@@ -3274,6 +3274,7 @@ struct
 
   let invariant_ikind e ik x =
     match x with
+    | x when is_top x -> Invariant.top ()
     | Some (c, m) when m =: Ints_t.zero ->
       if get_bool "witness.invariant.exact" then
         let c = Ints_t.to_bigint c in