diff options
Diffstat (limited to 'test/regress/regress0/rewriterules/length_gen_010.smt2')
| -rw-r--r-- | test/regress/regress0/rewriterules/length_gen_010.smt2 | 10 |
1 files changed, 6 insertions, 4 deletions
diff --git a/test/regress/regress0/rewriterules/length_gen_010.smt2 b/test/regress/regress0/rewriterules/length_gen_010.smt2 index 7c7663b17..41cc61c9e 100644 --- a/test/regress/regress0/rewriterules/length_gen_010.smt2 +++ b/test/regress/regress0/rewriterules/length_gen_010.smt2 @@ -16,14 +16,16 @@ (assert (= (length nil) 0)) -(assert (forall ((?e Int) (?l list)) (! (= (length (cons ?e ?l)) (+ 1 (length ?l))) :rewrite-rule))) +;; (assert (forall ((?e Int) (?l list)) (! (= (length (cons ?e ?l)) (+ 1 (length ?l))) :rewrite-rule))) + +(assert-rewrite ((?e Int) (?l list)) () (length (cons ?e ?l)) (+ 1 (length ?l)) ()) (declare-fun gen_cons (Int list) list) -(assert (forall ((?n Int) (?l list)) (! (=> (= ?n 0) (= (gen_cons ?n ?l) ?l)) :rewrite-rule))) +(assert-rewrite ((?n Int) (?l list)) (= ?n 0) (gen_cons ?n ?l) (?l) ()) -(assert (forall ((?n Int) (?l list)) (! (=> (> ?n 0) (= (gen_cons ?n ?l) - (gen_cons (- ?n 1) (cons 1 ?l)))) :rewrite-rule))) +(assert-rewrite ((?n Int) (?l list)) (> ?n 0) (gen_cons ?n ?l) + (gen_cons (- ?n 1) (cons 1 ?l)) ()) (declare-fun n () Int) |