diff --git a/src/intsolver/sidekick_intsolver.ml b/src/intsolver/sidekick_intsolver.ml
index f5e4fd1d..5ba5e62d 100644
--- a/src/intsolver/sidekick_intsolver.ml
+++ b/src/intsolver/sidekick_intsolver.ml
@@ -96,10 +96,12 @@ module Make(A : ARG)
     let empty : t = T_map.empty
 
     let pp out (self:t) : unit =
-      let pp_pair out (t,z) = Fmt.fprintf out "%a · %a" Z.pp z A.pp_term t in
+      let pp_pair out (t,z) =
+        if Z.(z = one) then A.pp_term out t
+        else Fmt.fprintf out "%a · %a" Z.pp z A.pp_term t in
       if is_empty self then Fmt.string out "0"
-      else Fmt.fprintf out "(@[+@ %a@])"
-          Fmt.(iter ~sep:(return "@ ") pp_pair) (T_map.to_iter self)
+      else Fmt.fprintf out "(@[%a@])"
+          Fmt.(iter ~sep:(return "@ + ") pp_pair) (T_map.to_iter self)
 
     let iter = T_map.iter
     let return t : t = T_map.add t Z.one empty
@@ -288,8 +290,12 @@ module Make(A : ARG)
           Sat m (* TODO: model *)
 
         | Some (t, _) ->
-          Log.debugf 30 (fun k->k "(@[intsolver.elim-var@ %a@])" A.pp_term t);
-          assert false
+          self.vars <- T_map.remove t self.vars;
+          Log.debugf 30
+            (fun k->k "(@[intsolver.elim-var@ %a@ :remaining %d@])"
+                A.pp_term t (T_map.cardinal self.vars));
+
+          assert false (* TODO *)
 
       end
 
diff --git a/src/tests/run_tests.ml b/src/tests/run_tests.ml
index 27035e82..834d28f5 100644
--- a/src/tests/run_tests.ml
+++ b/src/tests/run_tests.ml
@@ -1,17 +1,18 @@
 
 let tests : unit Alcotest.test list =
   List.flatten @@ [
-    [Sidekick_test_simplex.tests];
     [Sidekick_test_intsolver.tests];
+    [Sidekick_test_simplex.tests];
     [Sidekick_test_minicc.tests];
     Sidekick_test_util.tests;
   ]
 
 let props =
   List.flatten
-    [ Sidekick_test_simplex.props;
-      Sidekick_test_util.props;
+    [
       Sidekick_test_intsolver.props;
+      Sidekick_test_simplex.props;
+      Sidekick_test_util.props;
     ]
 
 let () =
@@ -21,6 +22,7 @@ let () =
     let argv= Array.of_list (a0::tl) in
     Alcotest.run ~argv ~and_exit:true "arith tests" tests;
   | a0::"qcheck"::tl ->
+    Sidekick_util.Log.set_debug 50;
     let argv= Array.of_list (a0::tl) in
     CCFormat.set_color_default true;
     QCheck_runner.run_tests_main ~argv props