Merge quantifiers2-trunk:

   - new syntax for rewrite rules
   - better rewrite rules theory
   - remove the rewriting with rewrite rules during ppRewrite temporarily
   - theory can define their own candidate generator
   - define a general candidate generator (inefficient ask to every theory)
   - split inst_match between the pattern matching used for quantifiers (inst_match.*) and
     the one used for rewrite rules (rr_inst_match.*):
      - the pattern matching is less exhaustive for quantifiers,
      - the one for rewrite rules can use efficient-e-matching.

16 files changed, 1320 insertions, 199 deletions

diff --git a/test/regress/regress0/rewriterules/Makefile.am b/test/regress/regress0/rewriterules/Makefile.am
index 94b558675..c0a3fb934 100644
--- a/test/regress/regress0/rewriterules/Makefile.am
+++ b/test/regress/regress0/rewriterules/Makefile.am
@@ -1,4 +1,8 @@
 BINARY = cvc4
+
+CVC4_REGRESSION_ARGS ?= --efficient-e-matching
+export CVC4_REGRESSION_ARGS
+
 if PROOF_REGRESSIONS
 TESTS_ENVIRONMENT = LFSC="$(LFSC) $(LFSCARGS)" @srcdir@/../../run_regression $(RUN_REGRESSION_ARGS) --proof @top_builddir@/src/main/$(BINARY)
 else
@@ -13,7 +17,8 @@ MAKEFLAGS = -k
 TESTS =	\
 	length_trick.smt2 length_trick2.smt2 length_gen_020.smt2 \
 	datatypes.smt2 datatypes_sat.smt2 set_A_new_fast_tableau-base.smt2 \
-	set_A_new_fast_tableau-base_sat.smt2
+	set_A_new_fast_tableau-base_sat.smt2 relation.smt2 simulate_rewritting.smt2 \
+	reachability_back_to_the_future.smt2 native_arrays.smt2 reachability_bbttf_eT_arrays.smt2
 
 EXTRA_DIST = $(TESTS)
 
diff --git a/test/regress/regress0/rewriterules/datatypes_clark.smt2 b/test/regress/regress0/rewriterules/datatypes_clark.smt2
index eacb5ff6a..f1e61a901 100644
--- a/test/regress/regress0/rewriterules/datatypes_clark.smt2
+++ b/test/regress/regress0/rewriterules/datatypes_clark.smt2
@@ -1,4 +1,4 @@
-(set-logic LRA)
+(set-logic AUFLIRA)
 
 ;; DATATYPE
 ;;   nat = succ(pred : nat) | zero,
@@ -17,16 +17,14 @@
 ;; injective
 
 (declare-fun inj1 (nat) nat)
-(assert (forall ((?x1 nat))
-                (! (! (=> true (=> true (= (inj1 (succ ?x1)) ?x1))) :pattern ((succ ?x1)) ) :rewrite-rule) ))
-
+(assert-propagation((?x1 nat))
+                 () () (= (inj1 (succ ?x1)) ?x1) (((succ ?x1))) )
 
 ;;;;;;;;;;;;;;;;;;;;
 ;; projection
 
 (declare-fun pred (nat) nat)
-(assert (forall ((?x1 nat))
-                (! (= (pred (succ ?x1)) ?x1) :rewrite-rule) ))
+(assert-rewrite ((?x1 nat)) () (pred (succ ?x1)) ?x1 () )
 
 (assert (= (pred zero) zero))
 
@@ -34,45 +32,34 @@
 ;; test
 (declare-fun is_succ (nat) Bool)
 (assert (= (is_succ zero) false))
-(assert (forall ((?x1 nat))
-                (! (! (=> true (=> true (= (is_succ (succ ?x1)) true))) :pattern ((succ ?x1)) ) :rewrite-rule) ))
+(assert-propagation ((?x1 nat)) () () (= (is_succ (succ ?x1)) true) (((succ ?x1))) )
 
-(assert (forall ((?x1 nat))
-                (! (! (=> true (=> (is_succ ?x1) (= ?x1 (succ (pred ?x1))))) :pattern ((pred ?x1)) ) :rewrite-rule) ))
+(assert-propagation ((?x1 nat)) () ((is_succ ?x1)) (= ?x1 (succ (pred ?x1))) (((pred ?x1))))
 
 (declare-fun is_zero (nat) Bool)
 (assert (= (is_zero zero) true))
-(assert (forall ((?x1 nat))
-                (! (=> true (=> (is_zero ?x1) (= ?x1 zero))) :rewrite-rule) ))
+(assert-propagation ((?x1 nat)) () ((is_zero ?x1)) (= ?x1 zero) ())
 
 ;;; directrr
-(assert (forall ((?x1 nat))
-                (! (= (is_succ (succ ?x1)) true) :rewrite-rule)))
-(assert (forall ((?x1 nat))
-                (! (= (is_zero (succ ?x1)) false) :rewrite-rule)))
+(assert-rewrite ((?x1 nat)) () (is_succ (succ ?x1)) true () )
+(assert-rewrite ((?x1 nat)) () (is_zero (succ ?x1)) false () )
 
 
 ;;;;;;;;;;;;;;;;;;;;
 ;; distinct
-(assert (forall ((?x1 nat))
-                (! (=> (is_zero ?x1) (not (is_succ ?x1)) ) :rewrite-rule) ))
-(assert (forall ((?x1 nat))
-                (! (=> (is_succ ?x1) (not (is_zero ?x1)) ) :rewrite-rule) ))
-(assert (forall ((?x1 nat))
-                (! (=> (not (is_zero ?x1)) (is_succ ?x1) ) :rewrite-rule) ))
-(assert (forall ((?x1 nat))
-                (! (=> (not (is_succ ?x1)) (is_zero ?x1) ) :rewrite-rule) ))
+(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 (forall ((?x1 nat))
-                (! (! (=> true (or (is_zero ?x1) (is_succ ?x1))) :pattern ((pred ?x1)) ) :rewrite-rule) ))
+(assert-propagation ((?x1 nat)) () () (or (is_zero ?x1) (is_succ ?x1)) (((pred ?x1))) )
 
 ;;;;;;;;;;;;;;;;;;;
 ;; non-cyclic
 (declare-fun size_nat (nat) Real)
-(assert (forall ((?x1 nat))
-                (! (! (=> true (> (size_nat (succ ?x1)) (size_nat ?x1))) :pattern ((succ ?x1)) ) :rewrite-rule) ))
+(assert-propagation ((?x1 nat)) () () (> (size_nat (succ ?x1)) (size_nat ?x1)) (((succ ?x1))) )
 
 
 
@@ -96,26 +83,22 @@
 ;; injective
 
 (declare-fun inj2 (list) tree)
-(assert (forall ((?x1 tree) (?x2 list))
-                (! (! (=> true (=> true (= (inj2 (cons ?x1 ?x2)) ?x1))) :pattern ((cons ?x1 ?x2)) ) :rewrite-rule) ))
+(assert-propagation ((?x1 tree) (?x2 list)) () () (= (inj2 (cons ?x1 ?x2)) ?x1) (((cons ?x1 ?x2))) )
 
 (declare-fun inj3 (list) list)
-(assert (forall ((?x1 tree) (?x2 list))
-                (! (! (=> true (=> true (= (inj3 (cons ?x1 ?x2)) ?x2))) :pattern ((cons ?x1 ?x2)) ) :rewrite-rule) ))
+(assert-propagation ((?x1 tree) (?x2 list)) () () (= (inj3 (cons ?x1 ?x2)) ?x2) (((cons ?x1 ?x2))) )
 
 
 ;;;;;;;;;;;;;;;;;;;;
 ;; projection
 
 (declare-fun car (list) tree)
-(assert (forall ((?x1 tree) (?x2 list))
-                (! (= (car (cons ?x1 ?x2)) ?x1) :rewrite-rule) ))
+(assert-rewrite ((?x1 tree) (?x2 list)) () (car (cons ?x1 ?x2)) ?x1 ())
 
 (assert (= (car null) (node null)))
 
 (declare-fun cdr (list) list)
-(assert (forall ((?x1 tree) (?x2 list))
-                (! (= (cdr (cons ?x1 ?x2)) ?x2) :rewrite-rule) ))
+(assert-rewrite ((?x1 tree) (?x2 list)) () (cdr (cons ?x1 ?x2)) ?x2 ())
 
 (assert (= (cdr null) null))
 
@@ -123,50 +106,36 @@
 ;; test
 (declare-fun is_cons (list) Bool)
 (assert (= (is_cons null) false))
-(assert (forall ((?x1 tree) (?x2 list))
-                (! (! (=> true (=> true (= (is_cons (cons ?x1 ?x2)) true))) :pattern ((cons ?x1 ?x2)) ) :rewrite-rule) ))
+(assert-propagation ((?x1 tree) (?x2 list)) () () (= (is_cons (cons ?x1 ?x2)) true) (((cons ?x1 ?x2))) )
 
-(assert (forall ((?x1 list))
-                (! (! (=> true (=> (is_cons ?x1) (= ?x1 (cons (car ?x1) (cdr ?x1))))) :pattern ((car ?x1)) ) :rewrite-rule) ))
-(assert (forall ((?x1 list))
-                (! (! (=> true (=> (is_cons ?x1) (= ?x1 (cons (car ?x1) (cdr ?x1))))) :pattern ((cdr ?x1)) ) :rewrite-rule) ))
+(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))) )
 
 (declare-fun is_null (list) Bool)
 (assert (= (is_null null) true))
 
