; header

(set-logic QF_LIA)

; initial variable declarations

(declare-fun var1 () Int)
(assert     (and
      (>= var1 0)
      (<= var1 7)
    ))
(declare-fun var1_post () Int)
(assert     (and
      (>= var1_post 0)
      (<= var1_post 7)
    ))
(declare-fun var2 () Int)
(assert     (and
      (>= var2 0)
      (<= var2 4)
    ))
(declare-fun var2_post () Int)
(assert     (and
      (>= var2_post 0)
      (<= var2_post 4)
    ))
(declare-fun var3 () Int)
(assert     (and
      (>= var3 0)
      (<= var3 4)
    ))
(declare-fun var3_post () Int)
(assert     (and
      (>= var3_post 0)
      (<= var3_post 4)
    ))
(declare-fun var4 () Int)
(assert     (and
      (>= var4 0)
      (<= var4 1)
    ))
(declare-fun var4_post () Int)
(assert     (and
      (>= var4_post 0)
      (<= var4_post 1)
    ))

(assert (not
(and
  (=
    var1
    7
  )
  (=
    var2
    0
  )
  (=
    var1_post
    2
  )
  (=
    var4_post
    1
  )
  (=
    var2_post
      var2
  )
  (=
    var3_post
      var3
  )
)
))

(assert
  (and
    (=
      var1
      0
    )
    (=
	var2
      0
    ) 
    (=
      var1_post
      2
    )
    (=
      var4_post
      1
    )
    (=
      var2_post
	var2
    )
    (=
      var3_post
	var3
    )

  )
)

; start check
(check-sat)
(get-model)
(exit)