Advertisement
Not a member of Pastebin yet?
Sign Up,
it unlocks many cool features!
- ; 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)
Advertisement
Add Comment
Please, Sign In to add comment
Advertisement