-(assert (forall ((?x1 list))
-                (! (! (=> true (=> (is_null ?x1) (= (car ?x1) (node null)))) :pattern ((car ?x1)) ) :rewrite-rule) ))
-(assert (forall ((?x1 list))
-                (! (! (=> true (=> (is_null ?x1) (= (cdr ?x1) null))) :pattern ((cdr ?x1)) ) :rewrite-rule) ))
+(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 (forall ((?x1 list))
-                (! (=> true (=> (is_null ?x1) (= ?x1 null))) :rewrite-rule) ))
+(assert-propagation ((?x1 list)) () ((is_null ?x1)) (= ?x1 null) ())
 
 ;;; directrr
-(assert (forall ((?x1 tree) (?x2 list))
-                (! (= (is_cons (cons ?x1 ?x2)) true) :rewrite-rule) ))
-(assert (forall ((?x1 tree) (?x2 list))
-                (! (= (is_null (cons ?x1 ?x2)) false) :rewrite-rule) ))
+(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 (forall ((?x1 list))
-                (! (=> (is_null ?x1) (not (is_cons ?x1)) ) :rewrite-rule) ))
-(assert (forall ((?x1 list))
-                (! (=> (is_cons ?x1) (not (is_null ?x1)) ) :rewrite-rule) ))
-(assert (forall ((?x1 list))
-                (! (=> (not (is_null ?x1)) (is_cons ?x1) ) :rewrite-rule) ))
-(assert (forall ((?x1 list))
-                (! (=> (not (is_cons ?x1)) (is_null ?x1) ) :rewrite-rule) ))
+(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 (forall ((?x1 list))
-            (! (! (=> true (or (is_null ?x1) (is_cons ?x1))) :pattern ((car ?x1)) ) :rewrite-rule) ))
-(assert (forall ((?x1 list))
-            (! (! (=> true (or (is_null ?x1) (is_cons ?x1))) :pattern ((cdr ?x1)) ) :rewrite-rule) ))
+(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))) )
 
 ;;;;;;;;;;;;;;;
 ;; tree
@@ -175,90 +144,61 @@
 ;; injective
 
 (declare-fun inj4 (tree) list)
-(assert (forall ((?x1 list))
-                (! (! (=> true (=> true (= (inj4 (node ?x1)) ?x1))) :pattern ((node ?x1)) ) :rewrite-rule) ))
+(assert-propagation ((?x1 list)) () () (= (inj4 (node ?x1)) ?x1) (((node ?x1))) )
 
 (declare-fun inj5 (tree) nat)
-(assert (forall ((?x1 nat))
-                (! (! (=> true (=> true (= (inj5 (leaf ?x1)) ?x1))) :pattern ((leaf ?x1)) ) :rewrite-rule) ))
+(assert-propagation ((?x1 nat)) () () (= (inj5 (leaf ?x1)) ?x1) (((leaf ?x1))) )
 
 
 ;;;;;;;;;;;;;;;;;;;;
 ;; projection
 
 (declare-fun children (tree) list)
-(assert (forall ((?x1 list))
-                (! (= (children (node ?x1)) ?x1) :rewrite-rule) ))
-(assert (forall ((?x1 nat))
-                (! (= (children (leaf ?x1)) null) :rewrite-rule) ))
-
+(assert-rewrite ((?x1 list)) () (children (node ?x1)) ?x1 () )
+(assert-rewrite ((?x1 nat)) () (children (leaf ?x1)) null () )
 
 (declare-fun data (tree) nat)
-(assert (forall ((?x1 nat))
-                (! (= (data (leaf ?x1)) ?x1) :rewrite-rule) ))
-(assert (forall ((?x1 list))
-                (! (= (data (node ?x1)) zero) :rewrite-rule) ))
+(assert-rewrite ((?x1 nat)) () (data (leaf ?x1)) ?x1 () )
+(assert-rewrite ((?x1 list)) () (data (node ?x1)) zero () )
 
 ;;;;;;;;;;;;;;;;;;;
 ;; test
 (declare-fun is_node (tree) Bool)
-(assert (forall ((?x1 list))
-                (! (! (=> true (=> true (= (is_node (node ?x1)) true))) :pattern ((node ?x1)) ) :rewrite-rule) ))
-
-(assert (forall ((?x1 tree))
-                (! (! (=> true (=> (is_node ?x1) (= ?x1 (node (children ?x1))))) :pattern ((children ?x1)) ) :rewrite-rule) ))
+(assert-propagation ((?x1 list)) () () (= (is_node (node ?x1)) true) (((node ?x1))) )
 
-(assert (forall ((?x1 tree))
-                (! (! (=> true (=> (is_node ?x1) (= (data ?x1) zero))) :pattern ((data ?x1)) ) :rewrite-rule) ))
+(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))) )
 
 
 (declare-fun is_leaf (tree) Bool)
-(assert (forall ((?x1 nat))
-                (! (! (=> true (=> true (= (is_leaf (leaf ?x1)) true))) :pattern ((leaf ?x1)) ) :rewrite-rule) ))
-
-(assert (forall ((?x1 tree))
-                (! (! (=> true (=> (is_leaf ?x1) (= ?x1 (leaf (data ?x1))))) :pattern ((data ?x1)) ) :rewrite-rule) ))
-(assert (forall ((?x1 tree))
-                (! (! (=> true (=> (is_leaf ?x1) (= (children ?x1) null))) :pattern ((children ?x1)) ) :rewrite-rule) ))
+(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))) )
 
 ;;; directrr
-(assert (forall ((?x1 list))
-                (! (= (is_node (node ?x1)) true) :rewrite-rule) ))
-(assert (forall ((?x1 list))
-                (! (= (is_leaf (node ?x1)) false) :rewrite-rule) ))
-(assert (forall ((?x1 nat))
-                (! (= (is_leaf (leaf ?x1)) true) :rewrite-rule) ))
-(assert (forall ((?x1 nat))
-                (! (= (is_node (leaf ?x1)) false) :rewrite-rule) ))
+(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 (forall ((?x1 tree))
-                (! (=> (is_node ?x1) (not (is_leaf ?x1)) ) :rewrite-rule) ))
-(assert (forall ((?x1 tree))
-                (! (=> (is_leaf ?x1) (not (is_node ?x1)) ) :rewrite-rule) ))
-(assert (forall ((?x1 tree))
-                (! (=> (not (is_node ?x1)) (is_leaf ?x1) ) :rewrite-rule) ))
-(assert (forall ((?x1 tree))
-                (! (=> (not (is_leaf ?x1)) (is_node ?x1) ) :rewrite-rule) ))
+(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 (forall ((?x1 tree))
-                (! (! (=> true (or (is_node ?x1) (is_leaf ?x1))) :pattern ((children ?x1)) ) :rewrite-rule) ))
-
-(assert (forall ((?x1 tree))
-                (! (! (=> true (or (is_node ?x1) (is_leaf ?x1))) :pattern ((data ?x1)) ) :rewrite-rule) ))
+(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))) )
 
 
 ;;;;;;;;;;;;;;;;;;
 ;; non-cyclic
 (declare-fun size_list (list) Real)
 (declare-fun size_tree (tree) Real)
