Skip to content

Instantly share code, notes, and snippets.

Embed
What would you like to do?
S-Corp tax optimization with the Z3 Theorem Prover
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;
;; Solo freelancer's S-Corp tax optimization
;;
;; Assumes an unmarried single-shareholder and tons of other stuff.
;; I'm not a tax professional, no guarantees here, probably typos, etc. Come on!
;; Run with https://github.com/Z3Prover/z3
;;
;; See also my notes at https://kevinlynagh.com/financial-plan/
;;;;;;;;;;;;;;
;; Projections
(define-const company-gross Real 500000.0)
(define-const company-expenses Real 20000.0)
;;;;;;;;;;;;
;; Utils
(define-fun max ((x Real) (y Real)) Real
(ite (< x y) y x))
(define-fun min ((x Real) (y Real)) Real
(ite (> x y) y x))
;;print output as decimals rather than fractions
(set-option :pp.decimal true)
;;;;;;;;;;;;;
;; W2
(define-const ss-wage-base Real
147000.0)
(declare-const wages-box-1 Real)
(declare-const ss-wages-box-3 Real)
(declare-const medicare-wages-box-5 Real)
(declare-const elective-deferral-box-12a Real)
(assert (>= wages-box-1 elective-deferral-box-12a))
(assert (<= elective-deferral-box-12a 20500.0))
(assert (= ss-wages-box-3 (min ss-wage-base wages-box-1)))
(assert (= medicare-wages-box-5 (+ wages-box-1 elective-deferral-box-12a)))
;;;;;;;;;;;;;;;;;;;;;;;;
;; FICA tax liabilites
;; see https://www.nerdwallet.com/article/taxes/fica-tax-withholding
(define-const ss-tax-rate Real
0.062)
(define-const ss-tax-employer Real
(* ss-tax-rate (max ss-wages-box-3 ss-wage-base)))
(define-const ss-tax-employee Real
(* ss-tax-rate (max ss-wages-box-3 ss-wage-base)))
(define-const medicare-tax-rate Real 0.0145)
(define-const medicare-tax-employer Real
(* medicare-tax-rate medicare-wages-box-5))
(define-const medicare-additional-tax-rate Real 0.009)
(define-const medicare-additional-tax-threshold Real 200000.0)
(define-const medicare-tax-employee Real
(+ (* medicare-tax-rate medicare-wages-box-5)
(* medicare-additional-tax-rate
(max 0 (- medicare-wages-box-5 medicare-additional-tax-threshold)))))
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; 1120 S - US Income Tax Return for an S Corporation
;; line 6
(define-const total-income Real
company-gross)
;; line 7
(define-const officer-compensation Real
;;would include company paid health insurance here too, if I had any this year
(+ wages-box-1
elective-deferral-box-12a))
;; line 17
(declare-const profit-sharing Real)
(assert (<= 0 profit-sharing (* 0.25 officer-compensation)))
(assert (>= 61000 ;;https://www.investopedia.com/retirement/401k-contribution-limits/
(+ elective-deferral-box-12a
profit-sharing)))
;; line 12
(define-const taxes-and-licenses Real
(+ ss-tax-employer
medicare-tax-employer
;;futa-tax
420.0))
;; line 19
(define-const other-deductions Real
company-expenses)
;; line 20
(define-const total-deductions Real
(+ officer-compensation
taxes-and-licenses
profit-sharing
other-deductions))
;; line 21
(define-const ordinary-business-income Real
(- total-income
total-deductions))
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; 1040 - US Individual Income Tax Return
;; line 13; see also 8995-A
(define-const qualified-business-income-deduction Real
;; For single taxpayers with taxable income more than $207,500 or married taxpayers with taxable income more than $415,000, the qualified business income deduction can’t exceed the greater of two amounts:
;; 50% of the W-2 wages paid by the business, or
;; 25% of the W-2 wages paid by the business plus 2.5% of the original cost depreciable assets used in the business.
(min (* 0.50 officer-compensation)
;;I'm business income is qualified because company is not an SSTB (specified service trade or business)
(* 0.2 ordinary-business-income)))
;; line 15, roughly.
(define-const personal-taxable-income Real
(+ wages-box-1
ordinary-business-income
(- qualified-business-income-deduction)))
(define-const personal-federal-tax-liability Real
;;https://taxfoundation.org/2022-tax-brackets/
(+ (* 0.10 (max 0 (- (min 10275 personal-taxable-income) 0)))
(* 0.12 (max 0 (- (min 41775 personal-taxable-income) 10275)))
(* 0.22 (max 0 (- (min 89075 personal-taxable-income) 41775)))
(* 0.24 (max 0 (- (min 170050 personal-taxable-income) 89075)))
(* 0.32 (max 0 (- (min 215950 personal-taxable-income) 170050)))
(* 0.35 (max 0 (- (min 539900 personal-taxable-income) 215950)))
(* 0.37 (max 0 (- personal-taxable-income 539900)))))
;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; Total tax liability
(define-const annual-tax-liability Real
(+ ss-tax-employer
ss-tax-employee
medicare-tax-employer
medicare-tax-employee
personal-federal-tax-liability))
(define-const retirement-tax-liability Real
;;assume 25% future tax rate when I withdraw from 401k
(* 0.25 (+ elective-deferral-box-12a profit-sharing)))
;;;;;;;;;;;;;;;;;;;;;;;;;;
;; Solve and print results
(minimize (+ annual-tax-liability
retirement-tax-liability))
(check-sat)
(eval wages-box-1)
(eval elective-deferral-box-12a)
(eval profit-sharing)
(eval qualified-business-income-deduction)
;; Double check via: https://www.ceclaw.com/wp-content/uploads/2017/01/Section-199A-Pass-Through-Deduction-and-the-Magic-Number.pdf
;; "So long as a qualified trade or business owner pays himself or herself a salary (or pays combined salaries to multiple employees) equal to 28.571% of the business’ QBI (calculated without taking into account salaries), the highest possible Section 199A deduction will be available."
;; (eval (/ officer-compensation (+ ordinary-business-income officer-compensation)))
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment