diff --git a/sledge/src/llair/exp.ml b/sledge/src/llair/exp.ml
index 36038c306..68ddd9eed 100644
--- a/sledge/src/llair/exp.ml
+++ b/sledge/src/llair/exp.ml
@@ -191,7 +191,10 @@ let rec invariant exp =
   | Reg {typ} | Nondet {typ} -> assert (Typ.is_sized typ)
   | Integer {data; typ} -> (
     match typ with
-    | Integer {bits} -> assert (Z.numbits data <= bits)
+    | Integer {bits} ->
+        (* data in −(2^(bits − 1)) to 2^(bits − 1) − 1 *)
+        let n = Z.shift_left Z.one (bits - 1) in
+        assert (Z.(Compare.(neg n <= data && data < n)))
     | Pointer _ -> assert (Z.equal Z.zero data)
     | _ -> assert false )
   | Float {typ} -> (
diff --git a/sledge/src/symbheap/term_test.ml b/sledge/src/symbheap/term_test.ml
index c1616931b..893864cd3 100644
--- a/sledge/src/symbheap/term_test.ml
+++ b/sledge/src/symbheap/term_test.ml
@@ -47,14 +47,16 @@ let%test_module _ =
         (Term.of_exp
            (Exp.eq Typ.bool
               (Exp.integer Typ.bool Z.minus_one)
-              (Exp.integer Typ.bool Z.one)))
+              (Exp.convert ~dst:Typ.bool ~src:Typ.siz
+                 (Exp.integer Typ.siz Z.one))))
 
     let%test "unsigned boolean overflow" =
       Term.is_true
         (Term.of_exp
            (Exp.uge Typ.bool
               (Exp.integer Typ.bool Z.minus_one)
-              (Exp.integer Typ.bool Z.one)))
+              (Exp.convert ~dst:Typ.bool ~src:Typ.siz
+                 (Exp.integer Typ.siz Z.one))))
 
     let%expect_test _ =
       pp (!42 + !13) ;