-(assert (forall ((?x1 tree) (?x2 list))
-                (! (! (=> true (and (> (size_list (cons ?x1 ?x2)) (size_tree ?x1)) (> (size_list (cons ?x1 ?x2)) (size_list ?x2)))) :pattern ((cons ?x1 ?x2)) ) :rewrite-rule) ))
-(assert (forall ((?x1 list))
-                (! (! (=> true (> (size_tree (node ?x1)) (size_list ?x1))) :pattern ((node ?x1)) ) :rewrite-rule) ))
-(assert (forall ((?x1 nat))
-                (! (! (=> true (> (size_tree (leaf ?x1)) (size_nat ?x1))) :pattern ((leaf ?x1)) ) :rewrite-rule) ))
+(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))) )
diff --git a/test/regress/regress0/rewriterules/datatypes_clark_quantification.smt2 b/test/regress/regress0/rewriterules/datatypes_clark_quantification.smt2
new file mode 100644
index 000000000..6e22816d7
--- /dev/null
+++ b/test/regress/regress0/rewriterules/datatypes_clark_quantification.smt2
@@ -0,0 +1,264 @@
+(set-logic AUFLIRA)
+
+;; DATATYPE
+;;   nat = succ(pred : nat) | zero,
+;;   list = cons(car : tree, cdr : list) | null,
+;;   tree = node(children : list) | leaf(data : nat)
+;; END;
+
+;;;;;;;;;;;
+;; nat   ;;
+;;;;;;;;;;;
+(declare-sort nat 0)
+(declare-fun zero () nat)
+(declare-fun succ (nat) nat)
+
+;;;;;;;;;;;;;;;;
+;; injective
+
+(declare-fun inj1 (nat) nat)
+(assert (forall ((?x1 nat))
+                (! (= (inj1 (succ ?x1)) ?x1) :pattern ((succ ?x1)) ) ))
+
+
+;;;;;;;;;;;;;;;;;;;;
+;; projection
+
+(declare-fun pred (nat) nat)
+(assert (forall ((?x1 nat))
+                (! (= (pred (succ ?x1)) ?x1) :pattern ((pred (succ ?x1))) ) ))
+
+(assert (= (pred zero) zero))
+
+;;;;;;;;;;;;;;;;;;;
+;; test
+(declare-fun is_succ (nat) Bool)
+(assert (= (is_succ zero) false))
+(assert (forall ((?x1 nat))
+                (! (= (is_succ (succ ?x1)) true) :pattern ((succ ?x1)) ) ))
+
+(assert (forall ((?x1 nat))
+                (! (=> (is_succ ?x1) (= ?x1 (succ (pred ?x1)))) :pattern ((is_succ ?x1) (pred ?x1)) ) ))
+
+(declare-fun is_zero (nat) Bool)
+(assert (= (is_zero zero) true))
+(assert (forall ((?x1 nat))
+                (! (=> (is_zero ?x1) (= ?x1 zero)) :pattern ((is_zero ?x1)) ) ))
+
+;;; directrr
+(assert (forall ((?x1 nat))
+                (! (= (is_succ (succ ?x1)) true) :pattern ((is_succ (succ ?x1))) ) ))
+(assert (forall ((?x1 nat))
+                (! (= (is_zero (succ ?x1)) false) :pattern ((is_zero (succ ?x1))) )))
+
+
+;;;;;;;;;;;;;;;;;;;;
+;; distinct
+(assert (forall ((?x1 nat))
+                (! (=> (is_zero ?x1) (not (is_succ ?x1)) ) :pattern ((is_zero ?x1)) ) ))
+(assert (forall ((?x1 nat))
+                (! (=> (is_succ ?x1) (not (is_zero ?x1)) ) :pattern ((is_succ ?x1)) ) ))
+(assert (forall ((?x1 nat))
+                (! (=> (not (is_zero ?x1)) (is_succ ?x1) ) :pattern ((is_zero ?x1)) ) ))
+(assert (forall ((?x1 nat))
+                (! (=> (not (is_succ ?x1)) (is_zero ?x1) ) :pattern ((is_succ ?x1)) ) ))
+
+;;;;;;;;;;;;;;;;;;;
+;; case-split
+(assert (forall ((?x1 nat))
+                (! (or (is_zero ?x1) (is_succ ?x1)) :pattern ((pred ?x1)) ) ))
+
+;;;;;;;;;;;;;;;;;;;
+;; non-cyclic
+(declare-fun size_nat (nat) Real)
+(assert (forall ((?x1 nat))
+                (! (> (size_nat (succ ?x1)) (size_nat ?x1)) :pattern ((succ ?x1)) ) ))
+
+
+
+;;;;;;;;;;;;;;;;;;;;;
+;; list and tree
+
+(declare-sort list 0)
+(declare-sort tree 0)
+
+;;;;;;;;;;;
+;; list  ;;
+;;;;;;;;;;;
+
+(declare-fun null () list)
+(declare-fun cons (tree list) list)
+
+(declare-fun node (list) tree)
+(declare-fun leaf (nat) tree)
+
+;;;;;;;;;;;;;;;;
+;; injective
+
+(declare-fun inj2 (list) tree)
+(assert (forall ((?x1 tree) (?x2 list))
+                (! (= (inj2 (cons ?x1 ?x2)) ?x1) :pattern ((cons ?x1 ?x2)) ) ))
+
+(declare-fun inj3 (list) list)
+(assert (forall ((?x1 tree) (?x2 list))
+                (! (= (inj3 (cons ?x1 ?x2)) ?x2) :pattern ((cons ?x1 ?x2)) ) ))
+
+
+;;;;;;;;;;;;;;;;;;;;
+;; projection
+
+(declare-fun car (list) tree)
+(assert (forall ((?x1 tree) (?x2 list))
+                (! (= (car (cons ?x1 ?x2)) ?x1) :pattern ((car (cons ?x1 ?x2))) ) ))
+
+(assert (= (car null) (node null)))
+
+(declare-fun cdr (list) list)
+(assert (forall ((?x1 tree) (?x2 list))
+                (! (= (cdr (cons ?x1 ?x2)) ?x2) :pattern ((cdr (cons ?x1 ?x2))) ) ))
+
+(assert (= (cdr null) null))
+
+;;;;;;;;;;;;;;;;;;;
+;; test
+(declare-fun is_cons (list) Bool)
+(assert (= (is_cons null) false))
+(assert (forall ((?x1 tree) (?x2 list))
+                (! (= (is_cons (cons ?x1 ?x2)) true) :pattern ((cons ?x1 ?x2)) ) ))
+
+(assert (forall ((?x1 list))
+                (! (=> (is_cons ?x1) (= ?x1 (cons (car ?x1) (cdr ?x1)))) :pattern ((is_cons ?x1)(car ?x1)) ) ))
+(assert (forall ((?x1 list))
+                (! (=> (is_cons ?x1) (= ?x1 (cons (car ?x1) (cdr ?x1)))) :pattern ((is_cons ?x1)(cdr ?x1)) ) ))
+
+(declare-fun is_null (list) Bool)
+(assert (= (is_null null) true))
+
+(assert (forall ((?x1 list))
+                (! (=> (is_null ?x1) (= (car ?x1) (node null))) :pattern ((is_null ?x1)(car ?x1)) )  ))
+(assert (forall ((?x1 list))
+                (! (=> (is_null ?x1) (= (cdr ?x1) null)) :pattern ((is_null ?x1)(cdr ?x1)) ) ))
+
+(assert (forall ((?x1 list))
+                (! (=> (is_null ?x1) (= ?x1 null)) :pattern ((is_null ?x1)) ) ))
+
+;;; directrr
+(assert (forall ((?x1 tree) (?x2 list))
+                (! (= (is_cons (cons ?x1 ?x2)) true) :pattern ((is_cons (cons ?x1 ?x2))) ) ))
+(assert (forall ((?x1 tree) (?x2 list))
+                (! (= (is_null (cons ?x1 ?x2)) false) :pattern ((is_null (cons ?x1 ?x2))) ) ))
+
+
+
+;;;;;;;;;;;;;;;;;;;;
+;; distinct
+(assert (forall ((?x1 list))
+                (! (=> (is_null ?x1) (not (is_cons ?x1)) ) :pattern ((is_null ?x1)) ) ))
+(assert (forall ((?x1 list))
+                (! (=> (is_cons ?x1) (not (is_null ?x1)) ) :pattern ((is_cons ?x1)) ) ))
+(assert (forall ((?x1 list))
+                (! (=> (not (is_null ?x1)) (is_cons ?x1) ) :pattern ((is_null ?x1)) ) ))
+(assert (forall ((?x1 list))
+                (! (=> (not (is_cons ?x1)) (is_null ?x1) ) :pattern ((is_cons ?x1)) ) ))
+
+;;;;;;;;;;;;;;;;;;;
+;; case-split
+(assert (forall ((?x1 list))
+            (!  (or (is_null ?x1) (is_cons ?x1)) :pattern ((car ?x1)) ) ))
+(assert (forall ((?x1 list))
+            (! (or (is_null ?x1) (is_cons ?x1)) :pattern ((cdr ?x1)) ) ))
+
+;;;;;;;;;;;;;;;
+;; tree
+
+;;;;;;;;;;;;;;;;
+;; injective
+
+(declare-fun inj4 (tree) list)
+(assert (forall ((?x1 list))
+                (! (= (inj4 (node ?x1)) ?x1) :pattern ((node ?x1)) ) ))
+
+(declare-fun inj5 (tree) nat)
+(assert (forall ((?x1 nat))
+                (!  (= (inj5 (leaf ?x1)) ?x1) :pattern ((leaf ?x1)) )  ))
+
+
+;;;;;;;;;;;;;;;;;;;;
+;; projection
+
+(declare-fun children (tree) list)
+(assert (forall ((?x1 list))
+                (! (= (children (node ?x1)) ?x1) :pattern ((children (node ?x1))) ) ))
+(assert (forall ((?x1 nat))
+                (! (= (children (leaf ?x1)) null) :pattern ((children (leaf ?x1))) ) ))
+
+
+(declare-fun data (tree) nat)
+(assert (forall ((?x1 nat))
+                (! (= (data (leaf ?x1)) ?x1) :pattern ((data (leaf ?x1))) ) ))
+(assert (forall ((?x1 list))
+                (! (= (data (node ?x1)) zero) :pattern ((data (node ?x1))) ) ))
+
+;;;;;;;;;;;;;;;;;;;
+;; test
+(declare-fun is_node (tree) Bool)
+(assert (forall ((?x1 list))
+                (! (= (is_node (node ?x1)) true) :pattern ((node ?x1)) )  ))
+
+(assert (forall ((?x1 tree))
+                (! (=> (is_node ?x1) (= ?x1 (node (children ?x1)))) :pattern ((is_node ?x1)(children ?x1)) ) ))
+
+(assert (forall ((?x1 tree))
+                (! (=> (is_node ?x1) (= (data ?x1) zero)) :pattern ((is_node ?x1)(data ?x1)) ) ))
+
+
+(declare-fun is_leaf (tree) Bool)
+(assert (forall ((?x1 nat))
+                (! (=> true (= (is_leaf (leaf ?x1)) true)) :pattern ((leaf ?x1)) ) ))
+
+(assert (forall ((?x1 tree))
+                (! (=> (is_leaf ?x1) (= ?x1 (leaf (data ?x1)))) :pattern ((is_leaf ?x1)(data ?x1)) ) ))
+(assert (forall ((?x1 tree))
+                (! (=> (is_leaf ?x1) (= (children ?x1) null)) :pattern ((is_leaf ?x1)(children ?x1)) ) ))
+
+;;; directrr
+(assert (forall ((?x1 list))
+                (! (= (is_node (node ?x1)) true) :pattern ((is_node (node ?x1))) ) ))
+(assert (forall ((?x1 list))
+                (! (= (is_leaf (node ?x1)) false) :pattern ((is_leaf (node ?x1))) ) ))
+(assert (forall ((?x1 nat))
+                (! (= (is_leaf (leaf ?x1)) true) :pattern (is_leaf (leaf ?x1)) ) ))
+(assert (forall ((?x1 nat))
+                (! (= (is_node (leaf ?x1)) false) :pattern ((is_node (leaf ?x1))) ) ))
+
+
+;;;;;;;;;;;;;;;;;;;;
+;; distinct
+(assert (forall ((?x1 tree))
+                (! (=> (is_node ?x1) (not (is_leaf ?x1)) ) :pattern ((is_node ?x1)) ) ))
+(assert (forall ((?x1 tree))
+                (! (=> (is_leaf ?x1) (not (is_node ?x1)) ) :pattern ((is_leaf ?x1)) ) ))
+(assert (forall ((?x1 tree))
+                (! (=> (not (is_node ?x1)) (is_leaf ?x1) ) :pattern ((is_node ?x1)) ) ))
+(assert (forall ((?x1 tree))
+                (! (=> (not (is_leaf ?x1)) (is_node ?x1) ) :pattern ((is_leaf ?x1)) ) ))
+
+;;;;;;;;;;;;;;;;;;;
+;; case-split
+(assert (forall ((?x1 tree))
+                (!  (or (is_node ?x1) (is_leaf ?x1)) :pattern ((children ?x1)) ) ))
+
+(assert (forall ((?x1 tree))
+                (! (or (is_node ?x1) (is_leaf ?x1)) :pattern ((data ?x1)) )  ))
+
+
+;;;;;;;;;;;;;;;;;;
+;; non-cyclic
+(declare-fun size_list (list) Real)
+(declare-fun size_tree (tree) Real)
+(assert (forall ((?x1 tree) (?x2 list))
+                (! (and (> (size_list (cons ?x1 ?x2)) (size_tree ?x1)) (> (size_list (cons ?x1 ?x2)) (size_list ?x2))) :pattern ((cons ?x1 ?x2)) ) ))
+(assert (forall ((?x1 list))
+                (! (> (size_tree (node ?x1)) (size_list ?x1)) :pattern ((node ?x1)) )  ))
+(assert (forall ((?x1 nat))
+                (! (> (size_tree (leaf ?x1)) (size_nat ?x1)) :pattern ((leaf ?x1)) ) ))
diff --git a/test/regress/regress0/rewriterules/length_gen_010.smt2 b/test/regress/regress0/rewriterules/length_gen_010.smt2
index 7c7663b17..41cc61c9e 100644
--- a/test/regress/regress0/rewriterules/length_gen_010.smt2
+++ b/test/regress/regress0/rewriterules/length_gen_010.smt2
@@ -16,14 +16,16 @@
 
 (assert (= (length nil) 0))
 
