Don't output trivial congruence invariant (closes #1218)

goblint · Oct 30, 2023 · a2a4fa2 · a2a4fa2
1 parent 2c0a08f
commit a2a4fa2
Showing 1 changed file with 1 addition and 0 deletions.
diff --git 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