diff --git a/2024/ruby/day_13.rb b/2024/ruby/day_13.rb
new file mode 100644
index 0000000..85a795f
--- /dev/null
+++ b/2024/ruby/day_13.rb
@@ -0,0 +1,63 @@
+require "bundler/inline"
+
+gemfile do
+  source "https://rubygems.org"
+  gem "z3"
+end
+
+input = DATA.read
+
+machines = input.split("\n\n")
+  .map {|machine| machine.scan(/\d+/).map(&:to_i) }
+
+wins = ->(machine) {
+  ax, ay = machine[0,2]
+  bx, by = machine[2,2]
+  cx, cy = machine[4,2]
+
+  (0..cx/ax).filter_map {|a|
+    b = (cx - a * ax) / bx.to_f
+    if a * ax + b.to_i * bx == cx && a * ay + b.to_i * by == cy
+      [a, b.to_i]
+    else
+      nil
+    end
+  }.sort_by {|a,b| a + b }
+}
+
+pp machines.map { wins[_1].first }.compact.sum { 3 * _1 + _2 }
+
+require "z3"
+
+machines.each do |machine|
+  machine[4,2] = machine[4,2].map { _1 + 10_000_000_000_000 }
+end
+
+def wins(machine)
+  return enum_for(__method__, machine) unless block_given?
+
+  ax, ay = machine[0,2]
+  bx, by = machine[2,2]
+  cx, cy = machine[4,2]
+
+  solutions = []
+  loop do
+    a = Z3.Int("a")
+    b = Z3.Int("b")
+    solver = Z3::Solver.new
+    solver.assert cx == a*ax + b*bx
+    solver.assert cy == a*ay + b*by
+    solutions.each do |a_s, b_s|
+      solver.assert a != a_s
+    end
+    return unless solver.satisfiable?
+
+    model = solver.model
+    solutions << [model[a].to_i, model[b].to_i]
+    yield solutions.last
+  end
+end
+
+pp machines.flat_map {|m| wins(m).sort_by { _1 + _2 } }.reject(&:empty?).sum { 3 * _1 + _2 }
+
+__END__