loop_invariant.smt2

(set-logic HORN)

(declare-fun loopInvStart (Int Int Int Int) Bool)
(declare-fun loopHeader (Int Int Int Int) Bool)
(declare-fun loopBody (Int Int Int Int) Bool)
(declare-fun loopInvBlock1 (Int Int Int Int) Bool)
(declare-fun summaryLoopInv (Int Int Int Int) Bool)

(assert
(forall ( (nInit Int) (xInit Int) (nCur Int) (xCur Int) )
(loopInvStart nInit xInit nCur xCur)
))

(assert
(forall ( (nInit Int) (xInit Int) (nCur Int) (xCur Int) )
(=>
	(and
		(loopInvStart nInit xInit nCur xCur)
		(= xInit 0)
		(= xCur xInit)
		(>= nInit 0)
		(< nInit 256)
		(= nInit nCur)
	)
	(loopHeader nInit xInit nCur xCur)
)))

(assert
(forall ( (nInit Int) (xInit Int) (nCur Int) (xCur Int) )
(=>
	(and
		(loopHeader nInit xInit nCur xCur)
		(< xCur nCur)
	)
	(loopBody nInit xInit nCur xCur)
)))

(assert
(forall ( (nInit Int) (xInit Int) (nCur Int) (xCur Int) )
(=>
	(and
		(loopHeader nInit xInit nCur xCur)
		(>= xCur nCur)
	)
	(loopInvBlock1 nInit xInit nCur xCur)
)))

(assert
(forall ( (nInit Int) (xInit Int) (nCur Int) (xCur Int) )
(=>
	(loopBody nInit xInit nCur xCur)
	(loopHeader nInit xInit nCur (+ xCur 1))
)))

(assert
(forall ( (nInit Int) (xInit Int) (nCur Int) (xCur Int) )
(=>
	(and
		(loopInvBlock1 nInit xInit nCur xCur)
		(not (= xCur nCur))
	)
	false
)))

(assert
(forall ( (nInit Int) (xInit Int) (nCur Int) (xCur Int) )
(=>
	(and
		(loopInvBlock1 nInit xInit nCur xCur)
		(= xCur nCur)
	)
	(summaryLoopInv nInit xInit nCur xCur)
)))

(check-sat)
(get-model)