diff --git a/2025/project.clj b/2025/project.clj
index e46d80e..905cc83 100644
--- a/2025/project.clj
+++ b/2025/project.clj
@@ -10,5 +10,6 @@
                  [babashka/fs "0.5.23"]
                  [org.babashka/http-client "0.4.22"]
                  [org.clojure/core.match "1.1.0"]
-                 [clj-python/libpython-clj "2.026"]]
-  :source-paths ["src" "../shared/clj/src"])
+                 [clj-python/libpython-clj "2.025"]
+                 [tools.aqua/z3-turnkey "4.14.1"]]
+ :source-paths ["src" "../shared/clj/src"])
diff --git a/2025/src/day10.clj b/2025/src/day10.clj
index 9a0bee4..07e375e 100644
--- a/2025/src/day10.clj
+++ b/2025/src/day10.clj
@@ -1,26 +1,23 @@
 (ns day10
-  (:require input-manager
-            [core :refer [dbg]]
-            [clojure.math.combinatorics :as combo]
-            [clojure.string :as str]
-            [libpython-clj2.require :refer [require-python]]
-            [libpython-clj2.python :as py]))
+  (:require [clojure.math.combinatorics :as combo]
+            [input-manager])
+  (:import (com.microsoft.z3 BoolExpr Context Expr IntNum Optimize Optimize$Handle)))
 
 (defn parse-line [line]
   {:indicators (->> line
                     (drop 1)
                     (take-while (complement #{\]}))
                     (mapv (partial = \#)))
-   :buttons (->> line
-                 (re-seq #"\([\d,]+\)")
-                 (map #(map parse-long (re-seq #"\d+" %))))
-   :joltages (->> line
-                  (drop-while #(not= % \{))
-                  (drop 1)
-                  (take-while #(not= % \}))
-                  (apply str)
-                  (re-seq #"\d+")
-                  (mapv parse-long))})
+   :buttons    (->> line
+                    (re-seq #"\([\d,]+\)")
+                    (map #(map parse-long (re-seq #"\d+" %))))
+   :joltages   (->> line
+                    (drop-while #(not= % \{))
+                    (drop 1)
+                    (take-while #(not= % \}))
+                    (apply str)
+                    (re-seq #"\d+")
+                    (mapv parse-long))})
 
 (def input (map parse-line (input-manager/get-input 2025 10)))
 
@@ -39,51 +36,48 @@
 ;; part 1
 (apply + (map minimum-button-mashing input))
 
-;; clj-python setup
-(defmacro !   [self method & args] `(py/call-attr ~method ~self ~@args))
-(defmacro py=  [self & args] `(! "__eq__" ~self ~@args))
-(defmacro py>= [self & args] `(! "__ge__" ~self ~@args))
-(defmacro pysubscript  [self & args] `(! "__getitem__" ~self ~@args))
-
-;; z3 stuff
-(require-python :from (str (System/getenv "HOME") "/.local/lib/python3.13/site-packages/") '[z3 :as z3])
-(def Int z3/Int)
-(def Optimize z3/Optimize)
-(def Sum z3/Sum)
-(defn add-formulas! [opt [f & fs]]
-  (when f
-    (! "add" opt f)
-    (recur opt fs)))
-
 ;; part 2
 (->> input
      (map (fn [{:keys [joltages buttons]}]
-            (let [opt (Optimize)
+            (let [ctx (Context.)
+                  ^Optimize opt (.mkOptimize ctx)
                   bs (->> buttons
                           count
                           range
-                          (map #(Int (str "b" %))))
+                          (map #(.mkIntConst ctx (str "b" %))))
                   js (->> joltages
                           count
                           range
-                          (map #(Int (str "j" %))))]
-              (add-formulas! opt (for [idx (range (count joltages))]
-                                   (let [jn (nth js idx)
-                                         summation-args (->> buttons
-                                                             (map set)
-                                                             (map-indexed vector)
-                                                             (filter #(contains? (second %) idx))
-                                                             (map first)
-                                                             (map #(nth bs %)))]
-                                     (py= jn (apply Sum summation-args)))))
-              (add-formulas! opt (for [[idx joltage] (map-indexed vector joltages)]
-                                   (let [jn (nth js idx)]
-                                     (py= jn joltage))))
-              (add-formulas! opt (for [b bs] (py>= b 0)))
-              (! "minimize" opt (apply Sum bs))
-              (! "check" opt)
-              (let [model (! "model" opt)]
-                (->> (for [b bs] (! "as_long" (pysubscript model b)))
-                     (apply +))))))
+                          (map #(.mkIntConst ctx (str "j" %))))]
+              (.Add
+                opt
+                (into-array
+                  BoolExpr
+                  (for [idx (range (count joltages))]
+                    (let [jn (nth js idx)
+                          summation-args (->> buttons
+                                              (map set)
+                                              (map-indexed vector)
+                                              (filter #(contains? (second %) idx))
+                                              (map first)
+                                              (map #(nth bs %))
+                                              (into-array Expr)
+                                              (.mkAdd ctx))]
+                      (.mkEq ctx jn summation-args)))))
+              (.Add
+                opt
+                (into-array
+                  Expr
+                  (for [[idx joltage] (map-indexed vector joltages)]
+                    (let [jn (nth js idx)]
+                      (.mkEq ctx jn (.mkInt ctx (long joltage)))))))
+              (.Add
+                opt
+                (into-array
+                  Expr
+                  (for [b bs]
+                    (.mkGe ctx b (.mkInt ctx (long 0))))))
+              (let [^Optimize$Handle mx (.MkMinimize opt (.mkAdd ctx (into-array Expr bs)))]
+                (.Check opt (into-array Expr []))
+                (.getInt ^IntNum (.getLower mx))))))
      (apply +))
-