From 4643949ff4f1586935dfc2607931f26604422b50 Mon Sep 17 00:00:00 2001 From: =?utf8?q?Fran=C3=A7ois=20Bobot?= Date: Fri, 30 Nov 2012 11:35:02 +0000 Subject: [PATCH] fix the syntax of assert-rewrite/-propagation/-reduction by putting the pattern first just after the bindings Do it before the release in order to not break user files later --- src/parser/smt2/Smt2.g | 4 +- .../regress0/rewriterules/datatypes2.smt2 | 16 +-- .../regress0/rewriterules/datatypes3.smt2 | 16 +-- .../rewriterules/datatypes_clark.smt2 | 112 ++++++++-------- .../regress0/rewriterules/length_gen_010.smt2 | 8 +- .../regress0/rewriterules/native_arrays.smt2 | 4 +- .../reachability_back_to_the_future.smt2 | 32 ++--- .../reachability_bbttf_eT_arrays.smt2 | 124 +++++++++--------- .../regress0/rewriterules/relation.smt2 | 6 +- .../set_A_new_fast_tableau-base.smt2 | 52 ++++---- .../set_A_new_fast_tableau-base_sat.smt2 | 52 ++++---- ...smt => why3_vstte10_max_sum_harness2.smt2} | 0 ... => why3_vstte10_max_sum_harness2_rr.smt2} | 0 ...smt => why3_vstte10_max_sum_harness3.smt2} | 0 ... => why3_vstte10_max_sum_harness3_rr.smt2} | 0 15 files changed, 212 insertions(+), 214 deletions(-) rename test/regress/regress0/rewriterules/{why3_vstte10_max_sum_harness2.smt => why3_vstte10_max_sum_harness2.smt2} (100%) rename test/regress/regress0/rewriterules/{why3_vstte10_max_sum_harness2_rr.smt => why3_vstte10_max_sum_harness2_rr.smt2} (100%) rename test/regress/regress0/rewriterules/{why3_vstte10_max_sum_harness3.smt => why3_vstte10_max_sum_harness3.smt2} (100%) rename test/regress/regress0/rewriterules/{why3_vstte10_max_sum_harness3_rr.smt => why3_vstte10_max_sum_harness3_rr.smt2} (100%) diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index 39149ec89..87cf2083d 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -532,9 +532,9 @@ rewriterulesCommand[CVC4::Command*& cmd] } bvl = MK_EXPR(kind::BOUND_VAR_LIST, args); } + LPAREN_TOK ( pattern[expr] { triggers.push_back( expr ); } )* RPAREN_TOK LPAREN_TOK (termList[guards,expr])? RPAREN_TOK term[head, expr2] term[body, expr2] - LPAREN_TOK ( pattern[expr] { triggers.push_back( expr ); } )* RPAREN_TOK { args.clear(); args.push_back(head); @@ -573,10 +573,10 @@ rewriterulesCommand[CVC4::Command*& cmd] } bvl = MK_EXPR(kind::BOUND_VAR_LIST, args); } + LPAREN_TOK ( pattern[expr] { triggers.push_back( expr ); } )* RPAREN_TOK LPAREN_TOK (termList[guards,expr])? RPAREN_TOK LPAREN_TOK (termList[heads,expr])? RPAREN_TOK term[body, expr2] - LPAREN_TOK ( pattern[expr] { triggers.push_back( expr ); } )* RPAREN_TOK { args.clear(); /* heads */ diff --git a/test/regress/regress0/rewriterules/datatypes2.smt2 b/test/regress/regress0/rewriterules/datatypes2.smt2 index 993cd2002..277ddc3ae 100644 --- a/test/regress/regress0/rewriterules/datatypes2.smt2 +++ b/test/regress/regress0/rewriterules/datatypes2.smt2 @@ -14,21 +14,21 @@ ;;;;;;;;;;;;;;;;;;;; ;; injective -(declare-fun inj1 (list) elt) +(declare-fun inj11 (list) elt) (assert (forall ((?e elt) (?l list)) - (! (! (=> true (=> true (= (inj1 (cons1 ?e ?l)) ?e))) :pattern ((cons1 ?e ?l)) ) :rewrite-rule) )) + (! (! (=> true (=> true (= (inj11 (cons1 ?e ?l)) ?e))) :pattern ((cons1 ?e ?l)) ) :rewrite-rule) )) -(declare-fun inj2 (list) list) +(declare-fun inj12 (list) list) (assert (forall ((?e elt) (?l list)) - (! (! (=> true (=> true (= (inj2 (cons1 ?e ?l)) ?l))) :pattern ((cons1 ?e ?l)) ) :rewrite-rule) )) + (! (! (=> true (=> true (= (inj12 (cons1 ?e ?l)) ?l))) :pattern ((cons1 ?e ?l)) ) :rewrite-rule) )) -(declare-fun inj1 (list) elt) +(declare-fun inj21 (list) elt) (assert (forall ((?e elt) (?l list)) - (! (! (=> true (=> true (= (inj1 (cons2 ?e ?l)) ?e))) :pattern ((cons2 ?e ?l)) ) :rewrite-rule) )) + (! (! (=> true (=> true (= (inj21 (cons2 ?e ?l)) ?e))) :pattern ((cons2 ?e ?l)) ) :rewrite-rule) )) -(declare-fun inj2 (list) list) +(declare-fun inj22 (list) list) (assert (forall ((?e elt) (?l list)) - (! (! (=> true (=> true (= (inj2 (cons2 ?e ?l)) ?l))) :pattern ((cons2 ?e ?l)) ) :rewrite-rule) )) + (! (! (=> true (=> true (= (inj22 (cons2 ?e ?l)) ?l))) :pattern ((cons2 ?e ?l)) ) :rewrite-rule) )) ;;;;;;;;;;;;;;;;;;;; diff --git a/test/regress/regress0/rewriterules/datatypes3.smt2 b/test/regress/regress0/rewriterules/datatypes3.smt2 index dc3c8e20c..1ec5dcbc4 100644 --- a/test/regress/regress0/rewriterules/datatypes3.smt2 +++ b/test/regress/regress0/rewriterules/datatypes3.smt2 @@ -14,21 +14,21 @@ ;;;;;;;;;;;;;;;;;;;; ;; injective -(declare-fun inj1 (list) elt) +(declare-fun inj11 (list) elt) (assert (forall ((?e elt) (?l list)) - (! (! (=> true (=> true (= (inj1 (cons1 ?e ?l)) ?e))) :pattern ((cons1 ?e ?l)) ) :rewrite-rule) )) + (! (! (=> true (=> true (= (inj11 (cons1 ?e ?l)) ?e))) :pattern ((cons1 ?e ?l)) ) :rewrite-rule) )) -(declare-fun inj2 (list) list) +(declare-fun inj12 (list) list) (assert (forall ((?e elt) (?l list)) - (! (! (=> true (=> true (= (inj2 (cons1 ?e ?l)) ?l))) :pattern ((cons1 ?e ?l)) ) :rewrite-rule) )) + (! (! (=> true (=> true (= (inj12 (cons1 ?e ?l)) ?l))) :pattern ((cons1 ?e ?l)) ) :rewrite-rule) )) -(declare-fun inj1 (list) elt) +(declare-fun inj21 (list) elt) (assert (forall ((?e elt) (?l list)) - (! (! (=> true (=> true (= (inj1 (cons2 ?e ?l)) ?e))) :pattern ((cons2 ?e ?l)) ) :rewrite-rule) )) + (! (! (=> true (=> true (= (inj21 (cons2 ?e ?l)) ?e))) :pattern ((cons2 ?e ?l)) ) :rewrite-rule) )) -(declare-fun inj2 (list) list) +(declare-fun inj22 (list) list) (assert (forall ((?e elt) (?l list)) - (! (! (=> true (=> true (= (inj2 (cons2 ?e ?l)) ?l))) :pattern ((cons2 ?e ?l)) ) :rewrite-rule) )) + (! (! (=> true (=> true (= (inj22 (cons2 ?e ?l)) ?l))) :pattern ((cons2 ?e ?l)) ) :rewrite-rule) )) ;;;;;;;;;;;;;;;;;;;; diff --git a/test/regress/regress0/rewriterules/datatypes_clark.smt2 b/test/regress/regress0/rewriterules/datatypes_clark.smt2 index f1e61a901..19163f49d 100644 --- a/test/regress/regress0/rewriterules/datatypes_clark.smt2 +++ b/test/regress/regress0/rewriterules/datatypes_clark.smt2 @@ -18,13 +18,13 @@ (declare-fun inj1 (nat) nat) (assert-propagation((?x1 nat)) - () () (= (inj1 (succ ?x1)) ?x1) (((succ ?x1))) ) + (((succ ?x1))) () () (= (inj1 (succ ?x1)) ?x1) ) ;;;;;;;;;;;;;;;;;;;; ;; projection (declare-fun pred (nat) nat) -(assert-rewrite ((?x1 nat)) () (pred (succ ?x1)) ?x1 () ) +(assert-rewrite ((?x1 nat)) () () (pred (succ ?x1)) ?x1 ) (assert (= (pred zero) zero)) @@ -32,34 +32,34 @@ ;; test (declare-fun is_succ (nat) Bool) (assert (= (is_succ zero) false)) -(assert-propagation ((?x1 nat)) () () (= (is_succ (succ ?x1)) true) (((succ ?x1))) ) +(assert-propagation ((?x1 nat)) (((succ ?x1))) () () (= (is_succ (succ ?x1)) true) ) -(assert-propagation ((?x1 nat)) () ((is_succ ?x1)) (= ?x1 (succ (pred ?x1))) (((pred ?x1)))) +(assert-propagation ((?x1 nat)) (((pred ?x1))) () ((is_succ ?x1)) (= ?x1 (succ (pred ?x1)))) (declare-fun is_zero (nat) Bool) (assert (= (is_zero zero) true)) -(assert-propagation ((?x1 nat)) () ((is_zero ?x1)) (= ?x1 zero) ()) +(assert-propagation ((?x1 nat)) () () ((is_zero ?x1)) (= ?x1 zero)) ;;; directrr -(assert-rewrite ((?x1 nat)) () (is_succ (succ ?x1)) true () ) -(assert-rewrite ((?x1 nat)) () (is_zero (succ ?x1)) false () ) +(assert-rewrite ((?x1 nat)) () () (is_succ (succ ?x1)) true ) +(assert-rewrite ((?x1 nat)) () () (is_zero (succ ?x1)) false ) ;;;;;;;;;;;;;;;;;;;; ;; distinct -(assert-propagation ((?x1 nat)) () ((is_zero ?x1)) (not (is_succ ?x1)) () ) -(assert-propagation ((?x1 nat)) () ((is_succ ?x1)) (not (is_zero ?x1)) () ) -(assert-propagation ((?x1 nat)) () ((not (is_zero ?x1))) (is_succ ?x1) () ) -(assert-propagation ((?x1 nat)) () ((not (is_succ ?x1))) (is_zero ?x1) () ) +(assert-propagation ((?x1 nat)) () () ((is_zero ?x1)) (not (is_succ ?x1)) ) +(assert-propagation ((?x1 nat)) () () ((is_succ ?x1)) (not (is_zero ?x1)) ) +(assert-propagation ((?x1 nat)) () () ((not (is_zero ?x1))) (is_succ ?x1) ) +(assert-propagation ((?x1 nat)) () () ((not (is_succ ?x1))) (is_zero ?x1) ) ;;;;;;;;;;;;;;;;;;; ;; case-split -(assert-propagation ((?x1 nat)) () () (or (is_zero ?x1) (is_succ ?x1)) (((pred ?x1))) ) +(assert-propagation ((?x1 nat)) (((pred ?x1))) () () (or (is_zero ?x1) (is_succ ?x1)) ) ;;;;;;;;;;;;;;;;;;; ;; non-cyclic (declare-fun size_nat (nat) Real) -(assert-propagation ((?x1 nat)) () () (> (size_nat (succ ?x1)) (size_nat ?x1)) (((succ ?x1))) ) +(assert-propagation ((?x1 nat)) (((succ ?x1))) () () (> (size_nat (succ ?x1)) (size_nat ?x1)) ) @@ -83,22 +83,22 @@ ;; injective (declare-fun inj2 (list) tree) -(assert-propagation ((?x1 tree) (?x2 list)) () () (= (inj2 (cons ?x1 ?x2)) ?x1) (((cons ?x1 ?x2))) ) +(assert-propagation ((?x1 tree) (?x2 list)) (((cons ?x1 ?x2))) () () (= (inj2 (cons ?x1 ?x2)) ?x1) ) (declare-fun inj3 (list) list) -(assert-propagation ((?x1 tree) (?x2 list)) () () (= (inj3 (cons ?x1 ?x2)) ?x2) (((cons ?x1 ?x2))) ) +(assert-propagation ((?x1 tree) (?x2 list)) (((cons ?x1 ?x2))) () () (= (inj3 (cons ?x1 ?x2)) ?x2) ) ;;;;;;;;;;;;;;;;;;;; ;; projection (declare-fun car (list) tree) -(assert-rewrite ((?x1 tree) (?x2 list)) () (car (cons ?x1 ?x2)) ?x1 ()) +(assert-rewrite ((?x1 tree) (?x2 list)) () () (car (cons ?x1 ?x2)) ?x1) (assert (= (car null) (node null))) (declare-fun cdr (list) list) -(assert-rewrite ((?x1 tree) (?x2 list)) () (cdr (cons ?x1 ?x2)) ?x2 ()) +(assert-rewrite ((?x1 tree) (?x2 list)) () () (cdr (cons ?x1 ?x2)) ?x2) (assert (= (cdr null) null)) @@ -106,36 +106,36 @@ ;; test (declare-fun is_cons (list) Bool) (assert (= (is_cons null) false)) -(assert-propagation ((?x1 tree) (?x2 list)) () () (= (is_cons (cons ?x1 ?x2)) true) (((cons ?x1 ?x2))) ) +(assert-propagation ((?x1 tree) (?x2 list)) (((cons ?x1 ?x2))) () () (= (is_cons (cons ?x1 ?x2)) true) ) -(assert-propagation ((?x1 list)) () ((is_cons ?x1)) (= ?x1 (cons (car ?x1) (cdr ?x1))) (((car ?x1))) ) -(assert-propagation ((?x1 list)) () ((is_cons ?x1)) (= ?x1 (cons (car ?x1) (cdr ?x1))) (((cdr ?x1))) ) +(assert-propagation ((?x1 list)) (((car ?x1))) () ((is_cons ?x1)) (= ?x1 (cons (car ?x1) (cdr ?x1))) ) +(assert-propagation ((?x1 list)) (((cdr ?x1))) () ((is_cons ?x1)) (= ?x1 (cons (car ?x1) (cdr ?x1))) ) (declare-fun is_null (list) Bool) (assert (= (is_null null) true)) -(assert-propagation ((?x1 list)) () ((is_null ?x1)) (= (car ?x1) (node null)) (((car ?x1))) ) -(assert-propagation ((?x1 list)) () ((is_null ?x1)) (= (cdr ?x1) null) (((cdr ?x1))) ) +(assert-propagation ((?x1 list)) (((car ?x1))) () ((is_null ?x1)) (= (car ?x1) (node null)) ) +(assert-propagation ((?x1 list)) (((cdr ?x1))) () ((is_null ?x1)) (= (cdr ?x1) null) ) -(assert-propagation ((?x1 list)) () ((is_null ?x1)) (= ?x1 null) ()) +(assert-propagation ((?x1 list)) () () ((is_null ?x1)) (= ?x1 null)) ;;; directrr -(assert-rewrite ((?x1 tree) (?x2 list)) () (is_cons (cons ?x1 ?x2)) true ()) -(assert-rewrite ((?x1 tree) (?x2 list)) () (is_null (cons ?x1 ?x2)) false ()) +(assert-rewrite ((?x1 tree) (?x2 list)) () () (is_cons (cons ?x1 ?x2)) true) +(assert-rewrite ((?x1 tree) (?x2 list)) () () (is_null (cons ?x1 ?x2)) false) ;;;;;;;;;;;;;;;;;;;; ;; distinct -(assert-propagation ((?x1 list)) () ((is_null ?x1)) (not (is_cons ?x1)) () ) -(assert-propagation ((?x1 list)) () ((is_cons ?x1)) (not (is_null ?x1)) () ) -(assert-propagation ((?x1 list)) () ((not (is_null ?x1))) (is_cons ?x1) () ) -(assert-propagation ((?x1 list)) () ((not (is_cons ?x1))) (is_null ?x1) () ) +(assert-propagation ((?x1 list)) () () ((is_null ?x1)) (not (is_cons ?x1)) ) +(assert-propagation ((?x1 list)) () () ((is_cons ?x1)) (not (is_null ?x1)) ) +(assert-propagation ((?x1 list)) () () ((not (is_null ?x1))) (is_cons ?x1) ) +(assert-propagation ((?x1 list)) () () ((not (is_cons ?x1))) (is_null ?x1) ) ;;;;;;;;;;;;;;;;;;; ;; case-split -(assert-propagation ((?x1 list)) () () (or (is_null ?x1) (is_cons ?x1)) (((car ?x1))) ) -(assert-propagation ((?x1 list)) () () (or (is_null ?x1) (is_cons ?x1)) (((cdr ?x1))) ) +(assert-propagation ((?x1 list)) (((car ?x1))) () () (or (is_null ?x1) (is_cons ?x1)) ) +(assert-propagation ((?x1 list)) (((cdr ?x1))) () () (or (is_null ?x1) (is_cons ?x1)) ) ;;;;;;;;;;;;;;; ;; tree @@ -144,61 +144,61 @@ ;; injective (declare-fun inj4 (tree) list) -(assert-propagation ((?x1 list)) () () (= (inj4 (node ?x1)) ?x1) (((node ?x1))) ) +(assert-propagation ((?x1 list)) (((node ?x1))) () () (= (inj4 (node ?x1)) ?x1) ) (declare-fun inj5 (tree) nat) -(assert-propagation ((?x1 nat)) () () (= (inj5 (leaf ?x1)) ?x1) (((leaf ?x1))) ) +(assert-propagation ((?x1 nat)) (((leaf ?x1))) () () (= (inj5 (leaf ?x1)) ?x1) ) ;;;;;;;;;;;;;;;;;;;; ;; projection (declare-fun children (tree) list) -(assert-rewrite ((?x1 list)) () (children (node ?x1)) ?x1 () ) -(assert-rewrite ((?x1 nat)) () (children (leaf ?x1)) null () ) +(assert-rewrite ((?x1 list)) () () (children (node ?x1)) ?x1 ) +(assert-rewrite ((?x1 nat)) () () (children (leaf ?x1)) null ) (declare-fun data (tree) nat) -(assert-rewrite ((?x1 nat)) () (data (leaf ?x1)) ?x1 () ) -(assert-rewrite ((?x1 list)) () (data (node ?x1)) zero () ) +(assert-rewrite ((?x1 nat)) () () (data (leaf ?x1)) ?x1 ) +(assert-rewrite ((?x1 list)) () () (data (node ?x1)) zero ) ;;;;;;;;;;;;;;;;;;; ;; test (declare-fun is_node (tree) Bool) -(assert-propagation ((?x1 list)) () () (= (is_node (node ?x1)) true) (((node ?x1))) ) +(assert-propagation ((?x1 list)) (((node ?x1))) () () (= (is_node (node ?x1)) true) ) -(assert-propagation ((?x1 tree)) () ((is_node ?x1)) (= ?x1 (node (children ?x1))) (((children ?x1))) ) -(assert-propagation ((?x1 tree)) () ((is_node ?x1)) (= (data ?x1) zero) (((data ?x1))) ) +(assert-propagation ((?x1 tree)) (((children ?x1))) () ((is_node ?x1)) (= ?x1 (node (children ?x1))) ) +(assert-propagation ((?x1 tree)) (((data ?x1))) () ((is_node ?x1)) (= (data ?x1) zero) ) (declare-fun is_leaf (tree) Bool) -(assert-propagation ((?x1 nat)) () () (= (is_leaf (leaf ?x1)) true) (((leaf ?x1))) ) -(assert-propagation ((?x1 tree)) () ((is_leaf ?x1)) (= ?x1 (leaf (data ?x1))) (((data ?x1))) ) -(assert-propagation ((?x1 tree)) () ((is_leaf ?x1)) (= (children ?x1) null) (((children ?x1))) ) +(assert-propagation ((?x1 nat)) (((leaf ?x1))) () () (= (is_leaf (leaf ?x1)) true) ) +(assert-propagation ((?x1 tree)) (((data ?x1))) () ((is_leaf ?x1)) (= ?x1 (leaf (data ?x1))) ) +(assert-propagation ((?x1 tree)) (((children ?x1))) () ((is_leaf ?x1)) (= (children ?x1) null) ) ;;; directrr -(assert-rewrite ((?x1 list)) () (is_node (node ?x1)) true () ) -(assert-rewrite ((?x1 list)) () (is_leaf (node ?x1)) false () ) -(assert-rewrite ((?x1 nat)) () (is_leaf (leaf ?x1)) true () ) -(assert-rewrite ((?x1 nat)) () (is_node (leaf ?x1)) false () ) +(assert-rewrite ((?x1 list)) () () (is_node (node ?x1)) true ) +(assert-rewrite ((?x1 list)) () () (is_leaf (node ?x1)) false ) +(assert-rewrite ((?x1 nat)) () () (is_leaf (leaf ?x1)) true ) +(assert-rewrite ((?x1 nat)) () () (is_node (leaf ?x1)) false ) ;;;;;;;;;;;;;;;;;;;; ;; distinct -(assert-propagation ((?x1 tree)) () ((is_node ?x1)) (not (is_leaf ?x1)) () ) -(assert-propagation ((?x1 tree)) () ((is_leaf ?x1)) (not (is_node ?x1)) () ) -(assert-propagation ((?x1 tree)) () ((not (is_node ?x1))) (is_leaf ?x1) () ) -(assert-propagation ((?x1 tree)) () ((not (is_leaf ?x1))) (is_node ?x1) () ) +(assert-propagation ((?x1 tree)) () () ((is_node ?x1)) (not (is_leaf ?x1)) ) +(assert-propagation ((?x1 tree)) () () ((is_leaf ?x1)) (not (is_node ?x1)) ) +(assert-propagation ((?x1 tree)) () () ((not (is_node ?x1))) (is_leaf ?x1) ) +(assert-propagation ((?x1 tree)) () () ((not (is_leaf ?x1))) (is_node ?x1) ) ;;;;;;;;;;;;;;;;;;; ;; case-split -(assert-propagation ((?x1 tree)) () () (or (is_node ?x1) (is_leaf ?x1)) (((children ?x1))) ) -(assert-propagation ((?x1 tree)) () () (or (is_node ?x1) (is_leaf ?x1)) (((data ?x1))) ) +(assert-propagation ((?x1 tree)) (((children ?x1))) () () (or (is_node ?x1) (is_leaf ?x1)) ) +(assert-propagation ((?x1 tree)) (((data ?x1))) () () (or (is_node ?x1) (is_leaf ?x1)) ) ;;;;;;;;;;;;;;;;;; ;; non-cyclic (declare-fun size_list (list) Real) (declare-fun size_tree (tree) Real) -(assert-propagation ((?x1 tree) (?x2 list)) () () (and (> (size_list (cons ?x1 ?x2)) (size_tree ?x1)) (> (size_list (cons ?x1 ?x2)) (size_list ?x2))) (((cons ?x1 ?x2))) ) -(assert-propagation ((?x1 list)) () () (> (size_tree (node ?x1)) (size_list ?x1)) (((node ?x1))) ) -(assert-propagation ((?x1 nat)) () () (> (size_tree (leaf ?x1)) (size_nat ?x1)) (((leaf ?x1))) ) +(assert-propagation ((?x1 tree) (?x2 list)) (((cons ?x1 ?x2))) () () (and (> (size_list (cons ?x1 ?x2)) (size_tree ?x1)) (> (size_list (cons ?x1 ?x2)) (size_list ?x2))) ) +(assert-propagation ((?x1 list)) (((node ?x1))) () () (> (size_tree (node ?x1)) (size_list ?x1)) ) +(assert-propagation ((?x1 nat)) (((leaf ?x1))) () () (> (size_tree (leaf ?x1)) (size_nat ?x1)) ) diff --git a/test/regress/regress0/rewriterules/length_gen_010.smt2 b/test/regress/regress0/rewriterules/length_gen_010.smt2 index 41cc61c9e..052f5905b 100644 --- a/test/regress/regress0/rewriterules/length_gen_010.smt2 +++ b/test/regress/regress0/rewriterules/length_gen_010.smt2 @@ -18,14 +18,14 @@ ;; (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)) ()) +(assert-rewrite ((?e Int) (?l list)) () () (length (cons ?e ?l)) (+ 1 (length ?l))) (declare-fun gen_cons (Int list) list) -(assert-rewrite ((?n Int) (?l list)) (= ?n 0) (gen_cons ?n ?l) (?l) ()) +(assert-rewrite ((?n Int) (?l list)) () (= ?n 0) (gen_cons ?n ?l) (?l)) -(assert-rewrite ((?n Int) (?l list)) (> ?n 0) (gen_cons ?n ?l) - (gen_cons (- ?n 1) (cons 1 ?l)) ()) +(assert-rewrite ((?n Int) (?l list)) () (> ?n 0) (gen_cons ?n ?l) + (gen_cons (- ?n 1) (cons 1 ?l))) (declare-fun n () Int) diff --git a/test/regress/regress0/rewriterules/native_arrays.smt2 b/test/regress/regress0/rewriterules/native_arrays.smt2 index 1be13167d..b7d19b612 100644 --- a/test/regress/regress0/rewriterules/native_arrays.smt2 +++ b/test/regress/regress0/rewriterules/native_arrays.smt2 @@ -10,8 +10,8 @@ ;;A dumb predicate for a simple example (declare-fun P (Element) Bool) -(assert-rewrite ((?i1 Index) (?i2 Index) (?e Element) (?a (Array Index Element))) () - (P (select (store ?a ?i1 ?e) ?i2)) true () ) +(assert-rewrite ((?i1 Index) (?i2 Index) (?e Element) (?a (Array Index Element))) () () + (P (select (store ?a ?i1 ?e) ?i2)) true ) (declare-fun a1 () (Array Index Element)) (declare-fun a2 () (Array Index Element)) diff --git a/test/regress/regress0/rewriterules/reachability_back_to_the_future.smt2 b/test/regress/regress0/rewriterules/reachability_back_to_the_future.smt2 index 7cd61738b..13f7234e9 100644 --- a/test/regress/regress0/rewriterules/reachability_back_to_the_future.smt2 +++ b/test/regress/regress0/rewriterules/reachability_back_to_the_future.smt2 @@ -8,32 +8,32 @@ (declare-fun Rf (elt elt elt) Bool) ;;eq -(assert-propagation ((?x elt)) () () (or (= ?x ?x) (not (= ?x ?x))) ((?x)) ) +(assert-propagation ((?x elt)) ((?x)) () () (or (= ?x ?x) (not (= ?x ?x))) ) ;; reflexive -(assert-propagation ((?x elt)) () () (Rf ?x ?x ?x) ((?x)) ) +(assert-propagation ((?x elt)) ((?x)) () () (Rf ?x ?x ?x) ) ;; step -(assert-propagation ((?x elt)) () () (Rf ?x (f ?x) (f ?x)) (((f ?x))) ) +(assert-propagation ((?x elt)) (((f ?x))) () () (Rf ?x (f ?x) (f ?x)) ) ;; reach -(assert-propagation ((?x1 elt)(?x2 elt)) () ((Rf ?x1 ?x2 ?x2)) (or (= ?x1 ?x2) (Rf ?x1 (f ?x1) ?x2)) (((f ?x1))) ) +(assert-propagation ((?x1 elt)(?x2 elt)) (((f ?x1))) () ((Rf ?x1 ?x2 ?x2)) (or (= ?x1 ?x2) (Rf ?x1 (f ?x1) ?x2)) ) ;; cycle -(assert-propagation ((?x1 elt)(?x2 elt)) ((= (f ?x1) ?x1)) ((Rf ?x1 ?x2 ?x2)) (= ?x1 ?x2) (((f ?x1))) ) +(assert-propagation ((?x1 elt)(?x2 elt)) (((f ?x1))) ((= (f ?x1) ?x1)) ((Rf ?x1 ?x2 ?x2)) (= ?x1 ?x2) ) ;; sandwich -(assert-propagation ((?x1 elt)(?x2 elt)) () ((Rf ?x1 ?x2 ?x1)) (= ?x1 ?x2) () ) +(assert-propagation ((?x1 elt)(?x2 elt)) () () ((Rf ?x1 ?x2 ?x1)) (= ?x1 ?x2) ) ;; order1 -(assert-propagation ((?x1 elt)(?x2 elt)(?x3 elt)) () ((Rf ?x1 ?x2 ?x2)(Rf ?x1 ?x3 ?x3)) - (or (Rf ?x1 ?x2 ?x3) (Rf ?x1 ?x3 ?x2)) () ) +(assert-propagation ((?x1 elt)(?x2 elt)(?x3 elt)) () () ((Rf ?x1 ?x2 ?x2)(Rf ?x1 ?x3 ?x3)) + (or (Rf ?x1 ?x2 ?x3) (Rf ?x1 ?x3 ?x2)) ) ;; order2 -(assert-propagation ((?x1 elt)(?x2 elt)(?x3 elt)) () ((Rf ?x1 ?x2 ?x3)) - (and (Rf ?x1 ?x2 ?x2) (Rf ?x2 ?x3 ?x3)) () ) +(assert-propagation ((?x1 elt)(?x2 elt)(?x3 elt)) () () ((Rf ?x1 ?x2 ?x3)) + (and (Rf ?x1 ?x2 ?x2) (Rf ?x2 ?x3 ?x3)) ) ;; transitive1 -(assert-propagation ((?x1 elt)(?x2 elt)(?x3 elt)) () ((Rf ?x1 ?x2 ?x2)(Rf ?x2 ?x3 ?x3)) - (Rf ?x1 ?x3 ?x3) () ) +(assert-propagation ((?x1 elt)(?x2 elt)(?x3 elt)) () () ((Rf ?x1 ?x2 ?x2)(Rf ?x2 ?x3 ?x3)) + (Rf ?x1 ?x3 ?x3) ) ;; transitive2 -(assert-propagation ((?x0 elt)(?x1 elt)(?x2 elt)(?x3 elt)) () ((Rf ?x0 ?x1 ?x2)(Rf ?x1 ?x3 ?x2)) - (and (Rf ?x0 ?x1 ?x3) (Rf ?x0 ?x3 ?x2)) () ) +(assert-propagation ((?x0 elt)(?x1 elt)(?x2 elt)(?x3 elt)) () () ((Rf ?x0 ?x1 ?x2)(Rf ?x1 ?x3 ?x2)) + (and (Rf ?x0 ?x1 ?x3) (Rf ?x0 ?x3 ?x2)) ) ;;transitive3 -(assert-propagation ((?x0 elt)(?x1 elt)(?x2 elt)(?x3 elt)) () ((Rf ?x0 ?x1 ?x2)(Rf ?x0 ?x3 ?x1)) - (and (Rf ?x0 ?x3 ?x2) (Rf ?x3 ?x1 ?x2)) () ) +(assert-propagation ((?x0 elt)(?x1 elt)(?x2 elt)(?x3 elt)) () () ((Rf ?x0 ?x1 ?x2)(Rf ?x0 ?x3 ?x1)) + (and (Rf ?x0 ?x3 ?x2) (Rf ?x3 ?x1 ?x2)) ) (declare-fun e1 () elt) (declare-fun e2 () elt) diff --git a/test/regress/regress0/rewriterules/reachability_bbttf_eT_arrays.smt2 b/test/regress/regress0/rewriterules/reachability_bbttf_eT_arrays.smt2 index b7069536a..8f30f38a5 100644 --- a/test/regress/regress0/rewriterules/reachability_bbttf_eT_arrays.smt2 +++ b/test/regress/regress0/rewriterules/reachability_bbttf_eT_arrays.smt2 @@ -8,97 +8,97 @@ (declare-fun R (mem elt elt elt) Bool) ;; reflexive -(assert-propagation ((?m mem)(?x elt)) () () (R ?m ?x ?x ?x) ((?m ?x)) ) +(assert-propagation ((?m mem)(?x elt)) ((?m ?x)) () () (R ?m ?x ?x ?x) ) ;; step -(assert-propagation ((?m mem)(?x elt)) () () (R ?m ?x (select ?m ?x) (select ?m ?x)) (((select ?m ?x))) ) -;; (assert-propagation ((?x elt)) () () (Rf ?x (f ?x) (f ?x)) (((Rf ?x (f ?x) (f ?x)))) ) -;; (assert-propagation ((?x elt)) () () (=> true (Rf ?x (f ?x) (f ?x))) (((f ?x))) ) +(assert-propagation ((?m mem)(?x elt)) (((select ?m ?x))) () () (R ?m ?x (select ?m ?x) (select ?m ?x)) ) +;; (assert-propagation ((?x elt)) (f ?x)))) () () (Rf ?x (f ?x) (f ?x)) (((Rf ?x (f ?x) ) +;; (assert-propagation ((?x elt)) (((f ?x))) () () (=> true (Rf ?x (f ?x) (f ?x))) ) ;; reach -(assert-propagation ((?m mem)(?x1 elt)(?x2 elt)) () ((R ?m ?x1 ?x2 ?x2)) (or (= ?x1 ?x2) (R ?m ?x1 (select ?m ?x1) ?x2)) (((select ?m ?x1))) ) +(assert-propagation ((?m mem)(?x1 elt)(?x2 elt)) (((select ?m ?x1))) () ((R ?m ?x1 ?x2 ?x2)) (or (= ?x1 ?x2) (R ?m ?x1 (select ?m ?x1) ?x2)) ) ;; ;; reach extended -;; (assert-propagation ((?x1 elt)(?x2 elt)) ((not (= ?x1 ?x2))(Rf ?x1 ?x2 ?x2)) () (Rf ?x1 (f ?x1) ?x2) (((Rf ?x1 (f ?x1) ?x2))) ) +;; (assert-propagation ((?x1 elt)(?x2 elt)) (((Rf ?x1 (f ?x1) ?x2))) ((not (= ?x1 ?x2))(Rf ?x1 ?x2 ?x2)) () (Rf ?x1 (f ?x1) ?x2) ) ;; ;; reach extended -;; (assert-propagation ((?x1 elt)(?x2 elt)) ((not (Rf ?x1 (f ?x1) ?x2))(Rf ?x1 ?x2 ?x2)) () (= ?x1 ?x2) (((Rf ?x1 (f ?x1) ?x2))) ) +;; (assert-propagation ((?x1 elt)(?x2 elt)) (((Rf ?x1 (f ?x1) ?x2))) ((not (Rf ?x1 (f ?x1) ?x2))(Rf ?x1 ?x2 ?x2)) () (= ?x1 ?x2) ) ;; cycle -(assert-propagation ((?m mem)(?x1 elt)(?x2 elt)) ((= (select ?m ?x1) ?x1)) ((R ?m ?x1 ?x2 ?x2)) (= ?x1 ?x2) (((select ?m ?x1))) ) -;; (assert-propagation ((?x1 elt)(?x2 elt)) ((= (f ?x1) ?x1)) ((Rf ?x1 ?x2 ?x2)) (= ?x1 ?x2) () ) +(assert-propagation ((?m mem)(?x1 elt)(?x2 elt)) (((select ?m ?x1))) ((= (select ?m ?x1) ?x1)) ((R ?m ?x1 ?x2 ?x2)) (= ?x1 ?x2) ) +;; (assert-propagation ((?x1 elt)(?x2 elt)) () ((= (f ?x1) ?x1)) ((Rf ?x1 ?x2 ?x2)) (= ?x1 ?x2) ) -;; (assert-propagation ((?x1 elt)(?x2 elt)) () () (=> (and (= (f ?x1) ?x1) (Rf ?x1 ?x2 ?x2)) (= ?x1 ?x2)) (((Rf ?x1 ?x2 ?x2)(f ?x1))) ) +;; (assert-propagation ((?x1 elt)(?x2 elt)) (((Rf ?x1 ?x2 ?x2)(f ?x1))) () () (=> (and (= (f ?x1) ?x1) (Rf ?x1 ?x2 ?x2)) (= ?x1 ?x2)) ) ;; sandwich -(assert-propagation ((?m mem)(?x1 elt)(?x2 elt)) () ((R ?m ?x1 ?x2 ?x1)) (= ?x1 ?x2) () ) -;; (assert-propagation ((?x1 elt)(?x2 elt)) () () (=> (Rf ?x1 ?x2 ?x1) (= ?x1 ?x2)) (((Rf ?x1 ?x2 ?x1))) ) +(assert-propagation ((?m mem)(?x1 elt)(?x2 elt)) () () ((R ?m ?x1 ?x2 ?x1)) (= ?x1 ?x2) ) +;; (assert-propagation ((?x1 elt)(?x2 elt)) (((Rf ?x1 ?x2 ?x1))) () () (=> (Rf ?x1 ?x2 ?x1) (= ?x1 ?x2)) ) ;; order1 -(assert-propagation ((?m mem)(?x1 elt)(?x2 elt)(?x3 elt)) () - ((R ?m ?x1 ?x2 ?x2)(R ?m ?x1 ?x3 ?x3)) (or (R ?m ?x1 ?x2 ?x3) (R ?m ?x1 ?x3 ?x2)) () ) +(assert-propagation ((?m mem)(?x1 elt)(?x2 elt)(?x3 elt)) () () + ((R ?m ?x1 ?x2 ?x2)(R ?m ?x1 ?x3 ?x3)) (or (R ?m ?x1 ?x2 ?x3) (R ?m ?x1 ?x3 ?x2)) ) -;; (assert-propagation ((?x1 elt)(?x2 elt)(?x3 elt)) () () -;; (=> (and (Rf ?x1 ?x2 ?x2)(Rf ?x1 ?x3 ?x3)) (or (Rf ?x1 ?x2 ?x3) (Rf ?x1 ?x3 ?x2))) (((Rf ?x1 ?x2 ?x2)(Rf ?x1 ?x3 ?x3))) ) +;; (assert-propagation ((?x1 elt)(?x2 elt)(?x3 elt)) (((Rf ?x1 ?x2 ?x2)(Rf ?x1 ?x3 ?x3))) () () +;; (=> (and (Rf ?x1 ?x2 ?x2)(Rf ?x1 ?x3 ?x3)) (or (Rf ?x1 ?x2 ?x3) (Rf ?x1 ?x3 ?x2))) ) ;; ;; order1 extended -;; (assert-propagation ((?x1 elt)(?x2 elt)(?x3 elt)) ((Rf ?x1 ?x2 ?x2)(Rf ?x1 ?x3 ?x3)(not (Rf ?x1 ?x3 ?x2))) () -;; (Rf ?x1 ?x2 ?x3) (((Rf ?x1 ?x2 ?x3))) ) +;; (assert-propagation ((?x1 elt)(?x2 elt)(?x3 elt)) (((Rf ?x1 ?x2 ?x3))) ((Rf ?x1 ?x2 ?x2)(Rf ?x1 ?x3 ?x3)(not (Rf ?x1 ?x3 ?x2))) () +;; (Rf ?x1 ?x2 ?x3) ) ;; ;; order1 extended -;; (assert-propagation ((?x1 elt)(?x2 elt)(?x3 elt)) ((Rf ?x1 ?x2 ?x2)(Rf ?x1 ?x3 ?x3)(not (Rf ?x1 ?x2 ?x3))) () -;; (Rf ?x1 ?x3 ?x2) (((Rf ?x1 ?x3 ?x2))) ) +;; (assert-propagation ((?x1 elt)(?x2 elt)(?x3 elt)) (((Rf ?x1 ?x3 ?x2))) ((Rf ?x1 ?x2 ?x2)(Rf ?x1 ?x3 ?x3)(not (Rf ?x1 ?x2 ?x3))) () +;; (Rf ?x1 ?x3 ?x2) ) ;; ;; order1 extended -;; (assert-propagation ((?x1 elt)(?x2 elt)(?x3 elt)) ((Rf ?x1 ?x2 ?x2)(Rf ?x1 ?x3 ?x3)(not (Rf ?x1 ?x3 ?x2))) () -;; (Rf ?x1 ?x2 ?x3) (((Rf ?x1 ?x3 ?x2))) ) +;; (assert-propagation ((?x1 elt)(?x2 elt)(?x3 elt)) (((Rf ?x1 ?x3 ?x2))) ((Rf ?x1 ?x2 ?x2)(Rf ?x1 ?x3 ?x3)(not (Rf ?x1 ?x3 ?x2))) () +;; (Rf ?x1 ?x2 ?x3) ) ;; ;; order1 extended -;; (assert-propagation ((?x1 elt)(?x2 elt)(?x3 elt)) ((Rf ?x1 ?x2 ?x2)(Rf ?x1 ?x3 ?x3)(not (Rf ?x1 ?x2 ?x3))) () -;; (Rf ?x1 ?x3 ?x2) (((Rf ?x1 ?x2 ?x3))) ) +;; (assert-propagation ((?x1 elt)(?x2 elt)(?x3 elt)) (((Rf ?x1 ?x2 ?x3))) ((Rf ?x1 ?x2 ?x2)(Rf ?x1 ?x3 ?x3)(not (Rf ?x1 ?x2 ?x3))) () +;; (Rf ?x1 ?x3 ?x2) ) ;; ;; order1 extended -;; (assert-propagation ((?x1 elt)(?x2 elt)(?x3 elt)) ((Rf ?x1 ?x2 ?x2)(Rf ?x1 ?x3 ?x3)(not (Rf ?x1 ?x3 ?x2))) () -;; (Rf ?x1 ?x2 ?x3) (((Rf ?x1 ?x2 ?x2)(Rf ?x1 ?x3 ?x3))) ) +;; (assert-propagation ((?x1 elt)(?x2 elt)(?x3 elt)) (((Rf ?x1 ?x2 ?x2)(Rf ?x1 ?x3 ?x3))) ((Rf ?x1 ?x2 ?x2)(Rf ?x1 ?x3 ?x3)(not (Rf ?x1 ?x3 ?x2))) () +;; (Rf ?x1 ?x2 ?x3) ) ;; ;; order1 extended -;; (assert-propagation ((?x1 elt)(?x2 elt)(?x3 elt)) ((Rf ?x1 ?x2 ?x2)(Rf ?x1 ?x3 ?x3)(not (Rf ?x1 ?x2 ?x3))) () -;; (Rf ?x1 ?x3 ?x2) (((Rf ?x1 ?x2 ?x2)(Rf ?x1 ?x3 ?x3))) ) +;; (assert-propagation ((?x1 elt)(?x2 elt)(?x3 elt)) (((Rf ?x1 ?x2 ?x2)(Rf ?x1 ?x3 ?x3))) ((Rf ?x1 ?x2 ?x2)(Rf ?x1 ?x3 ?x3)(not (Rf ?x1 ?x2 ?x3))) () +;; (Rf ?x1 ?x3 ?x2) ) ;; order2 -(assert-propagation ((?m mem)(?x1 elt)(?x2 elt)(?x3 elt)) () ((R ?m ?x1 ?x2 ?x3)) - (and (R ?m ?x1 ?x2 ?x2) (R ?m ?x2 ?x3 ?x3)) () ) +(assert-propagation ((?m mem)(?x1 elt)(?x2 elt)(?x3 elt)) () () ((R ?m ?x1 ?x2 ?x3)) + (and (R ?m ?x1 ?x2 ?x2) (R ?m ?x2 ?x3 ?x3)) ) ;; transitive1 -(assert-propagation ((?m mem)(?x1 elt)(?x2 elt)(?x3 elt)) () ((R ?m ?x1 ?x2 ?x2)(R ?m ?x2 ?x3 ?x3)) - (R ?m ?x1 ?x3 ?x3) () ) +(assert-propagation ((?m mem)(?x1 elt)(?x2 elt)(?x3 elt)) () () ((R ?m ?x1 ?x2 ?x2)(R ?m ?x2 ?x3 ?x3)) + (R ?m ?x1 ?x3 ?x3) ) ;; ;; transitive1 extended -;; (assert-propagation ((?x1 elt)(?x2 elt)(?x3 elt)) () ((not (Rf ?x1 ?x3 ?x3))(Rf ?x2 ?x3 ?x3)) -;; (not (Rf ?x1 ?x2 ?x2)) () ) +;; (assert-propagation ((?x1 elt)(?x2 elt)(?x3 elt)) () () ((not (Rf ?x1 ?x3 ?x3))(Rf ?x2 ?x3 ?x3)) +;; (not (Rf ?x1 ?x2 ?x2)) ) ;; ;; transitive1 extended -;; (assert-propagation ((?x1 elt)(?x2 elt)(?x3 elt)) () ((Rf ?x1 ?x2 ?x2)(not (Rf ?x1 ?x3 ?x3))) -;; (not (Rf ?x2 ?x3 ?x3)) () ) +;; (assert-propagation ((?x1 elt)(?x2 elt)(?x3 elt)) () () ((Rf ?x1 ?x2 ?x2)(not (Rf ?x1 ?x3 ?x3))) +;; (not (Rf ?x2 ?x3 ?x3)) ) ;;transitive2 -(assert-propagation ((?m mem)(?x0 elt)(?x1 elt)(?x2 elt)(?x3 elt)) () ((R ?m ?x0 ?x1 ?x2)(R ?m ?x1 ?x3 ?x2)) - (and (R ?m ?x0 ?x1 ?x3) (R ?m ?x0 ?x3 ?x2)) () ) +(assert-propagation ((?m mem)(?x0 elt)(?x1 elt)(?x2 elt)(?x3 elt)) () () ((R ?m ?x0 ?x1 ?x2)(R ?m ?x1 ?x3 ?x2)) + (and (R ?m ?x0 ?x1 ?x3) (R ?m ?x0 ?x3 ?x2)) ) -;; (assert-propagation ((?x0 elt)(?x1 elt)(?x2 elt)(?x3 elt)) () () +;; (assert-propagation ((?x0 elt)(?x1 elt)(?x2 elt)(?x3 elt)) (((Rf ?x0 ?x1 ?x2)(Rf ?x1 ?x3 ?x2))) () () ;; (=> (and (Rf ?x0 ?x1 ?x2)(Rf ?x1 ?x3 ?x2)) ;; (and (Rf ?x0 ?x1 ?x3) (Rf ?x0 ?x3 ?x2))) -;; (((Rf ?x0 ?x1 ?x2)(Rf ?x1 ?x3 ?x2))) ) +;; ) ;; ;; transitive2 extended -;; (assert-propagation ((?x0 elt)(?x1 elt)(?x2 elt)(?x3 elt)) () ((not (Rf ?x0 ?x1 ?x3))(Rf ?x1 ?x3 ?x2)) -;; (not (Rf ?x0 ?x1 ?x2)) (((Rf ?x0 ?x1 ?x2))) ) +;; (assert-propagation ((?x0 elt)(?x1 elt)(?x2 elt)(?x3 elt)) (((Rf ?x0 ?x1 ?x2))) () ((not (Rf ?x0 ?x1 ?x3))(Rf ?x1 ?x3 ?x2)) +;; (not (Rf ?x0 ?x1 ?x2)) ) ;; ;; transitive2 extended -;; (assert-propagation ((?x0 elt)(?x1 elt)(?x2 elt)(?x3 elt)) () ((Rf ?x0 ?x1 ?x2)(not (Rf ?x0 ?x1 ?x3))) -;; (not (Rf ?x1 ?x3 ?x2)) (((Rf ?x1 ?x3 ?x2))) ) +;; (assert-propagation ((?x0 elt)(?x1 elt)(?x2 elt)(?x3 elt)) (((Rf ?x1 ?x3 ?x2))) () ((Rf ?x0 ?x1 ?x2)(not (Rf ?x0 ?x1 ?x3))) +;; (not (Rf ?x1 ?x3 ?x2)) ) ;; ;; transitive2 extended -;; (assert-propagation ((?x0 elt)(?x1 elt)(?x2 elt)(?x3 elt)) () ((not (Rf ?x0 ?x3 ?x2))(Rf ?x1 ?x3 ?x2)) -;; (not (Rf ?x0 ?x1 ?x2)) (((Rf ?x0 ?x1 ?x2))) ) +;; (assert-propagation ((?x0 elt)(?x1 elt)(?x2 elt)(?x3 elt)) (((Rf ?x0 ?x1 ?x2))) () ((not (Rf ?x0 ?x3 ?x2))(Rf ?x1 ?x3 ?x2)) +;; (not (Rf ?x0 ?x1 ?x2)) ) ;; ;; transitive2 extended -;; (assert-propagation ((?x0 elt)(?x1 elt)(?x2 elt)(?x3 elt)) () ((Rf ?x0 ?x1 ?x2)(not (Rf ?x0 ?x3 ?x2))) -;; (not (Rf ?x1 ?x3 ?x2)) (((Rf ?x1 ?x3 ?x2))) ) +;; (assert-propagation ((?x0 elt)(?x1 elt)(?x2 elt)(?x3 elt)) (((Rf ?x1 ?x3 ?x2))) () ((Rf ?x0 ?x1 ?x2)(not (Rf ?x0 ?x3 ?x2))) +;; (not (Rf ?x1 ?x3 ?x2)) ) ;; ;;transitive3 -(assert-propagation ((?m mem)(?x0 elt)(?x1 elt)(?x2 elt)(?x3 elt)) () ((R ?m ?x0 ?x1 ?x2)(R ?m ?x0 ?x3 ?x1)) - (and (R ?m ?x0 ?x3 ?x2) (R ?m ?x3 ?x1 ?x2)) () ) +(assert-propagation ((?m mem)(?x0 elt)(?x1 elt)(?x2 elt)(?x3 elt)) () () ((R ?m ?x0 ?x1 ?x2)(R ?m ?x0 ?x3 ?x1)) + (and (R ?m ?x0 ?x3 ?x2) (R ?m ?x3 ?x1 ?x2)) ) -;; (assert-propagation ((?x0 elt)(?x1 elt)(?x2 elt)(?x3 elt)) () () +;; (assert-propagation ((?x0 elt)(?x1 elt)(?x2 elt)(?x3 elt)) (((Rf ?x0 ?x1 ?x2)(Rf ?x0 ?x3 ?x1))) () () ;; (=> (and (Rf ?x0 ?x1 ?x2)(Rf ?x0 ?x3 ?x1)) -;; (and (Rf ?x0 ?x3 ?x2) (Rf ?x3 ?x1 ?x2))) (((Rf ?x0 ?x1 ?x2)(Rf ?x0 ?x3 ?x1))) ) +;; (and (Rf ?x0 ?x3 ?x2) (Rf ?x3 ?x1 ?x2))) ) (declare-fun next () mem) @@ -112,17 +112,16 @@ (declare-fun R_avoid (mem elt elt elt) Bool) -(assert-rewrite ((?m mem)(?x0 elt)(?x1 elt)(?exc elt)) () (R_avoid ?m ?x0 ?x1 ?exc) - (or (R ?m ?x0 ?x1 ?exc) (and (R ?m ?x0 ?x1 ?x1) (not (R ?m ?x0 ?exc ?exc)))) () ) +(assert-rewrite ((?m mem)(?x0 elt)(?x1 elt)(?exc elt)) () () (R_avoid ?m ?x0 ?x1 ?exc) + (or (R ?m ?x0 ?x1 ?exc) (and (R ?m ?x0 ?x1 ?x1) (not (R ?m ?x0 ?exc ?exc)))) ) ;; Identity of Back to the future p175 -(assert-rewrite ((?p elt)(?q elt)(?u elt)(?v elt)(?w elt)(?m mem)) () (R (store ?m ?p ?q) ?u ?v ?w) +(assert-rewrite ((?p elt)(?q elt)(?u elt)(?v elt)(?w elt)(?m mem)) () () (R (store ?m ?p ?q) ?u ?v ?w) (or (and (R ?m ?u ?v ?w) (R_avoid ?m ?u ?w ?p) ) (and (not (= ?p ?w)) (R_avoid ?m ?u ?p ?w) (R ?m ?u ?v ?p) (R_avoid ?m ?q ?w ?p) ) (and (not (= ?p ?w)) (R_avoid ?m ?u ?p ?w) (R ?m ?q ?v ?w) (R_avoid ?m ?q ?w ?p) ) ) - () -) + ) @@ -131,14 +130,14 @@ (declare-fun null () elt) (assert (= (select next null) null)) -(assert-propagation ((?m mem)(?x elt)(?y elt)(?z elt)) () ((R ?m ?x ?z ?z)(R ?m ?y ?z ?z)) (R ?m ?x (join ?m ?x ?y) ?z) (((join ?m ?x ?y))) ) -(assert-propagation ((?m mem)(?x elt)(?y elt)) () () (or (and (R ?m ?x (join ?m ?x ?y) (join ?m ?x ?y)) (R ?m ?y (join ?m ?x ?y) (join ?m ?x ?y))) (= (join ?m ?x ?y) null)) (((join ?m ?x ?y))) ) +(assert-propagation ((?m mem)(?x elt)(?y elt)(?z elt)) (((join ?m ?x ?y))) () ((R ?m ?x ?z ?z)(R ?m ?y ?z ?z)) (R ?m ?x (join ?m ?x ?y) ?z) ) +(assert-propagation ((?m mem)(?x elt)(?y elt)) (((join ?m ?x ?y))) () () (or (and (R ?m ?x (join ?m ?x ?y) (join ?m ?x ?y)) (R ?m ?y (join ?m ?x ?y) (join ?m ?x ?y))) (= (join ?m ?x ?y) null)) ) ;;extended join -(assert-propagation ((?m mem)(?x elt)(?y elt)(?z elt)) () ((R ?m ?x ?z (join ?m ?x ?y))(R ?m ?y ?z (join ?m ?x ?y))) (= ?z (join ?m ?x ?y)) () ) +(assert-propagation ((?m mem)(?x elt)(?y elt)(?z elt)) () () ((R ?m ?x ?z (join ?m ?x ?y))(R ?m ?y ?z (join ?m ?x ?y))) (= ?z (join ?m ?x ?y)) ) -(assert-propagation ((?p elt)(?q elt)(?m mem)(?u elt)(?v elt)) () () +(assert-propagation ((?p elt)(?q elt)(?m mem)(?u elt)(?v elt)) (((join (store ?m ?p ?q) ?u ?v))) () () (= (join (store ?m ?p ?q) ?u ?v) (let ((jp (join ?m ?u ?v))) ;; In ?m: ?u ?v have a nearest point of junction (join ?m ?u ?v) @@ -173,8 +172,7 @@ ) ) )) - (((join (store ?m ?p ?q) ?u ?v))) - ) + ) (declare-fun next2 () mem) diff --git a/test/regress/regress0/rewriterules/relation.smt2 b/test/regress/regress0/rewriterules/relation.smt2 index a327a90a4..e8c0139e8 100644 --- a/test/regress/regress0/rewriterules/relation.smt2 +++ b/test/regress/regress0/rewriterules/relation.smt2 @@ -7,13 +7,13 @@ (declare-fun R (elt elt) Bool) ;; reflexive -(assert-rewrite ((x elt)) () (R x x) true ()) +(assert-rewrite ((x elt)) () () (R x x) true) ;; transitive -(assert-propagation ((x elt) (y elt) (z elt)) () ((R x y) (R y z)) (R x z) ()) +(assert-propagation ((x elt) (y elt) (z elt)) () () ((R x y) (R y z)) (R x z)) ;; anti-symmetric -(assert-propagation ((x elt) (y elt)) () ((R x y) (R y x)) (= x y) ()) +(assert-propagation ((x elt) (y elt)) () () ((R x y) (R y x)) (= x y)) (declare-fun e1 () elt) (declare-fun e2 () elt) diff --git a/test/regress/regress0/rewriterules/set_A_new_fast_tableau-base.smt2 b/test/regress/regress0/rewriterules/set_A_new_fast_tableau-base.smt2 index 1b397ef5b..9bd49f714 100644 --- a/test/regress/regress0/rewriterules/set_A_new_fast_tableau-base.smt2 +++ b/test/regress/regress0/rewriterules/set_A_new_fast_tableau-base.smt2 @@ -12,98 +12,98 @@ ;; inter (declare-fun inter (set set) set) -(assert-propagation ((?s elt) (?t1 set) (?t2 set)) () - ((in ?s (inter ?t1 ?t2))) (and (in ?s ?t1) (in ?s ?t2)) ()) +(assert-propagation ((?s elt) (?t1 set) (?t2 set)) () () + ((in ?s (inter ?t1 ?t2))) (and (in ?s ?t1) (in ?s ?t2))) (assert-propagation ((?s elt) (?t1 set) (?t2 set)) - () ((not (in ?s ?t1))) (not (in ?s (inter ?t1 ?t2))) (((inter ?t1 ?t2))) ) + (((inter ?t1 ?t2))) () ((not (in ?s ?t1))) (not (in ?s (inter ?t1 ?t2))) ) (assert-propagation ((?s elt) (?t1 set) (?t2 set)) - () ((not (in ?s ?t2))) (not (in ?s (inter ?t1 ?t2))) (((inter ?t1 ?t2))) ) + (((inter ?t1 ?t2))) () ((not (in ?s ?t2))) (not (in ?s (inter ?t1 ?t2))) ) (assert-propagation ((?s elt) (?t1 set) (?t2 set)) - () ((not (in ?s (inter ?t1 ?t2))) (in ?s ?t1)) (not (in ?s ?t2)) () ) + () () ((not (in ?s (inter ?t1 ?t2))) (in ?s ?t1)) (not (in ?s ?t2)) ) (assert-propagation ((?s elt) (?t1 set) (?t2 set)) - () ((not (in ?s (inter ?t1 ?t2))) (in ?s ?t2)) (not (in ?s ?t1)) ()) + () () ((not (in ?s (inter ?t1 ?t2))) (in ?s ?t2)) (not (in ?s ?t1))) (assert-propagation ((?s elt) (?t1 set) (?t2 set)) - () ((in ?s ?t1) (in ?s ?t2)) (in ?s (inter ?t1 ?t2)) (((inter ?t1 ?t2))) ) + (((inter ?t1 ?t2))) () ((in ?s ?t1) (in ?s ?t2)) (in ?s (inter ?t1 ?t2)) ) ;;;;;;;;;;;;;;;;; ;; union (declare-fun union (set set) set) (assert-propagation ((?s elt) (?t1 set) (?t2 set)) - () ((not (in ?s (union ?t1 ?t2)))) (and (not (in ?s ?t1)) (not (in ?s ?t2))) ()) + () () ((not (in ?s (union ?t1 ?t2)))) (and (not (in ?s ?t1)) (not (in ?s ?t2)))) (assert-propagation ((?s elt) (?t1 set) (?t2 set)) - () ((in ?s ?t1)) (in ?s (union ?t1 ?t2)) (((union ?t1 ?t2)))) + (((union ?t1 ?t2))) () ((in ?s ?t1)) (in ?s (union ?t1 ?t2))) (assert-propagation ((?s elt) (?t1 set) (?t2 set)) - () ((in ?s ?t2)) (in ?s (union ?t1 ?t2)) (((union ?t1 ?t2)))) + (((union ?t1 ?t2))) () ((in ?s ?t2)) (in ?s (union ?t1 ?t2))) (assert-propagation ((?s elt) (?t1 set) (?t2 set)) - () ((in ?s (union ?t1 ?t2)) (not (in ?s ?t1))) (in ?s ?t2) ()) + () () ((in ?s (union ?t1 ?t2)) (not (in ?s ?t1))) (in ?s ?t2)) (assert-propagation ((?s elt) (?t1 set) (?t2 set)) - () ((in ?s (union ?t1 ?t2)) (not (in ?s ?t2))) (in ?s ?t1) ()) + () () ((in ?s (union ?t1 ?t2)) (not (in ?s ?t2))) (in ?s ?t1)) (assert-propagation ((?s elt) (?t1 set) (?t2 set)) - () ((not (in ?s ?t1)) (not (in ?s ?t2))) (not (in ?s (union ?t1 ?t2))) (((union ?t1 ?t2)))) + (((union ?t1 ?t2))) () ((not (in ?s ?t1)) (not (in ?s ?t2))) (not (in ?s (union ?t1 ?t2)))) ;;;;;;;;;;;;;;;;;;;; ;; diff (declare-fun diff (set set) set) (assert-propagation ((?s elt) (?t1 set) (?t2 set)) - () ((in ?s (diff ?t1 ?t2))) (and (in ?s ?t1) (not (in ?s ?t2))) ()) + () () ((in ?s (diff ?t1 ?t2))) (and (in ?s ?t1) (not (in ?s ?t2)))) (assert-propagation ((?s elt) (?t1 set) (?t2 set)) - () ((not (in ?s ?t1))) (not (in ?s (diff ?t1 ?t2))) (((diff ?t1 ?t2))) ) + (((diff ?t1 ?t2))) () ((not (in ?s ?t1))) (not (in ?s (diff ?t1 ?t2))) ) (assert-propagation ((?s elt) (?t1 set) (?t2 set)) - () ((in ?s ?t2)) (not (in ?s (diff ?t1 ?t2))) (((diff ?t1 ?t2)))) + (((diff ?t1 ?t2))) () ((in ?s ?t2)) (not (in ?s (diff ?t1 ?t2)))) (assert-propagation ((?s elt) (?t1 set) (?t2 set)) - () ((not (in ?s (diff ?t1 ?t2))) (in ?s ?t1)) (in ?s ?t2) ()) + () () ((not (in ?s (diff ?t1 ?t2))) (in ?s ?t1)) (in ?s ?t2)) (assert-propagation ((?s elt) (?t1 set) (?t2 set)) - () ((not (in ?s (diff ?t1 ?t2))) (not (in ?s ?t2))) (not (in ?s ?t1)) ()) + () () ((not (in ?s (diff ?t1 ?t2))) (not (in ?s ?t2))) (not (in ?s ?t1))) (assert-propagation ((?s elt) (?t1 set) (?t2 set)) - () ((in ?s ?t1) (not (in ?s ?t2))) (in ?s (diff ?t1 ?t2)) (((diff ?t1 ?t2))) ) + (((diff ?t1 ?t2))) () ((in ?s ?t1) (not (in ?s ?t2))) (in ?s (diff ?t1 ?t2)) ) ;;;;;;;;;;;;;;;; ;;sing (declare-fun sing (elt) set) (assert-propagation ((?s elt)) - () () (in ?s (sing ?s)) (((sing ?s))) ) + (((sing ?s))) () () (in ?s (sing ?s)) ) (assert-propagation ((?s elt) (?t1 elt)) - () ((in ?s (sing ?t1))) (= ?s ?t1) ()) + () () ((in ?s (sing ?t1))) (= ?s ?t1)) (assert-propagation ((?s elt) (?t1 elt)) - () ((not (in ?s (sing ?t1)))) (not (= ?s ?t1)) ()) + () () ((not (in ?s (sing ?t1)))) (not (= ?s ?t1))) ;;;;;;;;;;;;;;;;;;; ;; fullfiling runned at Full effort (assert-propagation ((?s elt) (?t1 set) (?t2 set)) - () ((in ?s (union ?t1 ?t2))) (or (in ?s ?t1) (not (in ?s ?t1))) ()) + () () ((in ?s (union ?t1 ?t2))) (or (in ?s ?t1) (not (in ?s ?t1)))) (assert-propagation ((?s elt) (?t1 set) (?t2 set)) - () ((in ?s ?t1)) (or (in ?s ?t2) (not (in ?s ?t2))) (((inter ?t1 ?t2)))) + (((inter ?t1 ?t2))) () ((in ?s ?t1)) (or (in ?s ?t2) (not (in ?s ?t2)))) (assert-propagation ((?t1 set) (?t2 set)) - () ((not (= ?t1 ?t2))) (exists ((?e elt)) (or (and (in ?e ?t1) (not (in ?e ?t2))) (and (not (in ?e ?t1)) (in ?e ?t2)))) ()) + () () ((not (= ?t1 ?t2))) (exists ((?e elt)) (or (and (in ?e ?t1) (not (in ?e ?t2))) (and (not (in ?e ?t1)) (in ?e ?t2))))) ;;;;;;;;;;;;;;;;;;; ;; shortcut (declare-fun subset (set set) Bool) (assert-reduction ((?t1 set) (?t2 set)) - () ((subset ?t1 ?t2)) (= (union ?t1 ?t2) ?t2) ()) + () () ((subset ?t1 ?t2)) (= (union ?t1 ?t2) ?t2)) (declare-fun e () elt) (declare-fun t1 () set) diff --git a/test/regress/regress0/rewriterules/set_A_new_fast_tableau-base_sat.smt2 b/test/regress/regress0/rewriterules/set_A_new_fast_tableau-base_sat.smt2 index 55050ac1a..4d65ffac5 100644 --- a/test/regress/regress0/rewriterules/set_A_new_fast_tableau-base_sat.smt2 +++ b/test/regress/regress0/rewriterules/set_A_new_fast_tableau-base_sat.smt2 @@ -13,98 +13,98 @@ ;; inter (declare-fun inter (set set) set) -(assert-propagation ((?s elt) (?t1 set) (?t2 set)) () - ((in ?s (inter ?t1 ?t2))) (and (in ?s ?t1) (in ?s ?t2)) ()) +(assert-propagation ((?s elt) (?t1 set) (?t2 set)) () () + ((in ?s (inter ?t1 ?t2))) (and (in ?s ?t1) (in ?s ?t2))) (assert-propagation ((?s elt) (?t1 set) (?t2 set)) - () ((not (in ?s ?t1))) (not (in ?s (inter ?t1 ?t2))) (((inter ?t1 ?t2))) ) + (((inter ?t1 ?t2))) () ((not (in ?s ?t1))) (not (in ?s (inter ?t1 ?t2))) ) (assert-propagation ((?s elt) (?t1 set) (?t2 set)) - () ((not (in ?s ?t2))) (not (in ?s (inter ?t1 ?t2))) (((inter ?t1 ?t2))) ) + (((inter ?t1 ?t2))) () ((not (in ?s ?t2))) (not (in ?s (inter ?t1 ?t2))) ) (assert-propagation ((?s elt) (?t1 set) (?t2 set)) - () ((not (in ?s (inter ?t1 ?t2))) (in ?s ?t1)) (not (in ?s ?t2)) () ) + () () ((not (in ?s (inter ?t1 ?t2))) (in ?s ?t1)) (not (in ?s ?t2)) ) (assert-propagation ((?s elt) (?t1 set) (?t2 set)) - () ((not (in ?s (inter ?t1 ?t2))) (in ?s ?t2)) (not (in ?s ?t1)) ()) + () () ((not (in ?s (inter ?t1 ?t2))) (in ?s ?t2)) (not (in ?s ?t1))) (assert-propagation ((?s elt) (?t1 set) (?t2 set)) - () ((in ?s ?t1) (in ?s ?t2)) (in ?s (inter ?t1 ?t2)) (((inter ?t1 ?t2))) ) + (((inter ?t1 ?t2))) () ((in ?s ?t1) (in ?s ?t2)) (in ?s (inter ?t1 ?t2)) ) ;;;;;;;;;;;;;;;;; ;; union (declare-fun union (set set) set) (assert-propagation ((?s elt) (?t1 set) (?t2 set)) - () ((not (in ?s (union ?t1 ?t2)))) (and (not (in ?s ?t1)) (not (in ?s ?t2))) ()) + () () ((not (in ?s (union ?t1 ?t2)))) (and (not (in ?s ?t1)) (not (in ?s ?t2)))) (assert-propagation ((?s elt) (?t1 set) (?t2 set)) - () ((in ?s ?t1)) (in ?s (union ?t1 ?t2)) (((union ?t1 ?t2)))) + (((union ?t1 ?t2))) () ((in ?s ?t1)) (in ?s (union ?t1 ?t2))) (assert-propagation ((?s elt) (?t1 set) (?t2 set)) - () ((in ?s ?t2)) (in ?s (union ?t1 ?t2)) (((union ?t1 ?t2)))) + (((union ?t1 ?t2))) () ((in ?s ?t2)) (in ?s (union ?t1 ?t2))) (assert-propagation ((?s elt) (?t1 set) (?t2 set)) - () ((in ?s (union ?t1 ?t2)) (not (in ?s ?t1))) (in ?s ?t2) ()) + () () ((in ?s (union ?t1 ?t2)) (not (in ?s ?t1))) (in ?s ?t2)) (assert-propagation ((?s elt) (?t1 set) (?t2 set)) - () ((in ?s (union ?t1 ?t2)) (not (in ?s ?t2))) (in ?s ?t1) ()) + () () ((in ?s (union ?t1 ?t2)) (not (in ?s ?t2))) (in ?s ?t1)) (assert-propagation ((?s elt) (?t1 set) (?t2 set)) - () ((not (in ?s ?t1)) (not (in ?s ?t2))) (not (in ?s (union ?t1 ?t2))) (((union ?t1 ?t2)))) + (((union ?t1 ?t2))) () ((not (in ?s ?t1)) (not (in ?s ?t2))) (not (in ?s (union ?t1 ?t2)))) ;;;;;;;;;;;;;;;;;;;; ;; diff (declare-fun diff (set set) set) (assert-propagation ((?s elt) (?t1 set) (?t2 set)) - () ((in ?s (diff ?t1 ?t2))) (and (in ?s ?t1) (not (in ?s ?t2))) ()) + () () ((in ?s (diff ?t1 ?t2))) (and (in ?s ?t1) (not (in ?s ?t2)))) (assert-propagation ((?s elt) (?t1 set) (?t2 set)) - () ((not (in ?s ?t1))) (not (in ?s (diff ?t1 ?t2))) (((diff ?t1 ?t2))) ) + (((diff ?t1 ?t2))) () ((not (in ?s ?t1))) (not (in ?s (diff ?t1 ?t2))) ) (assert-propagation ((?s elt) (?t1 set) (?t2 set)) - () ((in ?s ?t2)) (not (in ?s (diff ?t1 ?t2))) (((diff ?t1 ?t2)))) + (((diff ?t1 ?t2))) () ((in ?s ?t2)) (not (in ?s (diff ?t1 ?t2)))) (assert-propagation ((?s elt) (?t1 set) (?t2 set)) - () ((not (in ?s (diff ?t1 ?t2))) (in ?s ?t1)) (in ?s ?t2) ()) + () () ((not (in ?s (diff ?t1 ?t2))) (in ?s ?t1)) (in ?s ?t2)) (assert-propagation ((?s elt) (?t1 set) (?t2 set)) - () ((not (in ?s (diff ?t1 ?t2))) (not (in ?s ?t2))) (not (in ?s ?t1)) ()) + () () ((not (in ?s (diff ?t1 ?t2))) (not (in ?s ?t2))) (not (in ?s ?t1))) (assert-propagation ((?s elt) (?t1 set) (?t2 set)) - () ((in ?s ?t1) (not (in ?s ?t2))) (in ?s (diff ?t1 ?t2)) (((diff ?t1 ?t2))) ) + (((diff ?t1 ?t2))) () ((in ?s ?t1) (not (in ?s ?t2))) (in ?s (diff ?t1 ?t2)) ) ;;;;;;;;;;;;;;;; ;;sing (declare-fun sing (elt) set) (assert-propagation ((?s elt)) - () () (in ?s (sing ?s)) (((sing ?s))) ) + (((sing ?s))) () () (in ?s (sing ?s)) ) (assert-propagation ((?s elt) (?t1 elt)) - () ((in ?s (sing ?t1))) (= ?s ?t1) ()) + () () ((in ?s (sing ?t1))) (= ?s ?t1)) (assert-propagation ((?s elt) (?t1 elt)) - () ((not (in ?s (sing ?t1)))) (not (= ?s ?t1)) ()) + () () ((not (in ?s (sing ?t1)))) (not (= ?s ?t1))) ;;;;;;;;;;;;;;;;;;; ;; fullfiling runned at Full effort (assert-propagation ((?s elt) (?t1 set) (?t2 set)) - () ((in ?s (union ?t1 ?t2))) (or (in ?s ?t1) (not (in ?s ?t1))) ()) + () () ((in ?s (union ?t1 ?t2))) (or (in ?s ?t1) (not (in ?s ?t1)))) (assert-propagation ((?s elt) (?t1 set) (?t2 set)) - () ((in ?s ?t1)) (or (in ?s ?t2) (not (in ?s ?t2))) (((inter ?t1 ?t2)))) + (((inter ?t1 ?t2))) () ((in ?s ?t1)) (or (in ?s ?t2) (not (in ?s ?t2)))) (assert-propagation ((?t1 set) (?t2 set)) - () ((not (= ?t1 ?t2))) (exists ((?e elt)) (or (and (in ?e ?t1) (not (in ?e ?t2))) (and (not (in ?e ?t1)) (in ?e ?t2)))) ()) + () () ((not (= ?t1 ?t2))) (exists ((?e elt)) (or (and (in ?e ?t1) (not (in ?e ?t2))) (and (not (in ?e ?t1)) (in ?e ?t2))))) ;;;;;;;;;;;;;;;;;;; ;; shortcut (declare-fun subset (set set) Bool) (assert-reduction ((?t1 set) (?t2 set)) - () ((subset ?t1 ?t2)) (= (union ?t1 ?t2) ?t2) ()) + () () ((subset ?t1 ?t2)) (= (union ?t1 ?t2) ?t2)) (declare-fun e () elt) (declare-fun t1 () set) diff --git a/test/regress/regress0/rewriterules/why3_vstte10_max_sum_harness2.smt b/test/regress/regress0/rewriterules/why3_vstte10_max_sum_harness2.smt2 similarity index 100% rename from test/regress/regress0/rewriterules/why3_vstte10_max_sum_harness2.smt rename to test/regress/regress0/rewriterules/why3_vstte10_max_sum_harness2.smt2 diff --git a/test/regress/regress0/rewriterules/why3_vstte10_max_sum_harness2_rr.smt b/test/regress/regress0/rewriterules/why3_vstte10_max_sum_harness2_rr.smt2 similarity index 100% rename from test/regress/regress0/rewriterules/why3_vstte10_max_sum_harness2_rr.smt rename to test/regress/regress0/rewriterules/why3_vstte10_max_sum_harness2_rr.smt2 diff --git a/test/regress/regress0/rewriterules/why3_vstte10_max_sum_harness3.smt b/test/regress/regress0/rewriterules/why3_vstte10_max_sum_harness3.smt2 similarity index 100% rename from test/regress/regress0/rewriterules/why3_vstte10_max_sum_harness3.smt rename to test/regress/regress0/rewriterules/why3_vstte10_max_sum_harness3.smt2 diff --git a/test/regress/regress0/rewriterules/why3_vstte10_max_sum_harness3_rr.smt b/test/regress/regress0/rewriterules/why3_vstte10_max_sum_harness3_rr.smt2 similarity index 100% rename from test/regress/regress0/rewriterules/why3_vstte10_max_sum_harness3_rr.smt rename to test/regress/regress0/rewriterules/why3_vstte10_max_sum_harness3_rr.smt2 -- 2.30.2