diff --git a/README.md b/README.md
index 4e905fa..fa89906 100644
--- a/README.md
+++ b/README.md
@@ -1,17 +1,5 @@
 # Advent of Code in OCaml
 
-## Install Dependencies
-
-```
-opam install . --deps-only
-```
-
-## Lock Dependencies
-
-```
-opam lock . --direct-only
-```
-
 ## Run
 
 ```
@@ -37,3 +25,15 @@ dune test
 ```
 opam switch create ./ ocaml-base-compiler.5.1.1 --deps-only
 ```
+
+## Install New Dependencies
+
+```
+opam install . --deps-only
+```
+
+## Lock New Dependencies
+
+```
+opam lock . --direct-only
+```
diff --git a/aoc.opam b/aoc.opam
index be8eed2..2fa7680 100644
--- a/aoc.opam
+++ b/aoc.opam
@@ -11,6 +11,8 @@ depends: [
   "ocaml"
   "ocaml-lsp-server"
   "ocamlformat"
+  "odig"
+  "odoc"
   "utop"
   "angstrom"
   "core"
@@ -19,8 +21,8 @@ depends: [
   "core_unix"
   "pcre"
   "ppx_jane"
+  "z3"
   "zarith"
-  "odoc" {with-doc}
 ]
 build: [
   ["dune" "subst"] {dev}
diff --git a/aoc.opam.locked b/aoc.opam.locked
index 6b8099c..d70fd0c 100644
--- a/aoc.opam.locked
+++ b/aoc.opam.locked
@@ -13,14 +13,16 @@ depends: [
   "core_bench" {= "v0.16.0"}
   "core_kernel" {= "v0.16.0"}
   "core_unix" {= "v0.16.0"}
-  "domainslib" {= "0.5.0"}
   "dune" {= "3.12.1"}
   "ocaml" {= "5.1.1"}
   "ocaml-lsp-server" {= "1.17.0"}
   "ocamlformat" {= "0.26.1"}
+  "odig" {= "0.0.9"}
+  "odoc" {= "2.4.0"}
   "pcre" {= "7.5.0"}
   "ppx_jane" {= "v0.16.0"}
   "utop" {= "2.13.1"}
+  "z3" {= "4.12.4"}
   "zarith" {= "1.13"}
 ]
 build: [
@@ -37,4 +39,4 @@ build: [
     "@doc" {with-doc}
   ]
 ]
-dev-repo: "git+https://github.com/drewolson/aoc-ocaml.git"
\ No newline at end of file
+dev-repo: "git+https://github.com/drewolson/aoc-ocaml.git"
diff --git a/bin/main.ml b/bin/main.ml
index e203c00..8aa08e2 100644
--- a/bin/main.ml
+++ b/bin/main.ml
@@ -6,7 +6,7 @@ let year_arg =
   Command.Arg_type.create (fun year_str ->
     match Int.of_string_opt year_str with
     | Some year when Set.mem years year -> year
-    | _ -> failwith "Year must be [2022, 2023]")
+    | _ -> failwith "Year must be in [2022, 2023]")
 ;;
 
 let day_arg =
diff --git a/dune-project b/dune-project
index 6b9672e..8541c62 100644
--- a/dune-project
+++ b/dune-project
@@ -21,6 +21,8 @@
     ocaml
     ocaml-lsp-server
     ocamlformat
+    odig
+    odoc
     utop
 
     angstrom
@@ -30,4 +32,5 @@
     core_unix
     pcre
     ppx_jane
+    z3
     zarith))
diff --git a/lib/year2023/day24.ml b/lib/year2023/day24.ml
index 1a12395..0ccf644 100644
--- a/lib/year2023/day24.ml
+++ b/lib/year2023/day24.ml
@@ -1,3 +1,6 @@
+module A = Z3.Arithmetic
+module B = Z3.Boolean
+module I = Z3.Arithmetic.Integer
 module P = Util.Parser
 open P.Syntax
 
@@ -28,17 +31,13 @@ let stone_p =
 
 let stones_p = P.sep_by1 P.end_of_line stone_p
 
-let to_line { x; y; dx; dy } =
-  let open Q in
-  let x1 = x in
-  let y1 = y in
-  let x2 = x1 + dx in
-  let y2 = y1 + dy in
-  { a = y1 - y2; b = x2 - x1; c = ~-((x1 * y2) - (x2 * y1)) }
-;;
-
 let in_test_area target (h1, h2) =
   let open Q in
+  let to_line { x; y; dx; dy } =
+    let x' = x + dx in
+    let y' = y + dy in
+    { a = y - y'; b = x' - x; c = ~-((x * y') - (x' * y)) }
+  in
   let in_range (a, b) v = a <= v && v <= b in
   let sign f = ~$(compare f ~$0) in
   let in_future h1 h2 x y =
@@ -60,32 +59,61 @@ let in_test_area target (h1, h2) =
     in_range target x && in_range target y && in_future h1 h2 x y)
 ;;
 
-let make_matrix stones ~f =
-  let m = List.map stones ~f in
-  List.take m 4
-  |> List.map ~f:(fun d ->
-    List.zip_exn d (List.last_exn m) |> List.map ~f:(fun (a, b) -> Q.(a - b)))
-  |> List.map ~f:Array.of_list
-  |> Array.of_list
-;;
-
-let elim m =
-  let l = Array.length m in
-  for i = 0 to l - 1 do
-    let t = m.(i).(i) in
-    m.(i) <- Array.map m.(i) ~f:(fun x -> Q.(x / t));
-    for j = i + 1 to l - 1 do
-      let t = m.(j).(i) in
-      m.(j) <- Array.mapi m.(j) ~f:(fun k x -> Q.(x - (t * m.(i).(k))))
-    done
-  done;
-  for i = l - 1 downto 0 do
-    for j = 0 to i - 1 do
-      let t = m.(j).(i) in
-      m.(j) <- Array.mapi m.(j) ~f:(fun k x -> Q.(x - (t * m.(i).(k))))
-    done
-  done;
-  Array.map m ~f:(fun r -> Array.last r)
+let solve_system stones =
+  let check_sat_exn s =
+    match Z3.Solver.check s [] with
+    | UNKNOWN -> failwith "UNKNOWN"
+    | UNSATISFIABLE -> failwith "UNSATISFIABLE"
+    | SATISFIABLE -> ()
+  in
+  let get_model_exn s =
+    check_sat_exn s;
+    s |> Z3.Solver.get_model |> Option.value_exn
+  in
+  let ctx = Z3.mk_context [ "model", "true"; "proof", "false" ] in
+  let zero = I.mk_numeral_i ctx 0 in
+  let x = I.mk_const_s ctx "x" in
+  let y = I.mk_const_s ctx "y" in
+  let z = I.mk_const_s ctx "z" in
+  let dx = I.mk_const_s ctx "dx" in
+  let dy = I.mk_const_s ctx "dy" in
+  let dz = I.mk_const_s ctx "dz" in
+  let s = Z3.Solver.mk_simple_solver ctx in
+  stones
+  |> Util.List.take ~n:3
+  |> List.iteri ~f:(fun i h ->
+    let t = I.mk_const_s ctx (Printf.sprintf "t%i" i) in
+    Z3.Solver.add
+      s
+      [ A.mk_gt ctx t zero
+      ; B.mk_eq
+          ctx
+          (A.mk_add ctx [ x; A.mk_mul ctx [ dx; t ] ])
+          (A.mk_add
+             ctx
+             [ I.mk_numeral_i ctx (Q.to_int h.x)
+             ; A.mk_mul ctx [ I.mk_numeral_i ctx (Q.to_int h.dx); t ]
+             ])
+      ; B.mk_eq
+          ctx
+          (A.mk_add ctx [ y; A.mk_mul ctx [ dy; t ] ])
+          (A.mk_add
+             ctx
+             [ I.mk_numeral_i ctx (Q.to_int h.y)
+             ; A.mk_mul ctx [ I.mk_numeral_i ctx (Q.to_int h.dy); t ]
+             ])
+      ; B.mk_eq
+          ctx
+          (A.mk_add ctx [ z; A.mk_mul ctx [ dz; t ] ])
+          (A.mk_add
+             ctx
+             [ I.mk_numeral_i ctx (Q.to_int h.z)
+             ; A.mk_mul ctx [ I.mk_numeral_i ctx (Q.to_int h.dz); t ]
+             ])
+      ]);
+  let m = get_model_exn s in
+  let result = A.mk_add ctx [ x; y; z ] in
+  Z3.Model.eval m result false |> Option.value_exn |> Z3.Expr.to_string |> Int.of_string
 ;;
 
 let part1 target input =
@@ -96,19 +124,4 @@ let part1 target input =
   |> List.length
 ;;
 
-(* all credit to https://github.com/tckmn/polyaoc-2023/blob/97689dc6b5ff38c557cd885b10be425e14928958/24/rb/24.rb#L22 *)
-let part2 input =
-  let open Q in
-  let stones = P.parse_exn stones_p input in
-  let a =
-    make_matrix stones ~f:(fun h ->
-      [ ~-(h.dy); h.dx; h.y; ~-(h.x); (h.y * h.dx) - (h.x * h.dy) ])
-  in
-  let b =
-    make_matrix stones ~f:(fun h ->
-      [ ~-(h.dy); h.dz; h.y; ~-(h.z); (h.y * h.dz) - (h.z * h.dy) ])
-  in
-  let r1 = elim a in
-  let r2 = elim b in
-  r1.(0) + r1.(1) + r2.(0) |> Q.to_int
-;;
+let part2 input = input |> P.parse_exn stones_p |> solve_system
diff --git a/lib/year2023/dune b/lib/year2023/dune
index 6f2807f..647df47 100644
--- a/lib/year2023/dune
+++ b/lib/year2023/dune
@@ -7,6 +7,7 @@
     ppx_jane
     pcre
     util
+    z3
     zarith)
   (preprocess
     (pps ppx_jane))