; @author Jonas Schöpf ; this LCTRS needs splitting in order to be analyzed properly (format LCTRS :smtlib 2.6) (theory Ints) (fun f (-> Int Int)) (fun g (-> Int Int)) (fun a Int) (fun c Int) (rule c (f x) :guard (and (<= 1 x) (<= x 10))) (rule c (g x) :guard (and (<= 1 x) (<= x 10))) (rule (f x) a :guard (and (<= 1 x) (<= x 5))) (rule (f x) a :guard (and (<= 6 x) (<= x 10))) (rule (g x) a :guard (and (<= 1 x) (<= x 5))) (rule (g x) a :guard (and (<= 6 x) (<= x 10)))