test/regress/regress1/rewriterules/length_gen_020_sat.smt2

   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
   4
   5 (set-logic AUFLIA)
   6 (set-info :status sat)
   7
   8 ;; don't use a datatypes for currently focusing in uf
   9 (declare-sort list 0)
  10
  11 (declare-fun cons (Int list) list)
  12 (declare-fun nil  ()         list)
  13
  14
  15 ;;define length
  16 (declare-fun length (list) Int)
  17
  18 (assert (= (length nil) 0))
  19
  20 (assert (forall ((?e Int) (?l list)) (! (= (length (cons ?e ?l)) (+ 1 (length ?l))) :rewrite-rule)))
  21
  22 (declare-fun gen_cons (Int list) list)
  23
  24 (assert (forall ((?n Int) (?l list)) (! (=> (= ?n 0) (= (gen_cons ?n ?l) ?l)) :rewrite-rule)))
  25
  26 (assert (forall ((?n Int) (?l list)) (! (=> (> ?n 0) (= (gen_cons ?n ?l)
  27         (gen_cons (- ?n 1) (cons 1 ?l)))) :rewrite-rule)))
  28
  29 (declare-fun n () Int)
  30
  31 (assert (not (= (length (gen_cons 20 nil)) 200)))
  32
  33 (check-sat)
  34
  35 (exit)