loop.smt2

; Horn encoding of the following pseudocode:
;
; assume x < y
; while (x < y) ++x;
; assert (x == y)
;
; We consider the CFG to be the following:
;
; Init -> LoopHeader
; LoopHeader -> LoopBody
; LoopHeader -> AfterLoop
; AfterLoop -> ErrorTarget
;
; We create a predicate for each CFG node above,
; where the arguments of a predicate are the variables in the
; scope of the CFG node it represents.
; All variables are bound (are local to a quantifier inside an assertion, no globals).
;
; A certain predicate is `true` if the CFG node it represents is reachable.
;
; We omit Init as a predicate because we can just
; encode `assume(x < y)` as the constraint `x < y`
; in the fact LoopHeader (it is always reachable).
;
; Then we basically ask the question, is `ErrorTarget` reachable?
;
; To run z3:
; z3 loop.smt2
;
; To run Eldarica:
; eld -sol -cex

(set-logic HORN)
(set-option :produce-proofs true)

(declare-const x Int)
(declare-const y Int)

(declare-fun loop_header (Int Int) Bool)
(declare-fun loop_body (Int Int) Bool)
(declare-fun after_loop (Int Int) Bool)
(declare-fun error_target () Bool)

; x < y => LoopHeader(x, y)
(assert (forall ((x Int) (y Int))
(=>
	(< x y)
	(loop_header x y)
)
))

; LoopHeader(x, y) && x < y => LoopBody(x, y)
(assert (forall ((x Int) (y Int))
(=>
	(and
		(loop_header x y)
		(< x y)
	)
	(loop_body x y)
)
))

; LoopHeader(x, y) && x >= y => AfterLoop(x, y)
(assert (forall ((x Int) (y Int))
(=>
	(and
		(loop_header x y)
		(>= x y)
	)
	(after_loop x y)
)
))

; LoopBody(x, y) => LoopHeader(x + 1, y)
(assert (forall ((x Int) (y Int))
(=>
	(loop_body x y)
	; Uncomment below to make it succeed
	(loop_header (+ x 1) y)
	; Uncomment below to make it fail
	;(loop_header (+ x 2) y)
)
))

; AfterLoop(x, y) && x != y => ErrorTarget()
(assert (forall ((x Int) (y Int))
(=>
	(and
		(after_loop x y)
		(not (= x y))
	)
	error_target
)
))

; ErrorTarget => false
; We're saying we don't want to reach `ErrorTarget`.
(assert
	(=> error_target false)
)

(check-sat)
(get-proof)
(get-model)