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

15 files changed, 212 insertions, 214 deletions

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
index 4d39e12bb..4d39e12bb 100644
--- a/test/regress/regress0/rewriterules/why3_vstte10_max_sum_harness2.smt
+++ b/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
index 686b9ff04..686b9ff04 100644
--- a/test/regress/regress0/rewriterules/why3_vstte10_max_sum_harness2_rr.smt
+++ b/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
index e468128ac..e468128ac 100644
--- a/test/regress/regress0/rewriterules/why3_vstte10_max_sum_harness3.smt
+++ b/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
index a6f4106e5..a6f4106e5 100644
--- a/test/regress/regress0/rewriterules/why3_vstte10_max_sum_harness3_rr.smt
+++ b/test/regress/regress0/rewriterules/why3_vstte10_max_sum_harness3_rr.smt2