diff --git a/src/kernel_services/ast_queries/cil.ml b/src/kernel_services/ast_queries/cil.ml
index da1da6f3bd0ebef888a2fa38efb47cd793abf1db..21881ba48f900997cfef04f8a704fb3d99a2c067 100644
--- a/src/kernel_services/ast_queries/cil.ml
+++ b/src/kernel_services/ast_queries/cil.ml
@@ -5310,12 +5310,12 @@ let rec constFoldTermNodeAtTop = function
   | TSizeOfE _ | TAlignOfE _ ->
     assert false (* sizeof/alignof of logic types are rejected
                     by typing anyway. *)
-  | TUnOp (op, { term_node = t1 }) as t ->
+  | TUnOp (op, ({ term_node = n1 } as t1)) ->
     begin
       let constFoldTermUnOp int_unop =
-        match constFoldTermNodeAtTop t1 with
+        match constFoldTermNodeAtTop n1 with
         | TConst (Integer (i, _)) -> TConst (Integer (int_unop i, None))
-        | _ -> t
+        | n1 -> TUnOp (op, {t1 with term_node = n1})
       in
       match op with
       | Neg -> constFoldTermUnOp Integer.neg
@@ -5324,13 +5324,17 @@ let rec constFoldTermNodeAtTop = function
                   (fun i -> if Integer.is_zero i
                     then Integer.one else Integer.zero)
     end
-  | TBinOp (op, {term_node = t1}, {term_node = t2}) as t ->
+  | TBinOp (op, ({term_node = n1} as t1), ({term_node = n2} as t2)) ->
     begin
+      let n1 = constFoldTermNodeAtTop n1 in
+      let n2 = constFoldTermNodeAtTop n2 in
       let constFoldTermBinOp int_bop =
-        match constFoldTermNodeAtTop t1, constFoldTermNodeAtTop t2 with
+        match n1, n2 with
         | TConst (Integer (i1, _)), TConst (Integer (i2, _)) ->
           TConst (Integer (int_bop i1 i2, None))
-        | _ -> t
+        | n1, n2 ->
+          TBinOp (op, {t1 with term_node = n1}, {t2 with term_node = n2})
+
       in
       match op with
       | PlusA -> constFoldTermBinOp Integer.add
@@ -5342,7 +5346,8 @@ let rec constFoldTermNodeAtTop = function
       | BAnd -> constFoldTermBinOp Integer.logand
       | BXor -> constFoldTermBinOp Integer.logxor
       | BOr -> constFoldTermBinOp Integer.logor
-      | _ -> t
+      | _ ->
+        TBinOp (op, {t1 with term_node = n1}, {t2 with term_node = n2})
     end
   | t -> t