;; Timeout (alors qu'il devrait trouver un contrex) (set-logic HORN) (declare-datatypes ((nat 0) (natlist 0)) ( ( (z) (s (pred nat)) ) ( (nil) (cons (hd nat) (tl natlist)) ) ) ) (define-fun-rec append ((l1 natlist) (l2 natlist)) natlist ( match l1 ( (nil l2) ((cons h1 t1) (cons h1 (append t1 l2))) ) ) ) (define-fun-rec not_null ((l natlist)) Bool ( match l ( (nil false) ( (cons x ll) true) ) ) ) (assert (forall ((l1 natlist) (l2 natlist)) (=> (not_null l1) (not_null (append l1 l2))))) (check-sat)