; synthèse d'invariant de programme ; on déclare le symbole non interprété de relation Invar (declare-fun Invar (Int Int) Bool) ; équation (58) : la relation Invar est un invariant de boucle (assert (forall (( x Int ) ( y Int )) (=> (and (Invar x y) (< x 10)) (Invar (+ x 2) (+ y 1))))) ; équation (59) : la relation Invar est vraie initialement (assert (Invar 0 1)) ; équation (60) : l'assertion finale est vérifiée (assert (forall (( x Int ) ( y Int )) (=> (and (Invar x y) (>= x 10)) (< y 10)))) ; appel au solveur (check-sat-using (then qe smt)) (get-model) (exit)