; trap(x) holds iff Q_x is a trap
(define-fun trap ((x1 Bool) (x2 Bool) (x3 Bool) (x4 Bool)) Bool
  (and
    (=> (or x1 x2) (or x1))
    (=> (or x1) (or x1 x2))
    (=> (or x2) (or x4))
    (=> (or x4) (or x2 x3 x4))
    (=> (or x4) (or x1 x4))
  )
)

; mintrap(x) holds iff Q_x is a minimal trap
(define-fun mintrap ((x1 Bool) (x2 Bool) (x3 Bool) (x4 Bool)) Bool
  (and
    (trap x1 x2 x3 x4)                                        ; Q_x is a trap
    (or x1 x2 x3 x4)                                          ; Q_x is non empty
    (forall ((y1 Bool) (y2 Bool) (y3 Bool) (y4 Bool))         ; Every strict subset of Q_x is not a trap
      (=>
        (and
          (or y1 y2 y3 y4)                                    ; Q_y is non empty
          (=> y1 x1) (=> y2 x2) (=> y3 x3) (=> y4 x4)         ; Q_y subset of Q_y
          (or (and (not y1) x1) (and (not y2) x2)             ; Q_y != Q_x
              (and (not y3) x3) (and (not y4) x4))
        )
        (not (trap y1 y2 y3 y4))                              ; Q(y) is not a trap
      )
    )
  )
)

; constraints(x, M) holds iff "Q_x marks M_0" implies "Q_x marks M"
(define-fun constraints ((x1 Bool) (x2 Bool) (x3 Bool) (x4 Bool)
                         (m1 Int) (m2 Int) (m3 Int) (m4 Int)) Bool
  (=>
    (or x1 x4)          ; Q_x is marked in M_0, i.e. contains place p1 or p4
    (or                 ; Some place of Q_x is marked in M
      (and x1 (> m1 0))
      (and x2 (> m2 0))
      (and x3 (> m3 0))
      (and x4 (> m4 0))
    )
  )
)

; mreach(m) holds iff there is a solution of the marking equation
; from (2, 0, 0, 1) thats leads to m
(define-fun mreach ((m1 Int) (m2 Int) (m3 Int) (m4 Int)) Bool
  (exists ((t1 Int) (t2 Int) (t3 Int) (t4 Int) (t5 Int))
    (and
      (>= t1 0)
      (>= t2 0)
      (>= t3 0)
      (>= t4 0)
      (>= t5 0)
      (= m1 (+ 2 t1 (- 0 t2) t5))
      (= m2 (+ (* -2 t1) t2 (- 0 t3) t4))
      (= m3 t4)
      (= m4 (+ 1 t3 (- 0 t4) (- 0 t5)))
    )
  )
)

; There exists a solution to the marking equation
(declare-const m1 Int)
(declare-const m2 Int)
(declare-const m3 Int)
(declare-const m4 Int)

(assert (>= m1 0))
(assert (= m2 2))
(assert (>= m3 1))
(assert (>= m4 0))
(assert (mreach m1 m2 m3 m4))

; The reachable marking satisfies minimal trap constraints
;; (In general, non minimal trap constraints may be necessary
;;  to disprove reachability, but here it's not the case.
;;  You may simply replace "mintrap" by "trap" below.)
(assert
  (forall ((x1 Bool) (x2 Bool) (x3 Bool) (x4 Bool))
    (=>
      (mintrap x1 x2 x3 x4)
      (constraints x1 x2 x3 x4 m1 m2 m3 m4)      
    )
  )
)

(check-sat)