-(assert (forall ((?e Int) (?l list)) (! (= (length (cons ?e ?l)) (+ 1 (length ?l))) :rewrite-rule)))
+;; (assert (forall ((?e Int) (?l list)) (! (= (length (cons ?e ?l)) (+ 1 (length ?l))) :rewrite-rule)))
+
+(assert-rewrite ((?e Int) (?l list)) () (length (cons ?e ?l)) (+ 1 (length ?l)) ())
 
 (declare-fun gen_cons (Int list) list)
 
-(assert (forall ((?n Int) (?l list)) (! (=> (= ?n 0) (= (gen_cons ?n ?l) ?l)) :rewrite-rule)))
+(assert-rewrite ((?n Int) (?l list)) (= ?n 0) (gen_cons ?n ?l) (?l) ())
 
-(assert (forall ((?n Int) (?l list)) (! (=> (> ?n 0) (= (gen_cons ?n ?l)
-        (gen_cons (- ?n 1) (cons 1 ?l)))) :rewrite-rule)))
+(assert-rewrite ((?n Int) (?l list)) (> ?n 0) (gen_cons ?n ?l)
+              (gen_cons (- ?n 1) (cons 1 ?l)) ())
 
 (declare-fun n () Int)
 
diff --git a/test/regress/regress0/rewriterules/native_arrays.smt2 b/test/regress/regress0/rewriterules/native_arrays.smt2
new file mode 100644
index 000000000..1be13167d
--- /dev/null
+++ b/test/regress/regress0/rewriterules/native_arrays.smt2
@@ -0,0 +1,34 @@
+;; This example can't be done if we don't access the EqualityEngine of
+;; the theory of arrays
+
+(set-logic AUFLIA)
+(set-info :status unsat)
+
+(declare-sort Index 0)
+(declare-sort Element 0)
+
+;;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 () )
+
+(declare-fun a1 () (Array Index Element))
+(declare-fun a2 () (Array Index Element))
+(declare-fun a3 () (Array Index Element))
+(declare-fun i1 () Index)
+(declare-fun i2 () Index)
+(declare-fun e1 () Element)
+
+(assert (not (=>  (or (= a1 (store a2 i1 e1)) (= a1 (store a3 i1 e1))) (P (select a1 i2)) )))
+(check-sat)
+(exit)
+
+
+;; (declare-fun a1 () (Array Index Element))
+;; (declare-fun a2 () (Array Index Element))
+;; (declare-fun i1 () Index)
+;; (assert (= (store a1 i1 (select a2 i1)) (store a2 i1 (select a1 i1))))
+;; (assert (not (= a1 a2)))
+;; (check-sat)
+;; (exit)
diff --git a/test/regress/regress0/rewriterules/native_datatypes.smt2 b/test/regress/regress0/rewriterules/native_datatypes.smt2
new file mode 100644
index 000000000..f5d53e3d5
--- /dev/null
+++ b/test/regress/regress0/rewriterules/native_datatypes.smt2
@@ -0,0 +1,33 @@
+;; Same than length.smt2 but the nil case is not a rewrite rule
+;; So here the rewrite rules have no guards length
+
+(set-info :status unsat)
+
+(declare-datatypes (
+(nat  (succ (pred nat)) (zero ) )
+(list  (cons (car nat)(cdr list)) (nil ) )
+
+))
+
+
+;;define length
+(declare-fun length (list) nat)
+
+(assert (= (length nil) zero))
+
+(assert (forall ((?e nat) (?l list)) (! (= (length (cons ?e ?l)) (succ (length ?l))) :rewrite-rule)))
+
+(declare-fun gen_cons (nat list) list)
+
+(assert (forall ((?l list)) (! (= (gen_cons zero ?l) ?l) :rewrite-rule)))
+
+(assert (forall ((?n nat) (?l list)) (! (= (gen_cons (succ ?n) ?l)
+        (gen_cons ?n (cons zero ?l))) :rewrite-rule)))
+
+(declare-fun n () nat)
+
+(assert (not (= (length (gen_cons (succ (succ zero)) nil)) (succ (succ zero)))))
+
+(check-sat)
+
+(exit)
diff --git a/test/regress/regress0/rewriterules/native_datatypes2.smt2 b/test/regress/regress0/rewriterules/native_datatypes2.smt2
new file mode 100644
index 000000000..4a719fb85
--- /dev/null
+++ b/test/regress/regress0/rewriterules/native_datatypes2.smt2
@@ -0,0 +1,35 @@
+;; Same than length.smt2 but the nil case is not a rewrite rule
+;; So here the rewrite rules have no guards length
+
+(set-info :status unsat)
+
+(declare-datatypes (
+(nat  (succ (pred nat)) (zero ) )
+(list  (cons (car nat)(cdr list)) (nil ) )
+
+))
+
+
+;;define length
+(declare-fun length (list) nat)
+
+(assert (= (length nil) zero))
+
+(assert-rewrite ((?e nat) (?l list)) () (length (cons ?e ?l)) (succ (length ?l)) () )
+(assert-propagation ((?l list)) ((= (length ?l) zero)) () (= ?l nil) (((length ?l))) )
+;(assert-propagation ((?l list)) () () (= ?l nil) (((= (length ?l) 0))) )
+
+(declare-fun gen_cons (nat list) list)
+
+(assert-rewrite ((?l list)) () (gen_cons zero ?l) ?l () )
+
+(assert-rewrite ((?n nat) (?l list)) () (gen_cons (succ ?n) ?l) (gen_cons ?n (cons zero ?l)) () )
+
+(declare-fun l1 () list)
+(declare-fun l2 () list)
+
+(assert (not (=> (= (length l1) zero) (= l1 nil))))
+
+(check-sat)
+
+(exit)
diff --git a/test/regress/regress0/rewriterules/reachability_back_to_the_future.smt2 b/test/regress/regress0/rewriterules/reachability_back_to_the_future.smt2
new file mode 100644
index 000000000..7cd61738b
--- /dev/null
+++ b/test/regress/regress0/rewriterules/reachability_back_to_the_future.smt2
@@ -0,0 +1,54 @@
+;; Back to the Future ... Shuvendu K.Lhiri, Shaz Qadeer
+(set-logic AUFLIA)
+(set-info :status unsat)
+
+(declare-sort elt 0)
+
+(declare-fun f (elt) elt)
+(declare-fun Rf (elt elt elt) Bool)
+
+;;eq
+(assert-propagation ((?x elt)) () () (or (= ?x ?x) (not (= ?x ?x))) ((?x)) )
+;; reflexive
+(assert-propagation ((?x elt)) () () (Rf ?x ?x ?x) ((?x)) )
+;; step
+(assert-propagation ((?x elt)) () () (Rf ?x (f ?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))) )
+;; cycle
+(assert-propagation ((?x1 elt)(?x2 elt)) ((= (f ?x1) ?x1)) ((Rf ?x1 ?x2 ?x2)) (= ?x1 ?x2) (((f ?x1))) )
+;; sandwich
+(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)) () )
+;; order2
+(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) () )
+;; 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)) () )
+;;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)) () )
+
+(declare-fun e1 () elt)
+(declare-fun e2 () elt)
+(declare-fun e3 () elt)
+(declare-fun e4 () elt)
+
+
+;; (assert (=> (Rf e1 e2 e3) (Rf e1 (f e1) (f e1)) ))
+
+;; (assert (=> (Rf e1 e2 e3) (Rf e1 e3 e3) ))
+
+;; (assert (=> (Rf e1 e2 e3) (or (= e1 e3) (Rf e1 (f e1) e3)) ))
+
+(assert (not (=> (and (not (= e1 e2)) (Rf e1 e2 e3)) (Rf e1 (f e1) e3) )))
+
+
+(check-sat)
+(exit)
\ No newline at end of file
diff --git a/test/regress/regress0/rewriterules/reachability_back_to_the_future_extended.smt2 b/test/regress/regress0/rewriterules/reachability_back_to_the_future_extended.smt2
new file mode 100644
index 000000000..955c810aa
--- /dev/null
+++ b/test/regress/regress0/rewriterules/reachability_back_to_the_future_extended.smt2
@@ -0,0 +1,72 @@
+;; Back to the Future ... Shuvendu K.Lhiri, Shaz Qadeer
+(set-logic AUFLIA)
+(set-info :status unsat)
+
+(declare-sort elt 0)
+
+(declare-fun f (elt) elt)
+(declare-fun Rf (elt elt elt) Bool)
+
+;;eq
+(assert-propagation ((?x elt)) () () (or (= ?x ?x) (not (= ?x ?x))) ((?x)) )
+;; reflexive
+(assert-propagation ((?x elt)) () () (Rf ?x ?x ?x) ((?x)) )
+;; step
+(assert-propagation ((?x elt)) () () (Rf ?x (f ?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))) )
+;; 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))) )
+;; 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))) )
+
+;; cycle
+(assert-propagation ((?x1 elt)(?x2 elt)) ((= (f ?x1) ?x1)) ((Rf ?x1 ?x2 ?x2)) (= ?x1 ?x2) (((f ?x1))) )
+;; sandwich
+(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)) () )
+;; 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))) )
+;; 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))) )
+
+;; order2
+(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) () )
+;; 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)) () )
+;;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)) () )
+
+(declare-fun e1 () elt)
+(declare-fun e2 () elt)
+(declare-fun e3 () elt)
+(declare-fun e4 () elt)
+
+
+(assert (and (hack e1) (hack e2) (hack e3) (hack e4) (hack (f e1))))
+
+
+;; (assert (=> (Rf e1 e2 e3) (Rf e1 (f e1) (f e1)) ))
+
+;; (assert (=> (Rf e1 e2 e3) (Rf e1 e3 e3) ))
+
+;; (assert (=> (Rf e1 e2 e3) (or (= e1 e3) (Rf e1 (f e1) e3)) ))
+
+;;(assert (not (=> (and (not (= e1 e2)) (Rf e1 e2 e3)) (Rf e1 (f e1) e3) )))
+
+(assert (and (not (= e1 e2)) (Rf e1 e2 e3) (not (Rf e1 (f e1) e3)) ))
+
+
+(check-sat)
+(exit)
\ No newline at end of file
diff --git a/test/regress/regress0/rewriterules/reachability_bbttf_eT_arrays.smt2 b/test/regress/regress0/rewriterules/reachability_bbttf_eT_arrays.smt2
new file mode 100644
index 000000000..b7069536a
--- /dev/null
+++ b/test/regress/regress0/rewriterules/reachability_bbttf_eT_arrays.smt2
@@ -0,0 +1,332 @@
+;; Back to the Future ... Shuvendu K.Lhiri, Shaz Qadeer
+(set-logic AUFLIA)
+(set-info :status unsat)
+
+(declare-sort elt 0)
+(define-sort mem () (Array elt elt))
+
+(declare-fun R (mem elt elt elt) Bool)
+
+;; reflexive
+(assert-propagation ((?m mem)(?x elt)) () () (R ?m ?x ?x ?x) ((?m ?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))) )
+
+;; 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))) )
+;; ;; 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))) )
+;; ;; 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))) )
+
+;; 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 ((?x1 elt)(?x2 elt)) () () (=> (and (= (f ?x1) ?x1) (Rf ?x1 ?x2 ?x2)) (= ?x1 ?x2)) (((Rf ?x1 ?x2 ?x2)(f ?x1))) )
+
+;; 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))) )
+
+;; 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 ((?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))) )
+
+;; ;; 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))) )
+;; ;; 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))) )
+;; ;; 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))) )
+;; ;; 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))) )
+;; ;; 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))) )
+;; ;; 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))) )
+
+;; 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)) () )
+;; 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) () )
+;; ;; transitive1 extended
+;; (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)) () )
+
+;;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 ((?x0 elt)(?x1 elt)(?x2 elt)(?x3 elt)) () ()
+;;                     (=> (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))) )
+;; ;; 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))) )
+;; ;; 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))) )
+;; ;; 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))) )
+
+;; ;;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 ((?x0 elt)(?x1 elt)(?x2 elt)(?x3 elt)) () ()
+;;                     (=> (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))) )
+
+
+(declare-fun next () mem)
+
+(declare-fun e1 () elt)
+(declare-fun e2 () elt)
+(declare-fun e3 () elt)
+(declare-fun e4 () elt)
+
+
+
+(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)))) () )
+
+
+;; 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)
+                (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) ) )
+                ()
+)
+
+
+
+(declare-fun join (mem elt elt) elt)
+
+(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))) )
+
+;;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 ((?p elt)(?q elt)(?m mem)(?u elt)(?v elt)) () ()
+                    (= (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)
+                         (ite (and (R ?m ?u jp jp) (R ?m ?v jp jp))
+                              ;; The modification is in the ?u branch
+                              (ite (R ?m ?u ?p jp)
+                                   ;; we can go by the new path and the new path doesn't cycle
+                                   (ite (and (R (store ?m ?p ?q) ?u ?p ?q) (R (store ?m ?p ?q) ?q (join ?m ?q ?v) (join ?m ?q ?v)))
+                                        (join ?m ?q ?v)
+                                   ;; we can't
+                                        null
+                                   )
+                              ;; The modification is in the ?v branch
+                              (ite (R ?m ?v ?p jp)
+                                   ;; we can go by the new path and the new path doesn't cycle
+                                   (ite (and (R (store ?m ?p ?q) ?v ?p ?q) (R (store ?m ?p ?q) ?q (join ?m ?u ?q) (join ?m ?u ?q)))
+                                        (join ?m ?u ?q)
+                                   ;; we can't
+                                        null
+                                   )
+                              ;; The modification is not before the point of junction
+                                   (join ?m ?u ?v)
+                              ))
+                         ;; In ?m: ?u ?v doens't have a point of junction
+                              ;;The modification is accesible from ?u
+                              (ite (R ?m ?u ?p ?p) (join ?m ?q ?v)
+                              ;;The modification is accesible from ?v
+                                   (ite (R ?m ?v ?p ?p) (join ?m ?u ?q)
+                              ;;The modification is accesible neither from ?u neither from ?v
+                                        (join ?m ?u ?v)
+                                   )
+                              )
+                         )
+                       ))
+                    (((join (store ?m ?p ?q) ?u ?v)))
+                    )
+
+(declare-fun next2 () mem)
+
+;; === Example 0 ===
+;; (assert (not (=>
+;;               (and (not (= e1 e2))
+;;                    (R next e1 e2 e3))
+;;               (R next e1 (select next e1) e3))
+;; ))
+
+;;================
+;;Thomas' example1 x,e1 y,e2 z,e3 y',e4
+;;================
+;; (assert (not (=>
+;;               (and (R next e1 e2 e3)
+;;                    (not (= e2 e3))
+;;                    (= e4 (select next e2)))
+;;               (R next e1 e4 e3))
+;; ))
+
+
+;;===================
+;; ;;Thomas' example2
+;;===================
+
+;; (assert (not (=>
+;;               (and (R next e1 null null)
+;;                    (= (join next e1 e2) null)
+;;                    (= next2 (store next e2 e1))
+;;                    )
+;;               (R next2 e1 null null)
+;;               )
+;;              )
+;;         )
+
+
+;;================
+;;Thomas' example3
+;;================
+(assert (not (=> (and (= (join next e1 e2) null)
+                      (R next e2 null null)
+                      (not (= e2 null))
+                      (= next2 (store next e2 e1))
+                      (= e3 e2)
+                      (= e4 (select next e2))
+                      )
+                 (= (join next2 e3 e4) null)
+                 )
+             )
+        )
+
+;; ==== for debugging example 3 ====
+;; ;;case to consider
+;; ;;(assert (or (not (R next e1 null null)) (R next e1 null null)))
+
+;; ;;first case to consider
+;; ;;(assert (R next e1 null null))
+
+;; ;;second case to consider
+;; ;; (assert (not (R next e1 null null)))
+
+
+;; ;;hyp
+;; (assert (= (join next e1 e2) null))
+;; (assert (R next e2 null null))
+;; (assert (not (= e2 null)))
+;; (assert (= next2 (store next e2 e1)))
+;; (assert (= e3 e2))
+;; (assert (= e4 (select next e2)))
+
+;; ;; help
+;; ;; have a join point
+;; ;; (assert (R next e2 e4 e4))
+;; ;; (assert (R next e4 e4 e4))
+
+;; ;; (assert (R next e2 (join next e2 e4) e4))
+;; ;; (assert (not (R next e4 e2 e2)))
+
+;; ;; (assert (not (= e2 (join next e2 e4))));;  slow with efficient (/axioms)
+
+;; ;; (assert (= e4 (join next e2 e4))) ;; unprovable with efficient (/axioms)
+;; ;; in e2 branch
+;; ;; (assert (not (R next e4 e2 null))) ;; 
+;; ;; the auxillary join
+;; ;; (assert (= (join next2 e1 e4) null))
+
+
+;; ;;to prove
+;; (assert (not (= (join next2 e3 e4) null)))
+
+
+;;====================
+;; ;;Thomas' example wrong sat?
+;;====================
+
+;; (assert (not (=> (and
+;;                   (= (join next e1 e2) null)
+;;                   (R next e2 null null)
+;;                   (not (= e2 null))
+;;                   (= next2 (store next e2 e1))
+;;                   )
+;;                  (= (join next2 e1 e2) null)
+;;                  )
+;;              )
+;;         )
+
+;;====================
+;; ;;example4 sat
+;;====================
+
+;; (assert (not (=> (and
+;;                   (= (join next e1 e2) null)
+;;                   (R next e2 null null) (not (= e2 null))
+;;                   )
+;; (not (R next e2 e2 e2))
+;; )))
+
+
+;;====================
+;;example5 unsat
+;;====================
+
+;; (assert (and
+;;          ;; (= (join e1 e2) null)
+;;          (= (select next (select next e1)) e1)
+;;          (R next e1 e2 e2)
+;;          (not (= e2 e1))
+;;          (not (= e2 (select next e1)))
+;;          )
+;; )
+
+;;====================
+;; ;; example 6 unsat
+;;====================
+
+;; ;; join is the nearest junction point
+;; (assert (and (not (= e3 (join next e1 e2)))
+;;              (R next e1 e3 (join next e1 e2))
+;;              (R next e2 e3 (join next e1 e2))
+;; ))
+
+
+;;====================
+;; example7 unsat
+;;====================
+
+;; (assert (R next e1 e2 (select next e1)))
+;; (assert (not (= e1 e2)))
+;; (assert (not (= e2 (select next e1))))
+
+
+
+(check-sat)
+(exit)
+
diff --git a/test/regress/regress0/rewriterules/reachability_bttf_ext_Thomas.smt2 b/test/regress/regress0/rewriterules/reachability_bttf_ext_Thomas.smt2
new file mode 100644
index 000000000..92103238c
--- /dev/null
+++ b/test/regress/regress0/rewriterules/reachability_bttf_ext_Thomas.smt2
@@ -0,0 +1,211 @@
+;; Back to the Future ... Shuvendu K.Lhiri, Shaz Qadeer
+(set-logic AUFLIA)
+(set-info :status unsat)
+
+(declare-sort elt 0)
+
+(declare-fun f (elt) elt)
+(declare-fun Rf (elt elt elt) Bool)
+
+;; reflexive
+;;(assert-propagation ((?x elt)) () () (Rf ?x ?x ?x) ((?x)) )
+;; step
+(assert-propagation ((?x elt)) () () (Rf ?x (f ?x) (f ?x)) (((f ?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))) )
+
+;; reach
+(assert-propagation ((?x1 elt)(?x2 elt)) () ((Rf ?x1 ?x2 ?x2)) (or (= ?x1 ?x2) (Rf ?x1 (f ?x1) ?x2)) (((f ?x1))) )
+;; ;; 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))) )
+;; ;; 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))) )
+
+;; 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) ?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))) )
+
+;; 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)) (((Rf ?x1 ?x2 ?x1))) )
+
+;; 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)) () ()
+;;                     (=> (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))) )
+
+;; ;; 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))) )
+;; ;; 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))) )
+;; ;; 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))) )
+;; ;; 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))) )
+;; ;; 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))) )
+;; ;; 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))) )
+
+;; order2
+(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) () )
+;; ;; transitive1 extended
+;; (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)) () )
+
+;;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)) () ()
+;;                     (=> (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))) )
+;; ;; 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))) )
+;; ;; 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))) )
+;; ;; 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))) )
+
+;; ;;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)) () ()
+;;                     (=> (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))) )
+
+
+(declare-fun e1 () elt)
+(declare-fun e2 () elt)
+(declare-fun e3 () elt)
+(declare-fun e4 () elt)
+
+
+;;Example0
+;;(assert (not (=> (and (not (= e1 e2)) (Rf e1 e2 e3)) (Rf e1 (f e1) e3))) )
+
+;;Thomas' example1 x,e1 y,e2 z,e3 y',e4
+;;(assert (not (=> (and (Rf e1 e2 e3) (not (= e2 e3)) (= e4 (f e2))) (Rf e1 e4 e3))))
+
+(declare-fun Rf_avoid (elt elt elt) Bool)
+
+;; (assert-rewrite ((?x0 elt)(?x1 elt)(?exc elt)) () (Rf_avoid ?x0 ?x1 ?exc)
+;;                  (or (Rf ?x0 ?x1 ?exc) (and (Rf ?x0 ?x1 ?x1) (not (Rf ?x0 ?exc ?exc)))) () )
+
+(declare-fun null () elt)
+(assert (= (f null) null))
+
+(declare-fun join (elt elt) elt)
+
+;; (assert-propagation ((?x elt)(?y elt)(?z elt)) () ((Rf ?x ?z ?z)(Rf ?y ?z ?z)) (Rf ?x (join ?x ?y) ?z) (((join ?x ?y))) )
+;; (assert-propagation ((?x elt)(?y elt)) () () (or (and (Rf ?x (join ?x ?y) (join ?x ?y)) (Rf ?y (join ?x ?y) (join ?x ?y))) (= (join ?x ?y) null))  (((join ?x ?y))) )
+
+;;Thomas' example2
+;; (assert (not (=> (and (Rf e1 null null) (= (join e1 e2) null)
+;; ;; (next' == upd(next, e, e1)
+;; )
+;; ;; (reach(next', e1, null) )
+;; (or (and (Rf e1 null null) (Rf_avoid e1 null e2) )
+;;     (and (not (= e2 null)) (Rf_avoid e1 e2 null) (Rf e1 null e2) (Rf_avoid e1 null e2) )
+;;     (and (not (= e2 null)) (Rf_avoid e1 e2 null) (Rf e1 null null) (Rf_avoid e1 null e2) ) )
+;; )))
+
+
+;;Thomas' example3
+;; join(next, first, e) == null &&
+;; reach(next, e, null) &&
+;; e != null &&
+;; next' == upd(next, e, first) &&
+;; first' == e &&
+;; e' == sel (next, e)
+;; ==>
+;; join(next', first', e') == null 
+
+
+;;Thomas' example3
+(assert(not
+        (=>
+         (and
+          ;; (= (join e1 e2) null)
+          (Rf e2 null null)
+          (not (= e2 null)))
+         ;; (next' == upd(next, e2, e1)
+         ;;join(next',e1,e2) == null
+(or (and (not (Rf (f e2) e2 e2)) (not (Rf e1 e2 e2) ))
+;;    (and (Rf (f e2) e2 e2) (not (Rf e1 e1 e1) ))
+    (and (Rf e1 e2 e2) (not (Rf (f e2) e1 e1)) )
+)
+;; (or
+;;  (and (not (Rf e1 e2 e2)) (not (Rf e2 e2 e2)))
+;;  (and (Rf e1 e2 e2) (not (Rf e2 e1 e1)))
+;;  (and (Rf e2 e2 e2) (not (Rf e1 e1 e1)))
+;; )
+)))
+
+
+
+;; ;;Thomas' example wrong sat?
+;; (assert (not (=> (and
+;;                   (= (join e1 e2) null)
+;;                   (Rf e2 null null) (not (= e2 null)))
+;; ;; (next' == upd(next, e2, e1)
+;; ;;join(next',e1,e2) == null
+;; (not (Rf e2 e2 e2))
+;; ;; (or
+;; ;;  (and (not (Rf e1 e2 e2)) (not (Rf e2 e2 e2)))
+;; ;;  (and (Rf e1 e2 e2) (not (Rf e2 e1 e1)))
+;; ;;  (and (Rf e2 e2 e2) (not (Rf e1 e1 e1)))
+;; ;; )
+;; )))
+
+;; ;;example4
+;; (assert (not (=> (and
+;;                   (= (join e1 e2) null)
+;;                   (Rf e2 null null) (not (= e2 null))
+;;                   )
+;; (not (Rf e2 e2 e2))
+;; )))
+
+
+;; ;;example5
+;; (assert (and
+;;          ;; (= (join e1 e2) null)
+;;          (= (f (f e1)) e1)
+;;          (Rf e1 e2 e2)
+;;          (not (= e2 e1))
+;;          (not (= e2 (f e1)))
+;;          )
+;; )
+
+
+
+
+(check-sat)
+(exit)
+
diff --git a/test/regress/regress0/rewriterules/relation.smt2 b/test/regress/regress0/rewriterules/relation.smt2
new file mode 100644
index 000000000..a327a90a4
--- /dev/null
+++ b/test/regress/regress0/rewriterules/relation.smt2
@@ -0,0 +1,27 @@
+(set-logic AUFLIA)
+(set-info :status unsat)
+
+;; don't use a datatypes for currently focusing in uf
+(declare-sort elt 0)
+
+(declare-fun R (elt elt) Bool)
+
+;; reflexive
+(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) ())
+
+;; anti-symmetric
+(assert-propagation ((x elt) (y elt)) () ((R x y) (R y x)) (= x y) ())
+
+(declare-fun e1 () elt)
+(declare-fun e2 () elt)
+(declare-fun e3 () elt)
+(declare-fun e4 () elt)
+
+(assert (not (=> (and (R e1 e2) (R e2 e3) (R e3 e4) (R e4 e1)) (= e1 e4))))
+
+(check-sat)
+
+(exit)
\ No newline at end of file
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 65dc23a10..1b397ef5b 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,72 +12,98 @@
 ;; inter
 
 (declare-fun inter (set set)  set)
-(assert (forall ((?s elt) (?t1 set) (?t2 set))
-                (! (=> (in ?s (inter ?t1 ?t2)) (and (in ?s ?t1) (in ?s ?t2))) :rewrite-rule)))
+(assert-propagation ((?s elt) (?t1 set) (?t2 set)) ()
+                  ((in ?s (inter ?t1 ?t2))) (and (in ?s ?t1) (in ?s ?t2)) ())
 
 
-(assert (forall ((?s elt) (?t1 set) (?t2 set))
-                (! (! (=> (not (in ?s ?t1)) (not (in ?s (inter ?t1 ?t2)))) :pattern ((inter ?t1 ?t2)) ) :rewrite-rule) ))
+(assert-propagation ((?s elt) (?t1 set) (?t2 set))
+                  () ((not (in ?s ?t1))) (not (in ?s (inter ?t1 ?t2))) (((inter ?t1 ?t2))) )
 
-(assert (forall ((?s elt) (?t1 set) (?t2 set))
-                (! (! (=> (not (in ?s ?t2)) (not (in ?s (inter ?t1 ?t2)))) :pattern ((inter ?t1 ?t2)) ) :rewrite-rule) ))
+(assert-propagation ((?s elt) (?t1 set) (?t2 set))
+                  () ((not (in ?s ?t2))) (not (in ?s (inter ?t1 ?t2))) (((inter ?t1 ?t2))) )
 
-(assert (forall ((?s elt) (?t1 set) (?t2 set))
-                (! (=> (and (not (in ?s (inter ?t1 ?t2)))  (in ?s ?t1)) (not (in ?s ?t2))) :rewrite-rule) ))
+(assert-propagation ((?s elt) (?t1 set) (?t2 set))
+                  () ((not (in ?s (inter ?t1 ?t2))) (in ?s ?t1)) (not (in ?s ?t2)) () )
 
-(assert (forall ((?s elt) (?t1 set) (?t2 set))
-                (! (=> (and (not (in ?s (inter ?t1 ?t2)))  (in ?s ?t2)) (not (in ?s ?t1))) :rewrite-rule) ))
+(assert-propagation ((?s elt) (?t1 set) (?t2 set))
+                  () ((not (in ?s (inter ?t1 ?t2))) (in ?s ?t2)) (not (in ?s ?t1)) ())
 
-(assert (forall ((?s elt) (?t1 set) (?t2 set))
-                (! (! (=> (and (in ?s ?t1)  (in ?s ?t2)) (in ?s (inter ?t1 ?t2))) :pattern ((inter ?t1 ?t2)) ) :rewrite-rule) ))
+(assert-propagation ((?s elt) (?t1 set) (?t2 set))
+                  () ((in ?s ?t1) (in ?s ?t2)) (in ?s (inter ?t1 ?t2)) (((inter ?t1 ?t2))) )
 
 ;;;;;;;;;;;;;;;;;
 ;; union
 
 (declare-fun union (set set)  set)
-(assert (forall ((?s elt) (?t1 set) (?t2 set))
-                (! (=> (not (in ?s (union ?t1 ?t2))) (and (not (in ?s ?t1)) (not (in ?s ?t2)))) :rewrite-rule)))
+(assert-propagation ((?s elt) (?t1 set) (?t2 set))
+                  () ((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))))
 
-(assert (forall ((?s elt) (?t1 set) (?t2 set))
-                (! (! (=> (in ?s ?t1) (in ?s (union ?t1 ?t2))) :pattern ((union ?t1 ?t2)) ) :rewrite-rule) ))
+(assert-propagation ((?s elt) (?t1 set) (?t2 set))
+                  () ((in ?s ?t2)) (in ?s (union ?t1 ?t2)) (((union ?t1 ?t2))))
 
-(assert (forall ((?s elt) (?t1 set) (?t2 set))
-                (! (! (=> (in ?s ?t2) (in ?s (union ?t1 ?t2))) :pattern ((union ?t1 ?t2)) ) :rewrite-rule) ))
+(assert-propagation ((?s elt) (?t1 set) (?t2 set))
+                  () ((in ?s (union ?t1 ?t2)) (not (in ?s ?t1))) (in ?s ?t2) ())
 
-(assert (forall ((?s elt) (?t1 set) (?t2 set))
-                (! (=> (and (in ?s (union ?t1 ?t2))  (not (in ?s ?t1))) (in ?s ?t2)) :rewrite-rule) ))
+(assert-propagation ((?s elt) (?t1 set) (?t2 set))
+                  () ((in ?s (union ?t1 ?t2)) (not (in ?s ?t2))) (in ?s ?t1) ())
 
-(assert (forall ((?s elt) (?t1 set) (?t2 set))
-                (! (=> (and (in ?s (union ?t1 ?t2))  (not (in ?s ?t2))) (in ?s ?t1)) :rewrite-rule) ))
+(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))))
 
-(assert (forall ((?s elt) (?t1 set) (?t2 set))
-                (! (! (=> (and (not (in ?s ?t1))  (not (in ?s ?t2))) (not (in ?s (union ?t1 ?t2)))) :pattern ((union ?t1 ?t2)) ) :rewrite-rule) ))
+;;;;;;;;;;;;;;;;;;;;
+;; 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))) ())
+
+(assert-propagation ((?s elt) (?t1 set) (?t2 set))
+                  () ((not (in ?s ?t1))) (not (in ?s (diff ?t1 ?t2))) (((diff ?t1 ?t2))) )
+
+(assert-propagation ((?s elt) (?t1 set) (?t2 set))
+                  () ((in ?s ?t2)) (not (in ?s (diff ?t1 ?t2))) (((diff ?t1 ?t2))))
+
+(assert-propagation ((?s elt) (?t1 set) (?t2 set))
+                  () ((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)) ())
+
+(assert-propagation ((?s elt) (?t1 set) (?t2 set))
+                  () ((in ?s ?t1) (not (in ?s ?t2))) (in ?s (diff ?t1 ?t2)) (((diff ?t1 ?t2))) )
 
 ;;;;;;;;;;;;;;;;
 ;;sing
 
 (declare-fun sing (elt)  set)
