S-Corp tax optimization with the Z3 Theorem Prover

taxes.smt2

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;
;;  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)))