1 ; COMMAND-LINE: --rewrite-rules --quiet
2 ;; Same than length.smt2 but the nil case is not a rewrite rule
3 ;; So here the rewrite rules have no guards length
8 ;; don't use a datatypes for currently focusing in uf
11 (declare-fun cons (Int list) list)
12 (declare-fun nil () list)
16 (declare-fun length (list) Int)
18 (assert (= (length nil) 0))
20 (assert (forall ((?e Int) (?l list)) (! (= (length (cons ?e ?l)) (+ 1 (length ?l))) :rewrite-rule)))
22 (declare-fun gen_cons (Int list) list)
24 (assert (forall ((?n Int) (?l list)) (! (=> (= ?n 0) (= (gen_cons ?n ?l) ?l)) :rewrite-rule)))
26 (assert (forall ((?n Int) (?l list)) (! (=> (> ?n 0) (= (gen_cons ?n ?l)
27 (gen_cons (- ?n 1) (cons 1 ?l)))) :rewrite-rule)))
29 (declare-fun n () Int)
31 (assert (not (= (length (gen_cons 20 nil)) 200)))