-(assert (forall ((?s elt))
-                (! (! (=> true (in ?s (sing ?s))) :pattern ((sing ?s)) ) :rewrite-rule) ))
-
-(assert (forall ((?s elt) (?t1 elt))
-                (! (=> true (=> (in ?s (sing ?t1)) (= ?s ?t1))) :rewrite-rule) ))
-
-(assert (forall ((?s elt) (?t1 elt))
-                (! (=> (not (in ?s (sing ?t1))) (not (= ?s ?t1))) :rewrite-rule) ))
+(assert-propagation ((?s elt))
+                  () () (in ?s (sing ?s)) (((sing ?s))) )
 
+(assert-propagation ((?s elt) (?t1 elt))
+                  () ((in ?s (sing ?t1))) (= ?s ?t1) ())
 
+(assert-propagation ((?s elt) (?t1 elt))
+                  () ((not (in ?s (sing ?t1)))) (not (= ?s ?t1)) ())
 
 ;;;;;;;;;;;;;;;;;;;
-;; fullfiling
-(assert (forall ((?s elt) (?t1 set) (?t2 set))
-                (! (=> (in ?s (union ?t1 ?t2)) (or (in ?s ?t1) (not (in ?s ?t1)))) :rewrite-rule)))
+;; 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))) ())
 
