diff --git a/2023/24/sol.z3 b/2023/24/sol.z3
deleted file mode 100644
index a3cd3fa..0000000
--- a/2023/24/sol.z3
+++ /dev/null
@@ -1,60 +0,0 @@
-(declare-fun t0 () Int)
-(declare-fun vx0 () Int)
-(declare-fun x0 () Int)
-(declare-fun vy0 () Int)
-(declare-fun y0 () Int)
-(declare-fun vz0 () Int)
-(declare-fun z0 () Int)
-(declare-fun t1 () Int)
-(declare-fun t2 () Int)
-(declare-fun t3 () Int)
-(declare-fun t4 () Int)
-(declare-fun t5 () Int)
-(declare-fun t6 () Int)
-(declare-fun t7 () Int)
-(declare-fun t8 () Int)
-(declare-fun t9 () Int)
-(assert (= (+ x0 (* (- 61) t0) (* vx0 t0)) 184964585341884))
-(assert (= (+ y0 (* (- 469) t0) (* vy0 t0)) 113631924395348))
-(assert (= (+ z0 (* 390 t0) (* vz0 t0)) 401845630841620))
-(assert (>= t0 0))
-(assert (= (+ x0 (* (- 46) t1) (* vx0 t1)) 331877282121819))
-(assert (= (+ y0 (* 106 t1) (* vy0 t1)) 365938348079363))
-(assert (= (+ z0 (* (- 24) t1) (* vz0 t1)) 314507465806130))
-(assert (>= t1 0))
-(assert (= (+ x0 (* (- 105) t2) (* vx0 t2)) 263775277465044))
-(assert (= (+ y0 (* 170 t2) (* vy0 t2)) 418701236136888))
-(assert (= (+ z0 (* (- 307) t2) (* vz0 t2)) 52607746821705))
-(assert (>= t2 0))
-(assert (= (+ x0 (* (- 46) t3) (* vx0 t3)) 208356602267478))
-(assert (= (+ y0 (* (- 8) t3) (* vy0 t3)) 274354112299498))
-(assert (= (+ z0 (* 49 t3) (* vz0 t3)) 294235176347885))
-(assert (>= t3 0))
-(assert (= (+ x0 (* 28 t4) (* vx0 t4)) 215069209934964))
-(assert (= (+ y0 (* (- 48) t4) (* vy0 t4)) 263266623283188))
-(assert (= (+ z0 (* 120 t4) (* vz0 t4)) 304961521854129))
-(assert (>= t4 0))
-(assert (= (+ x0 (* (- 101) t5) (* vx0 t5)) 218821711924084))
-(assert (= (+ y0 (* 181 t5) (* vy0 t5)) 386143011380798))
-(assert (= (+ z0 (* 189 t5) (* vz0 t5)) 415191763621655))
-(assert (>= t5 0))
-(assert (= (+ x0 (* 54 t6) (* vx0 t6)) 451773868335257))
-(assert (= (+ y0 (* 246 t6) (* vy0 t6)) 516705765114825))
-(assert (= (+ z0 (* 128 t6) (* vz0 t6)) 478982876413032))
-(assert (>= t6 0))
-(assert (= (+ x0 (* 106 t7) (* vx0 t7)) 160266893683207))
-(assert (= (+ y0 (* 238 t7) (* vy0 t7)) 318090322227659))
-(assert (= (+ z0 (* (- 26) t7) (* vz0 t7)) 233527333051300))
-(assert (>= t7 0))
-(assert (= (+ x0 (* (- 117) t8) (* vx0 t8)) 133382790359204))
-(assert (= (+ y0 (* (- 233) t8) (* vy0 t8)) 248866187487128))
-(assert (= (+ z0 (* 203 t8) (* vz0 t8)) 271295536804269))
-(assert (>= t8 0))
-(assert (= (+ x0 (* (- 180) t9) (* vx0 t9)) 126081027693345))
-(assert (= (+ y0 (* 398 t9) (* vy0 t9)) 357221115260331))
-(assert (= (+ z0 (* (- 420) t9) (* vz0 t9)) 166079877492738))
-(assert (>= t9 0))
-
-(check-sat)
-(get-model)
-(eval (+ x0 y0 z0))
\ No newline at end of file
diff --git a/2023/24/sol2.ml b/2023/24/sol2.ml
index dc6c457..cb22efb 100644
--- a/2023/24/sol2.ml
+++ b/2023/24/sol2.ml
@@ -2,6 +2,7 @@
 
 open! Core
 
+let debug = false
 let pat = Re.(compile (seq [ opt (char '-'); rep1 digit ]))
 
 let input =
@@ -26,7 +27,7 @@ let make_rules i (px, py, pz, vx, vy, vz) ~context ~x0 ~y0 ~z0 ~vx0 ~vy0 ~vz0 =
 
 let main () =
   let context = Z3.mk_context [] in
-  let solver = Z3.Solver.mk_simple_solver context in
+  let solver = Z3.Solver.mk_solver context None in
   let x0, y0, z0, vx0, vy0, vz0 =
     ( Z3.Arithmetic.Integer.mk_const_s context "x0"
     , Z3.Arithmetic.Integer.mk_const_s context "y0"
@@ -41,12 +42,12 @@ let main () =
       ~f:(make_rules ~context ~x0 ~y0 ~z0 ~vx0 ~vy0 ~vz0)
   in
   Z3.Solver.add solver rules;
-  print_endline (Z3.Solver.to_string solver);
+  if debug then print_endline (Z3.Solver.to_string solver);
   match Z3.Solver.check solver [] with
   | UNSATISFIABLE | UNKNOWN -> raise_s [%message "no solution"]
   | SATISFIABLE ->
     let model = Z3.Solver.get_model solver |> Option.value_exn in
-    print_endline (Z3.Model.to_string model);
+    if debug then print_endline (Z3.Model.to_string model);
     let ans =
       let get var =
         Z3.Model.get_const_interp_e model var
@@ -59,6 +60,4 @@ let main () =
     print_s [%sexp (ans : int)]
 ;;
 
-(* TODO: Why is this so much slower than printing the SMT and then plugging it
-   into z3 at the command line? *)
 let () = main ()