(set-logic QF_LIA)
(set-option :produce-models true)
(set-option :timeout 60000)

(define-fun weight ((enabled Bool)) Int
  (ite enabled 1 0))