-(assert (forall ((?s elt) (?t1 set) (?t2 set))
-                (! (! (=> (in ?s ?t1) (or (in ?s ?t2) (not (in ?s ?t2)))) :pattern ((inter ?t1 ?t2))) :rewrite-rule)))
+(assert-propagation ((?s elt) (?t1 set) (?t2 set))
+                  () ((in ?s ?t1)) (or (in ?s ?t2) (not (in ?s ?t2))) (((inter ?t1 ?t2))))
 
-(assert (forall ((?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))))) :rewrite-rule)))
+(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)))) ())
+
+;;;;;;;;;;;;;;;;;;;
+;; shortcut
+(declare-fun subset (set set) Bool)
+(assert-reduction ((?t1 set) (?t2 set))
+                () ((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 07e9f9643..55050ac1a 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
@@ -8,76 +8,103 @@
 
 (declare-fun in (elt set) Bool)
 
+
 ;;;;;;;;;;;;;;;;;;;;
 ;; inter
 
 (declare-fun inter (set set)  set)
-(assert (forall ((?s elt) (?t1 set) (?t2 set))
-                (! (=> (in ?s (inter ?t1 ?t2)) (and (in ?s ?t1) (in ?s ?t2))) :rewrite-rule)))
+(assert-propagation ((?s elt) (?t1 set) (?t2 set)) ()
+                  ((in ?s (inter ?t1 ?t2))) (and (in ?s ?t1) (in ?s ?t2)) ())
 
 
-(assert (forall ((?s elt) (?t1 set) (?t2 set))
-                (! (! (=> (not (in ?s ?t1)) (not (in ?s (inter ?t1 ?t2)))) :pattern ((inter ?t1 ?t2)) ) :rewrite-rule) ))
+(assert-propagation ((?s elt) (?t1 set) (?t2 set))
+                  () ((not (in ?s ?t1))) (not (in ?s (inter ?t1 ?t2))) (((inter ?t1 ?t2))) )
 
-(assert (forall ((?s elt) (?t1 set) (?t2 set))
-                (! (! (=> (not (in ?s ?t2)) (not (in ?s (inter ?t1 ?t2)))) :pattern ((inter ?t1 ?t2)) ) :rewrite-rule) ))
+(assert-propagation ((?s elt) (?t1 set) (?t2 set))
+                  () ((not (in ?s ?t2))) (not (in ?s (inter ?t1 ?t2))) (((inter ?t1 ?t2))) )
 
-(assert (forall ((?s elt) (?t1 set) (?t2 set))
-                (! (=> (and (not (in ?s (inter ?t1 ?t2)))  (in ?s ?t1)) (not (in ?s ?t2))) :rewrite-rule) ))
+(assert-propagation ((?s elt) (?t1 set) (?t2 set))
+                  () ((not (in ?s (inter ?t1 ?t2))) (in ?s ?t1)) (not (in ?s ?t2)) () )
 
-(assert (forall ((?s elt) (?t1 set) (?t2 set))
-                (! (=> (and (not (in ?s (inter ?t1 ?t2)))  (in ?s ?t2)) (not (in ?s ?t1))) :rewrite-rule) ))
+(assert-propagation ((?s elt) (?t1 set) (?t2 set))
+                  () ((not (in ?s (inter ?t1 ?t2))) (in ?s ?t2)) (not (in ?s ?t1)) ())
 
-(assert (forall ((?s elt) (?t1 set) (?t2 set))
-                (! (! (=> (and (in ?s ?t1)  (in ?s ?t2)) (in ?s (inter ?t1 ?t2))) :pattern ((inter ?t1 ?t2)) ) :rewrite-rule) ))
+(assert-propagation ((?s elt) (?t1 set) (?t2 set))
+                  () ((in ?s ?t1) (in ?s ?t2)) (in ?s (inter ?t1 ?t2)) (((inter ?t1 ?t2))) )
 
 ;;;;;;;;;;;;;;;;;
 ;; union
 
 (declare-fun union (set set)  set)
-(assert (forall ((?s elt) (?t1 set) (?t2 set))
-                (! (=> (not (in ?s (union ?t1 ?t2))) (and (not (in ?s ?t1)) (not (in ?s ?t2)))) :rewrite-rule)))
+(assert-propagation ((?s elt) (?t1 set) (?t2 set))
+                  () ((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))))
+
+(assert-propagation ((?s elt) (?t1 set) (?t2 set))
+                  () ((in ?s ?t2)) (in ?s (union ?t1 ?t2)) (((union ?t1 ?t2))))
+
+(assert-propagation ((?s elt) (?t1 set) (?t2 set))
+                  () ((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) ())
+
+(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))))
 
