diff --git a/src/arith/lra/simplex2.ml b/src/arith/lra/simplex2.ml
index fbd26f7a..15e2345b 100644
--- a/src/arith/lra/simplex2.ml
+++ b/src/arith/lra/simplex2.ml
@@ -404,10 +404,10 @@ module Make(Var: VAR)
       assert Erat.(sum = zero);
 
     done;
-    () (* TODO: more *)
+    ()
 
   (* for internal checking *)
-  let _check_invariants_internal self =
+  let[@inline] _check_invariants_internal self =
     if false (* FUDGE *) then _check_invariants self
 
   let[@inline] has_var_ (self:t) x : bool = V_map.mem x self.var_tbl
diff --git a/src/arith/tests/test_simplex2.ml b/src/arith/tests/test_simplex2.ml
index 90914926..79f68936 100644
--- a/src/arith/tests/test_simplex2.ml
+++ b/src/arith/tests/test_simplex2.ml
@@ -277,7 +277,7 @@ let check_sound =
   let ar =
     Step.(rand_for 0 300)
     |> QC.set_collect (fun pb -> if check_steps pb then "sat" else "unsat")
-    |> QC.set_stats steps_stats
+(*     |> QC.set_stats steps_stats *)
   in
   QC.Test.make ~long_factor:10 ~count:500 ~name:"simplex2_sound" ar prop_sound
 
@@ -287,6 +287,7 @@ let prop_invariants pb =
     add_steps simplex pb ~f:(fun () -> Spl._check_invariants simplex);
     Spl.check_exn simplex
    with Spl.E_unsat _ -> ());
+  Spl._check_invariants simplex;
   true
 
 let check_invariants =