+;;;;;;;;;;;;;;;;;;;;
+;; 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))) ())
 
-(assert (forall ((?s elt) (?t1 set) (?t2 set))
-                (! (! (=> (in ?s ?t1) (in ?s (union ?t1 ?t2))) :pattern ((union ?t1 ?t2)) ) :rewrite-rule) ))
+(assert-propagation ((?s elt) (?t1 set) (?t2 set))
+                  () ((not (in ?s ?t1))) (not (in ?s (diff ?t1 ?t2))) (((diff ?t1 ?t2))) )
 
-(assert (forall ((?s elt) (?t1 set) (?t2 set))
-                (! (! (=> (in ?s ?t2) (in ?s (union ?t1 ?t2))) :pattern ((union ?t1 ?t2)) ) :rewrite-rule) ))
+(assert-propagation ((?s elt) (?t1 set) (?t2 set))
+                  () ((in ?s ?t2)) (not (in ?s (diff ?t1 ?t2))) (((diff ?t1 ?t2))))
 
-(assert (forall ((?s elt) (?t1 set) (?t2 set))
-                (! (=> (and (in ?s (union ?t1 ?t2))  (not (in ?s ?t1))) (in ?s ?t2)) :rewrite-rule) ))
+(assert-propagation ((?s elt) (?t1 set) (?t2 set))
+                  () ((not (in ?s (diff ?t1 ?t2))) (in ?s ?t1)) (in ?s ?t2) ())
 
-(assert (forall ((?s elt) (?t1 set) (?t2 set))
-                (! (=> (and (in ?s (union ?t1 ?t2))  (not (in ?s ?t2))) (in ?s ?t1)) :rewrite-rule) ))
+(assert-propagation ((?s elt) (?t1 set) (?t2 set))
+                  () ((not (in ?s (diff ?t1 ?t2))) (not (in ?s ?t2))) (not (in ?s ?t1)) ())
 
-(assert (forall ((?s elt) (?t1 set) (?t2 set))
-                (! (! (=> (and (not (in ?s ?t1))  (not (in ?s ?t2))) (not (in ?s (union ?t1 ?t2)))) :pattern ((union ?t1 ?t2)) ) :rewrite-rule) ))
+(assert-propagation ((?s elt) (?t1 set) (?t2 set))
+                  () ((in ?s ?t1) (not (in ?s ?t2))) (in ?s (diff ?t1 ?t2)) (((diff ?t1 ?t2))) )
 
 ;;;;;;;;;;;;;;;;
 ;;sing
 
 (declare-fun sing (elt)  set)
-(assert (forall ((?s elt))
-                (! (! (=> true (in ?s (sing ?s))) :pattern ((sing ?s)) ) :rewrite-rule) ))
-
-(assert (forall ((?s elt) (?t1 elt))
-                (! (=> true (=> (in ?s (sing ?t1)) (= ?s ?t1))) :rewrite-rule) ))
-
-(assert (forall ((?s elt) (?t1 elt))
-                (! (=> (not (in ?s (sing ?t1))) (not (= ?s ?t1))) :rewrite-rule) ))
+(assert-propagation ((?s elt))
+                  () () (in ?s (sing ?s)) (((sing ?s))) )
 
+(assert-propagation ((?s elt) (?t1 elt))
+                  () ((in ?s (sing ?t1))) (= ?s ?t1) ())
 
+(assert-propagation ((?s elt) (?t1 elt))
+                  () ((not (in ?s (sing ?t1)))) (not (= ?s ?t1)) ())
 
 ;;;;;;;;;;;;;;;;;;;
-;; fullfiling
-(assert (forall ((?s elt) (?t1 set) (?t2 set))
-                (! (=> (in ?s (union ?t1 ?t2)) (or (in ?s ?t1) (not (in ?s ?t1)))) :rewrite-rule)))
+;; 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))) ())
+
+(assert-propagation ((?s elt) (?t1 set) (?t2 set))
+                  () ((in ?s ?t1)) (or (in ?s ?t2) (not (in ?s ?t2))) (((inter ?t1 ?t2))))
 
-(assert (forall ((?s elt) (?t1 set) (?t2 set))
-                (! (! (=> (in ?s ?t1) (or (in ?s ?t2) (not (in ?s ?t2)))) :pattern ((inter ?t1 ?t2))) :rewrite-rule)))
+(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)))) ())
 
-;; (assert (forall ((?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))))) )))
+;;;;;;;;;;;;;;;;;;;
+;; shortcut
+(declare-fun subset (set set) Bool)
+(assert-reduction ((?t1 set) (?t2 set))
+                () ((subset ?t1 ?t2)) (= (union ?t1 ?t2) ?t2) ())
 
 (declare-fun e () elt)
 (declare-fun t1 () set)
diff --git a/test/regress/regress0/rewriterules/simulate_rewritting.smt2 b/test/regress/regress0/rewriterules/simulate_rewritting.smt2
new file mode 100644
index 000000000..d1d88a549
--- /dev/null
+++ b/test/regress/regress0/rewriterules/simulate_rewritting.smt2
@@ -0,0 +1,24 @@
+;; A new fast tableau-base ... Domenico Cantone et Calogero G.Zarba
+(set-logic AUFLIA)
+(set-info :status sat)
+
+(declare-sort elt1 0)
+(declare-sort elt2 0)
+
+(declare-fun g (elt2) Bool)
+
+(declare-fun p (elt1 elt1) Bool)
+(declare-fun f (elt2) elt1)
+(declare-fun c1 () elt1)
+(declare-fun c2 () elt1)
+
+(assert (forall ((?e elt2)) (! (=> (g ?e) (= (f ?e) c2)) :rewrite-rule)))
+(assert (forall ((?e elt2)) (! (=> (g ?e) (= (f ?e) c1)) :rewrite-rule)))
+
+(declare-fun e () elt2)
+
+(assert (not (=> (g e) (=> (p c1 c2) (p (f e) (f e)))) ))
+
+(check-sat)
+
+(exit)
diff --git a/test/regress/regress0/rewriterules/test_efficient_ematching.smt2 b/test/regress/regress0/rewriterules/test_efficient_ematching.smt2
new file mode 100644
index 000000000..e91ef36c2
--- /dev/null
+++ b/test/regress/regress0/rewriterules/test_efficient_ematching.smt2
@@ -0,0 +1,35 @@
+(set-logic AUFLIA)
+(set-info :status unsat)
+
+;; don't use a datatypes for currently focusing in uf
+(declare-sort elt 0)
+
+(declare-fun R (elt elt) Bool)
+
+;; reflexive
+(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) ())
+
+;; anti-symmetric
+(assert-propagation ((x elt) (y elt)) () ((R x y) (R y x)) (= x y) ())
+
+(declare-fun f (elt) elt)
+(assert-propagation ((x elt)(y elt)) () ((R (f x) (f y))) (R x y) ())
+
+
+(declare-fun e1 () elt)
+(declare-fun e2 () elt)
+(declare-fun e3 () elt)
+(declare-fun e4 () elt)
+(declare-fun e5 () elt)
+
+(assert (not (=> (and (R e1 e2) (R e3 (f e4)) (R e4 e5)
+                      (or (and (= e3 (f e2)) (= e4 e1))
+                          (and (= e4 e2) (= e5 e1)) )
+        ) (= e1 e2))))
+
+(check-sat)
+
+(exit)
\ No newline at end of file