sets: Rename set.intersection to set.inter. (#7622)

This further renames kind SET_INTERSECTION to SET_INTER.

52 files changed, 70 insertions, 70 deletions

diff --git a/test/regress/regress0/rels/addr_book_0.cvc.smt2 b/test/regress/regress0/rels/addr_book_0.cvc.smt2
index 70488b4eb..9bc85f268 100644
--- a/test/regress/regress0/rels/addr_book_0.cvc.smt2
+++ b/test/regress/regress0/rels/addr_book_0.cvc.smt2
@@ -33,7 +33,7 @@
 (assert (set.member t_tup Target))
 (assert (set.subset (rel.join (rel.join Book addr) Target) Name))
 (assert (set.subset (rel.join Book names) Name))
-(assert (= (set.intersection Name Addr) (as set.empty (Set (Tuple Atom)))))
+(assert (= (set.inter Name Addr) (as set.empty (Set (Tuple Atom)))))
 (assert (= (rel.join (set.singleton n_tup) (rel.join (set.singleton b1_tup) addr)) (as set.empty (Set (Tuple Atom)))))
 (assert (let ((_let_1 (set.singleton n_tup))) (= (rel.join _let_1 (rel.join (set.singleton b2_tup) addr)) (set.union (rel.join _let_1 (rel.join (set.singleton b1_tup) addr)) (set.singleton t_tup)))))
 (assert (let ((_let_1 (set.singleton n_tup))) (= (rel.join _let_1 (rel.join (set.singleton b3_tup) addr)) (set.minus (rel.join _let_1 (rel.join (set.singleton b2_tup) addr)) (set.singleton t_tup)))))
diff --git a/test/regress/regress0/rels/iden_0.cvc.smt2 b/test/regress/regress0/rels/iden_0.cvc.smt2
index 1cdeffbff..75dc80d22 100644
--- a/test/regress/regress0/rels/iden_0.cvc.smt2
+++ b/test/regress/regress0/rels/iden_0.cvc.smt2
@@ -21,5 +21,5 @@
 (assert (set.member v x))
 (assert (set.member a x))
 (assert (= id (rel.iden t)))
-(assert (not (set.member (tuple 1 1) (set.intersection id x))))
+(assert (not (set.member (tuple 1 1) (set.inter id x))))
 (check-sat)
diff --git a/test/regress/regress0/sets/complement3.cvc.smt2 b/test/regress/regress0/sets/complement3.cvc.smt2
index 20cfb36f8..2046b2fc9 100644
--- a/test/regress/regress0/sets/complement3.cvc.smt2
+++ b/test/regress/regress0/sets/complement3.cvc.smt2
@@ -8,7 +8,7 @@
 (declare-fun C4 () (Set (Tuple Atom)))
 (declare-fun ATOM_UNIV () (Set (Tuple Atom)))
 (declare-fun V1 () Atom)
-(assert (= C32 (set.intersection (set.complement C2) (set.complement C4))))
+(assert (= C32 (set.inter (set.complement C2) (set.complement C4))))
 (assert (set.member (tuple V1) (set.complement C32)))
 (assert (= ATOM_UNIV (as set.universe (Set (Tuple Atom)))))
 (assert (set.member (tuple V1) ATOM_UNIV))
diff --git a/test/regress/regress0/sets/cvc-sample.cvc.smt2 b/test/regress/regress0/sets/cvc-sample.cvc.smt2
index 9ee199b43..9c89df0c6 100644
--- a/test/regress/regress0/sets/cvc-sample.cvc.smt2
+++ b/test/regress/regress0/sets/cvc-sample.cvc.smt2
@@ -20,12 +20,12 @@
 (declare-fun e () Int)
 (assert (= a (set.singleton 5)))
 (assert (= c (set.union a b)))
-(assert (not (= c (set.intersection a b))))
+(assert (not (= c (set.inter a b))))
 (assert (= c (set.minus a b)))
 (assert (set.subset a b))
 (assert (set.member e c))
 (assert (set.member e a))
-(assert (set.member e (set.intersection a b)))
+(assert (set.member e (set.inter a b)))
 (push 1)
 
 (assert true)
diff --git a/test/regress/regress0/sets/eqtest.smt2 b/test/regress/regress0/sets/eqtest.smt2
index 0ecd32bf8..c93b18857 100644
--- a/test/regress/regress0/sets/eqtest.smt2
+++ b/test/regress/regress0/sets/eqtest.smt2
@@ -10,9 +10,9 @@
 (declare-fun H () (Set Int) )
 (declare-fun I () (Set Int) )
 (declare-fun x () Int)
-(assert (set.member x (set.intersection (set.union A B) C)))
+(assert (set.member x (set.inter (set.union A B) C)))
 (assert (not (set.member x G)))
 (assert (= (set.union A B) D))
-(assert (= C (set.intersection E F)))
+(assert (= C (set.inter E F)))
 (assert (and (= F H) (= G H) (= H I)))
 (check-sat)
diff --git a/test/regress/regress0/sets/jan24/deepmeas0.hs.fqout.cvc4.47.smt2 b/test/regress/regress0/sets/jan24/deepmeas0.hs.fqout.cvc4.47.smt2
index 7e2f627ae..76592a691 100644
--- a/test/regress/regress0/sets/jan24/deepmeas0.hs.fqout.cvc4.47.smt2
+++ b/test/regress/regress0/sets/jan24/deepmeas0.hs.fqout.cvc4.47.smt2
@@ -6,7 +6,7 @@
 (define-fun smt_set_mem ((x Elt) (s mySet)) Bool (set.member x s))
 (define-fun smt_set_add ((s mySet) (x Elt)) mySet (set.union s (set.singleton x)))
 (define-fun smt_set_cup ((s1 mySet) (s2 mySet)) mySet (set.union s1 s2))
-(define-fun smt_set_cap ((s1 mySet) (s2 mySet)) mySet (set.intersection s1 s2))
+(define-fun smt_set_cap ((s1 mySet) (s2 mySet)) mySet (set.inter s1 s2))
 
 (define-fun smt_set_dif ((s1 mySet) (s2 mySet)) mySet (set.minus s1 s2))
 
diff --git a/test/regress/regress0/sets/jan27/ListConcat.hs.fqout.cvc4.177.smt2 b/test/regress/regress0/sets/jan27/ListConcat.hs.fqout.cvc4.177.smt2
index f6fd4bd53..b0172db39 100644
--- a/test/regress/regress0/sets/jan27/ListConcat.hs.fqout.cvc4.177.smt2
+++ b/test/regress/regress0/sets/jan27/ListConcat.hs.fqout.cvc4.177.smt2
@@ -6,7 +6,7 @@
 (define-fun smt_set_mem ((x Elt) (s mySet)) Bool (set.member x s))
 (define-fun smt_set_add ((s mySet) (x Elt)) mySet (set.union s (set.singleton x)))
 (define-fun smt_set_cup ((s1 mySet) (s2 mySet)) mySet (set.union s1 s2))
-(define-fun smt_set_cap ((s1 mySet) (s2 mySet)) mySet (set.intersection s1 s2))
+(define-fun smt_set_cap ((s1 mySet) (s2 mySet)) mySet (set.inter s1 s2))
 ;(define-fun smt_set_com ((s mySet)) mySet ((_ map not) s))
 (define-fun smt_set_dif ((s1 mySet) (s2 mySet)) mySet (set.minus s1 s2))
 ;(define-fun smt_set_sub ((s1 mySet) (s2 mySet)) Bool (= smt_set_emp (smt_set_dif s1 s2)))
diff --git a/test/regress/regress0/sets/rec_copy_loop_check_heap_access_43_4.smt2 b/test/regress/regress0/sets/rec_copy_loop_check_heap_access_43_4.smt2
index f70d59b16..1538a2e9f 100644
--- a/test/regress/regress0/sets/rec_copy_loop_check_heap_access_43_4.smt2
+++ b/test/regress/regress0/sets/rec_copy_loop_check_heap_access_43_4.smt2
@@ -66,7 +66,7 @@
 
 (assert (! (= sk_?X_36$0 FP$0) :named precondition_of_rec_copy_loop_34_11_18))
 
-(assert (! (= (as set.empty SetLoc) (set.intersection sk_?X_38$0 sk_?X_37$0))
+(assert (! (= (as set.empty SetLoc) (set.inter sk_?X_38$0 sk_?X_37$0))
    :named precondition_of_rec_copy_loop_34_11_19))
 
 (assert (! (= old_cp_2$0 cp$0) :named assign_41_4))
diff --git a/test/regress/regress0/sets/sets-inter.smt2 b/test/regress/regress0/sets/sets-inter.smt2
index 6857e5147..66f843c9d 100644
--- a/test/regress/regress0/sets/sets-inter.smt2
+++ b/test/regress/regress0/sets/sets-inter.smt2
@@ -5,7 +5,7 @@
 (declare-fun b () (Set Int))
 (declare-fun x () Int)
 ;(assert (not (set.member x a)))
-(assert (set.member x (set.intersection a b)))
+(assert (set.member x (set.inter a b)))
 (assert (not (set.member x b)))
 (check-sat)
 (exit)
diff --git a/test/regress/regress0/sets/sets-new.smt2 b/test/regress/regress0/sets/sets-new.smt2
index 4a49bef07..0020e5c55 100644
--- a/test/regress/regress0/sets/sets-new.smt2
+++ b/test/regress/regress0/sets/sets-new.smt2
@@ -8,7 +8,7 @@
 (declare-fun x () Int)
 (assert (set.member x (set.union A B)))
 
-(assert (not (set.member x (set.intersection A B))))
+(assert (not (set.member x (set.inter A B))))
 (assert (not (set.member x (set.minus A B))))
 ;(assert (not (set.member x (set.minus B A))))
 ;(assert (set.member x B))
diff --git a/test/regress/regress0/sets/sets-poly-int-real.smt2 b/test/regress/regress0/sets/sets-poly-int-real.smt2
index 20832c573..00546eee2 100644
--- a/test/regress/regress0/sets/sets-poly-int-real.smt2
+++ b/test/regress/regress0/sets/sets-poly-int-real.smt2
@@ -11,7 +11,7 @@
 (assert (= t1 (set.union s (set.singleton 2.5))))
 (assert (= t2 (set.union s (set.singleton 2.0))))
 (assert (= t3 (set.union r3 (set.singleton 2.5))))
-(assert (= (set.intersection r1 r2) (set.intersection s (set.singleton 0.0))))
+(assert (= (set.inter r1 r2) (set.inter s (set.singleton 0.0))))
 (assert (not (= r1 (as set.empty (Set Real)))))
 
 (check-sat)
diff --git a/test/regress/regress0/sets/sets-sample.smt2 b/test/regress/regress0/sets/sets-sample.smt2
index 3dcafae08..4a11bcc78 100644
--- a/test/regress/regress0/sets/sets-sample.smt2
+++ b/test/regress/regress0/sets/sets-sample.smt2
@@ -15,12 +15,12 @@
 (declare-fun e () Int)
 (assert (= a (set.singleton 5)))
 (assert (= c (set.union a b) ))
-(assert (not (= c (set.intersection a b) )))
+(assert (not (= c (set.inter a b) )))
 (assert (= c (set.minus a b) ))
 (assert (set.subset a b))
 (assert (set.member e c))
 (assert (set.member e a))
-(assert (set.member e (set.intersection a b)))
+(assert (set.member e (set.inter a b)))
 (check-sat)
 (pop 1)
 
diff --git a/test/regress/regress0/sets/sharing-simp.smt2 b/test/regress/regress0/sets/sharing-simp.smt2
index be746be1d..a591792cf 100644
--- a/test/regress/regress0/sets/sharing-simp.smt2
+++ b/test/regress/regress0/sets/sharing-simp.smt2
@@ -9,7 +9,7 @@
 
 (assert (set.member x A))
 (assert (set.member y B))
-(assert (or (= C (set.intersection A B)) (= D (set.intersection A B))))
+(assert (or (= C (set.inter A B)) (= D (set.inter A B))))
 
 
 (check-sat)
diff --git a/test/regress/regress1/quantifiers/set8.smt2 b/test/regress/regress1/quantifiers/set8.smt2
index 209b213c1..17eea7b0a 100644
--- a/test/regress/regress1/quantifiers/set8.smt2
+++ b/test/regress/regress1/quantifiers/set8.smt2
@@ -15,12 +15,12 @@
 (assert (forall ((?s1 Set) (?s2 Set)) (= (seteq ?s1 ?s2) (and (set.subset ?s1 ?s2) (set.subset ?s2 ?s1)))))
 (declare-fun union (Set Set) Set)
 (assert (forall ((?x Elem) (?s1 Set) (?s2 Set)) (= (set.member ?x (union ?s1 ?s2)) (or (set.member ?x ?s1) (set.member ?x ?s2)))))
-(declare-fun set.intersection (Set Set) Set)
-(assert (forall ((?x Elem) (?s1 Set) (?s2 Set)) (= (set.member ?x (set.intersection ?s1 ?s2)) (and (set.member ?x ?s1) (set.member ?x ?s2)))))
+(declare-fun set.inter (Set Set) Set)
+(assert (forall ((?x Elem) (?s1 Set) (?s2 Set)) (= (set.member ?x (set.inter ?s1 ?s2)) (and (set.member ?x ?s1) (set.member ?x ?s2)))))
 (declare-fun difference (Set Set) Set)
 (assert (forall ((?x Elem) (?s1 Set) (?s2 Set)) (= (set.member ?x (difference ?s1 ?s2)) (and (set.member ?x ?s1) (not (set.member ?x ?s2))))))
 (declare-fun a () Set)
 (declare-fun b () Set)
-(assert (not (seteq (set.intersection a b) (set.intersection b a))))
+(assert (not (seteq (set.inter a b) (set.inter b a))))
 (check-sat)
 (exit)
diff --git a/test/regress/regress1/rels/rel_complex_3.cvc.smt2 b/test/regress/regress1/rels/rel_complex_3.cvc.smt2
index 7e80fdd70..8269daf42 100644
--- a/test/regress/regress1/rels/rel_complex_3.cvc.smt2
+++ b/test/regress/regress1/rels/rel_complex_3.cvc.smt2
@@ -20,12 +20,12 @@
 (assert (= r (rel.join x y)))
 (declare-fun e () (Tuple Int Int))
 (assert (not (set.member e r)))
-(assert (not (= z (set.intersection x y))))
+(assert (not (= z (set.inter x y))))
 (assert (= z (set.minus x y)))
 (assert (set.subset x y))
 (assert (set.member e (rel.join r z)))
 (assert (set.member e x))
-(assert (set.member e (set.intersection x y)))
+(assert (set.member e (set.inter x y)))
 (push 1)
 
 (assert true)
diff --git a/test/regress/regress1/rels/rel_complex_4.cvc.smt2 b/test/regress/regress1/rels/rel_complex_4.cvc.smt2
index 9a35f336e..134a99c73 100644
--- a/test/regress/regress1/rels/rel_complex_4.cvc.smt2
+++ b/test/regress/regress1/rels/rel_complex_4.cvc.smt2
@@ -24,12 +24,12 @@
 (assert (= w (set.singleton e)))
 (assert (set.subset (rel.transpose w) y))
 (assert (not (set.member e r)))
-(assert (not (= z (set.intersection x y))))
+(assert (not (= z (set.inter x y))))
 (assert (= z (set.minus x y)))
 (assert (set.subset x y))
 (assert (set.member e (rel.join r z)))
 (assert (set.member e x))
-(assert (set.member e (set.intersection x y)))
+(assert (set.member e (set.inter x y)))
 (push 1)
 
 (assert true)
diff --git a/test/regress/regress1/rels/rel_complex_5.cvc.smt2 b/test/regress/regress1/rels/rel_complex_5.cvc.smt2
index fc2d73235..ed894518e 100644
--- a/test/regress/regress1/rels/rel_complex_5.cvc.smt2
+++ b/test/regress/regress1/rels/rel_complex_5.cvc.smt2
@@ -26,12 +26,12 @@
 (assert (let ((_let_1 (set.singleton a))) (= w (rel.product _let_1 _let_1))))
 (assert (set.subset (rel.transpose w) y))
 (assert (not (set.member e r)))
-(assert (not (= z (set.intersection x y))))
+(assert (not (= z (set.inter x y))))
 (assert (= z (set.minus x y)))
 (assert (set.subset x y))
 (assert (set.member e (rel.join r z)))
 (assert (set.member e x))
-(assert (set.member e (set.intersection x y)))
+(assert (set.member e (set.inter x y)))
 (push 1)
 
 (assert true)
diff --git a/test/regress/regress1/sets/ListElem.hs.fqout.cvc4.38.smt2 b/test/regress/regress1/sets/ListElem.hs.fqout.cvc4.38.smt2
index 144566fc5..e5b92a4fc 100644
--- a/test/regress/regress1/sets/ListElem.hs.fqout.cvc4.38.smt2
+++ b/test/regress/regress1/sets/ListElem.hs.fqout.cvc4.38.smt2
@@ -12,7 +12,7 @@
 (define-fun smt_set_mem ((x Elt) (s mySet)) Bool (set.member x s))
 (define-fun smt_set_add ((s mySet) (x Elt)) mySet (set.union s (set.singleton x)))
 (define-fun smt_set_cup ((s1 mySet) (s2 mySet)) mySet (set.union s1 s2))
-(define-fun smt_set_cap ((s1 mySet) (s2 mySet)) mySet (set.intersection s1 s2))
+(define-fun smt_set_cap ((s1 mySet) (s2 mySet)) mySet (set.inter s1 s2))
 ;(define-fun smt_set_com ((s mySet)) mySet ((_ map not) s))
 (define-fun smt_set_dif ((s1 mySet) (s2 mySet)) mySet (set.minus s1 s2))
 ;(define-fun smt_set_sub ((s1 mySet) (s2 mySet)) Bool (= smt_set_emp (smt_set_dif s1 s2)))
diff --git a/test/regress/regress1/sets/ListElts.hs.fqout.cvc4.317.smt2 b/test/regress/regress1/sets/ListElts.hs.fqout.cvc4.317.smt2
index 9a2521520..206450142 100644
--- a/test/regress/regress1/sets/ListElts.hs.fqout.cvc4.317.smt2
+++ b/test/regress/regress1/sets/ListElts.hs.fqout.cvc4.317.smt2
@@ -7,7 +7,7 @@
 (define-fun smt_set_mem ((x Elt) (s mySet)) Bool (set.member x s))
 (define-fun smt_set_add ((s mySet) (x Elt)) mySet (set.union s (set.singleton x)))
 (define-fun smt_set_cup ((s1 mySet) (s2 mySet)) mySet (set.union s1 s2))
-(define-fun smt_set_cap ((s1 mySet) (s2 mySet)) mySet (set.intersection s1 s2))
+(define-fun smt_set_cap ((s1 mySet) (s2 mySet)) mySet (set.inter s1 s2))
 ;(define-fun smt_set_com ((s mySet)) mySet ((_ map not) s))
 (define-fun smt_set_dif ((s1 mySet) (s2 mySet)) mySet (set.minus s1 s2))
 ;(define-fun smt_set_sub ((s1 mySet) (s2 mySet)) Bool (= smt_set_emp (smt_set_dif s1 s2)))
diff --git a/test/regress/regress1/sets/TalkingAboutSets.hs.fqout.cvc4.3577.smt2 b/test/regress/regress1/sets/TalkingAboutSets.hs.fqout.cvc4.3577.smt2
index b2732dbd2..fe7e7d7ac 100644
--- a/test/regress/regress1/sets/TalkingAboutSets.hs.fqout.cvc4.3577.smt2
+++ b/test/regress/regress1/sets/TalkingAboutSets.hs.fqout.cvc4.3577.smt2
@@ -7,7 +7,7 @@
 (define-fun smt_set_mem ((x Elt) (s mySet)) Bool (set.member x s))
 (define-fun smt_set_add ((s mySet) (x Elt)) mySet (set.union s (set.singleton x)))
 (define-fun smt_set_cup ((s1 mySet) (s2 mySet)) mySet (set.union s1 s2))
-(define-fun smt_set_cap ((s1 mySet) (s2 mySet)) mySet (set.intersection s1 s2))
+(define-fun smt_set_cap ((s1 mySet) (s2 mySet)) mySet (set.inter s1 s2))
 ;(define-fun smt_set_com ((s mySet)) mySet ((_ map not) s))
 (define-fun smt_set_dif ((s1 mySet) (s2 mySet)) mySet (set.minus s1 s2))
 ;(define-fun smt_set_sub ((s1 mySet) (s2 mySet)) Bool (= smt_set_emp (smt_set_dif s1 s2)))
diff --git a/test/regress/regress1/sets/UniqueZipper.hs.1030minimized.cvc4.smt2 b/test/regress/regress1/sets/UniqueZipper.hs.1030minimized.cvc4.smt2
index ee24367c3..078b98eef 100644
--- a/test/regress/regress1/sets/UniqueZipper.hs.1030minimized.cvc4.smt2
+++ b/test/regress/regress1/sets/UniqueZipper.hs.1030minimized.cvc4.smt2
@@ -6,7 +6,7 @@
 (define-fun smt_set_mem ((x Elt) (s mySet)) Bool (set.member x s))
 (define-fun smt_set_add ((s mySet) (x Elt)) mySet (set.union s (set.singleton x)))
 (define-fun smt_set_cup ((s1 mySet) (s2 mySet)) mySet (set.union s1 s2))
-(define-fun smt_set_cap ((s1 mySet) (s2 mySet)) mySet (set.intersection s1 s2))
+(define-fun smt_set_cap ((s1 mySet) (s2 mySet)) mySet (set.inter s1 s2))
 (define-fun smt_set_dif ((s1 mySet) (s2 mySet)) mySet (set.minus s1 s2))
 (define-fun smt_set_sub ((s1 mySet) (s2 mySet)) Bool (set.subset s1 s2))
 
diff --git a/test/regress/regress1/sets/UniqueZipper.hs.1030minimized2.cvc4.smt2 b/test/regress/regress1/sets/UniqueZipper.hs.1030minimized2.cvc4.smt2
index b0cfe4888..756f0430c 100644
--- a/test/regress/regress1/sets/UniqueZipper.hs.1030minimized2.cvc4.smt2
+++ b/test/regress/regress1/sets/UniqueZipper.hs.1030minimized2.cvc4.smt2
@@ -6,7 +6,7 @@
 (define-fun smt_set_mem ((x Elt) (s mySet)) Bool (set.member x s))
 (define-fun smt_set_add ((s mySet) (x Elt)) mySet (set.union s (set.singleton x)))
 (define-fun smt_set_cup ((s1 mySet) (s2 mySet)) mySet (set.union s1 s2))
-(define-fun smt_set_cap ((s1 mySet) (s2 mySet)) mySet (set.intersection s1 s2))
+(define-fun smt_set_cap ((s1 mySet) (s2 mySet)) mySet (set.inter s1 s2))
 (define-fun smt_set_dif ((s1 mySet) (s2 mySet)) mySet (set.minus s1 s2))
 (define-fun smt_set_sub ((s1 mySet) (s2 mySet)) Bool (set.subset s1 s2))
 
diff --git a/test/regress/regress1/sets/UniqueZipper.hs.fqout.cvc4.10.smt2 b/test/regress/regress1/sets/UniqueZipper.hs.fqout.cvc4.10.smt2
index 9ac15e9a4..1e45c21e9 100644
--- a/test/regress/regress1/sets/UniqueZipper.hs.fqout.cvc4.10.smt2
+++ b/test/regress/regress1/sets/UniqueZipper.hs.fqout.cvc4.10.smt2
@@ -6,7 +6,7 @@
 (define-fun smt_set_mem ((x Elt) (s mySet)) Bool (set.member x s))
 (define-fun smt_set_add ((s mySet) (x Elt)) mySet (set.union s (set.singleton x)))
 (define-fun smt_set_cup ((s1 mySet) (s2 mySet)) mySet (set.union s1 s2))
-(define-fun smt_set_cap ((s1 mySet) (s2 mySet)) mySet (set.intersection s1 s2))
+(define-fun smt_set_cap ((s1 mySet) (s2 mySet)) mySet (set.inter s1 s2))
 (define-fun smt_set_dif ((s1 mySet) (s2 mySet)) mySet (set.minus s1 s2))
 (define-fun smt_set_sub ((s1 mySet) (s2 mySet)) Bool (set.subset s1 s2))
 (declare-fun z3v66 () Int)
diff --git a/test/regress/regress1/sets/UniqueZipper.hs.fqout.cvc4.1832.smt2 b/test/regress/regress1/sets/UniqueZipper.hs.fqout.cvc4.1832.smt2
index 68ed72a93..a3fd883b6 100644
--- a/test/regress/regress1/sets/UniqueZipper.hs.fqout.cvc4.1832.smt2
+++ b/test/regress/regress1/sets/UniqueZipper.hs.fqout.cvc4.1832.smt2
@@ -6,7 +6,7 @@
 (define-fun smt_set_mem ((x Elt) (s mySet)) Bool (set.member x s))
 (define-fun smt_set_add ((s mySet) (x Elt)) mySet (set.union s (set.singleton x)))
 (define-fun smt_set_cup ((s1 mySet) (s2 mySet)) mySet (set.union s1 s2))
-(define-fun smt_set_cap ((s1 mySet) (s2 mySet)) mySet (set.intersection s1 s2))
+(define-fun smt_set_cap ((s1 mySet) (s2 mySet)) mySet (set.inter s1 s2))
 ;(define-fun smt_set_com ((s mySet)) mySet ((_ map not) s))
 (define-fun smt_set_dif ((s1 mySet) (s2 mySet)) mySet (set.minus s1 s2))
 ;(define-fun smt_set_sub ((s1 mySet) (s2 mySet)) Bool (= smt_set_emp (smt_set_dif s1 s2)))
diff --git a/test/regress/regress1/sets/card-3.smt2 b/test/regress/regress1/sets/card-3.smt2
index 383395b0d..bbcf1c489 100644
--- a/test/regress/regress1/sets/card-3.smt2
+++ b/test/regress/regress1/sets/card-3.smt2
@@ -8,5 +8,5 @@
 (assert (>= (set.card (set.union s u)) 8))
 (assert (<= (set.card (set.union t u)) 5))
 (assert (<= (set.card s) 5))
-(assert (= (as set.empty (Set E)) (set.intersection t u)))
+(assert (= (as set.empty (Set E)) (set.inter t u)))
 (check-sat)
diff --git a/test/regress/regress1/sets/card-4.smt2 b/test/regress/regress1/sets/card-4.smt2
index 019b16a09..9f0e96dc5 100644
--- a/test/regress/regress1/sets/card-4.smt2
+++ b/test/regress/regress1/sets/card-4.smt2
@@ -8,7 +8,7 @@
 (assert (>= (set.card (set.union s u)) 8))
 ;(assert (<= (set.card (set.union t u)) 5))
 (assert (<= (set.card s) 5))
-(assert (= (as set.empty (Set E)) (set.intersection t u)))
+(assert (= (as set.empty (Set E)) (set.inter t u)))
 (declare-fun x1 () E)
 (declare-fun x2 () E)
 (declare-fun x3 () E)
diff --git a/test/regress/regress1/sets/card-5.smt2 b/test/regress/regress1/sets/card-5.smt2
index c24ca974a..51ad7971c 100644
--- a/test/regress/regress1/sets/card-5.smt2
+++ b/test/regress/regress1/sets/card-5.smt2
@@ -8,7 +8,7 @@
 (assert (>= (set.card (set.union s u)) 8))
 ;(assert (<= (set.card (set.union t u)) 5))
 (assert (<= (set.card s) 5))
-(assert (= (as set.empty (Set E)) (set.intersection t u)))
+(assert (= (as set.empty (Set E)) (set.inter t u)))
 (declare-fun x1 () E)
 (declare-fun x2 () E)
 (declare-fun x3 () E)
diff --git a/test/regress/regress1/sets/card-6.smt2 b/test/regress/regress1/sets/card-6.smt2
index b0ef3a3b9..fc2d34acc 100644
--- a/test/regress/regress1/sets/card-6.smt2
+++ b/test/regress/regress1/sets/card-6.smt2
@@ -7,7 +7,7 @@
 (assert
   (and
     (= (as set.empty (Set E))
-       (set.intersection A B))
+       (set.inter A B))
     (set.subset C (set.union A B))
     (>= (set.card C) 5)
     (<= (set.card A) 2)
diff --git a/test/regress/regress1/sets/comp-intersect.smt2 b/test/regress/regress1/sets/comp-intersect.smt2
index 60d9046bd..5f6f7576b 100644
--- a/test/regress/regress1/sets/comp-intersect.smt2
+++ b/test/regress/regress1/sets/comp-intersect.smt2
@@ -9,6 +9,6 @@
 (assert (= x (set.comprehension ((z Int)) (> z 4) (* 5 z))))
 (assert (= y (set.comprehension ((z Int)) (< z 10) (+ (* 5 z) 1))))
 
-(assert (not (= (set.intersection x y) (as set.empty (Set Int)))))
+(assert (not (= (set.inter x y) (as set.empty (Set Int)))))
 
 (check-sat)
diff --git a/test/regress/regress1/sets/deepmeas0.hs.fqout.cvc4.41.smt2 b/test/regress/regress1/sets/deepmeas0.hs.fqout.cvc4.41.smt2
index 7c5e09b5a..93d359b60 100644
--- a/test/regress/regress1/sets/deepmeas0.hs.fqout.cvc4.41.smt2
+++ b/test/regress/regress1/sets/deepmeas0.hs.fqout.cvc4.41.smt2
@@ -7,7 +7,7 @@
 (define-fun smt_set_mem ((x Elt) (s mySet)) Bool (set.member x s))
 (define-fun smt_set_add ((s mySet) (x Elt)) mySet (set.union s (set.singleton x)))
 (define-fun smt_set_cup ((s1 mySet) (s2 mySet)) mySet (set.union s1 s2))
-(define-fun smt_set_cap ((s1 mySet) (s2 mySet)) mySet (set.intersection s1 s2))
+(define-fun smt_set_cap ((s1 mySet) (s2 mySet)) mySet (set.inter s1 s2))
 ;(define-fun smt_set_com ((s mySet)) mySet ((_ map not) s))
 (define-fun smt_set_dif ((s1 mySet) (s2 mySet)) mySet (set.minus s1 s2))
 ;(define-fun smt_set_sub ((s1 mySet) (s2 mySet)) Bool (= smt_set_emp (smt_set_dif s1 s2)))
diff --git a/test/regress/regress1/sets/finite-type/sets-card-bool-1.smt2 b/test/regress/regress1/sets/finite-type/sets-card-bool-1.smt2
index aa5b62d09..ec82ddb8b 100644
--- a/test/regress/regress1/sets/finite-type/sets-card-bool-1.smt2
+++ b/test/regress/regress1/sets/finite-type/sets-card-bool-1.smt2
@@ -7,6 +7,6 @@
 (declare-fun universe () (Set Bool))
 (assert (= (set.card A) 2))
 (assert (= (set.card B) 2))
-(assert (= (set.intersection A B) (as set.empty (Set Bool))))
+(assert (= (set.inter A B) (as set.empty (Set Bool))))
 (assert (= universe (as set.universe (Set Bool))))
 (check-sat)
diff --git a/test/regress/regress1/sets/finite-type/sets-card-bv-2.smt2 b/test/regress/regress1/sets/finite-type/sets-card-bv-2.smt2
index 91bf1905a..0003349b3 100644
--- a/test/regress/regress1/sets/finite-type/sets-card-bv-2.smt2
+++ b/test/regress/regress1/sets/finite-type/sets-card-bv-2.smt2
@@ -8,7 +8,7 @@
 (assert (= (set.card A) 5))
 (assert (= (set.card B) 5))
 (assert (not (= A B)))
-(assert (= (set.card (set.intersection A B)) 2))
+(assert (= (set.card (set.inter A B)) 2))
 (assert (= (set.card (set.minus A B)) 3))
 (assert (= (set.card (set.minus B A)) 3))
 (assert (= universe (as set.universe (Set (_ BitVec 3)))))
diff --git a/test/regress/regress1/sets/finite-type/sets-card-bv-3.smt2 b/test/regress/regress1/sets/finite-type/sets-card-bv-3.smt2
index adbe51507..5808c4ec7 100644
--- a/test/regress/regress1/sets/finite-type/sets-card-bv-3.smt2
+++ b/test/regress/regress1/sets/finite-type/sets-card-bv-3.smt2
@@ -9,7 +9,7 @@
 (assert (= (set.card A) 3))
 (assert (= (set.card B) 3))
 (assert (not (= A B)))
-(assert (= (set.card (set.intersection A B)) 1))
+(assert (= (set.card (set.inter A B)) 1))
 (assert (= (set.card (set.minus A B)) 2))
 (assert (= (set.card (set.minus B A)) 2))
 (assert (not (set.member x A)))
diff --git a/test/regress/regress1/sets/finite-type/sets-card-bv-4.smt2 b/test/regress/regress1/sets/finite-type/sets-card-bv-4.smt2
index 2ccbc8a58..81c49e1e3 100644
--- a/test/regress/regress1/sets/finite-type/sets-card-bv-4.smt2
+++ b/test/regress/regress1/sets/finite-type/sets-card-bv-4.smt2
@@ -9,7 +9,7 @@
 (assert (= (set.card A) 5))
 (assert (= (set.card B) 5))
 (assert (not (= A B)))
-(assert (= (set.card (set.intersection A B)) 2))
+(assert (= (set.card (set.inter A B)) 2))
 (assert (= (set.card (set.minus A B)) 3))
 (assert (= (set.card (set.minus B A)) 3))
 (assert (= universe (as set.universe (Set (_ BitVec 3)))))
diff --git a/test/regress/regress1/sets/finite-type/sets-card-datatype-1.smt2 b/test/regress/regress1/sets/finite-type/sets-card-datatype-1.smt2
index 4c113c84b..62c0bc224 100644
--- a/test/regress/regress1/sets/finite-type/sets-card-datatype-1.smt2
+++ b/test/regress/regress1/sets/finite-type/sets-card-datatype-1.smt2
@@ -9,6 +9,6 @@
 (declare-fun x () Rec)
 (assert (= (set.card A) 5))
 (assert (= (set.card B) 5))
-(assert (= (set.card (set.intersection A B)) 1))
+(assert (= (set.card (set.inter A B)) 1))
 (assert (= universe (as set.universe (Set Rec))))
 (check-sat)
diff --git a/test/regress/regress1/sets/finite-type/sets-card-datatype-2.smt2 b/test/regress/regress1/sets/finite-type/sets-card-datatype-2.smt2
index 4c9bdadd5..70e3a88d8 100644
--- a/test/regress/regress1/sets/finite-type/sets-card-datatype-2.smt2
+++ b/test/regress/regress1/sets/finite-type/sets-card-datatype-2.smt2
@@ -8,6 +8,6 @@
 (declare-fun universe () (Set Rec))
 (assert (= (set.card A) 9))
 (assert (= (set.card B) 9))
-(assert (= (set.card (set.intersection A B)) 1))
+(assert (= (set.card (set.inter A B)) 1))
 (assert (= universe (as set.universe (Set Rec))))
 (check-sat)
diff --git a/test/regress/regress1/sets/fuzz14418.smt2 b/test/regress/regress1/sets/fuzz14418.smt2
index 2fb60cb72..b09cf1151 100644
--- a/test/regress/regress1/sets/fuzz14418.smt2
+++ b/test/regress/regress1/sets/fuzz14418.smt2
@@ -34,7 +34,7 @@
 (let ((e14 (set.minus v2 v2)))
 (let ((e15 (f1 v1 v4 v1)))
 (let ((e16 (f1 e14 v1 v4)))
-(let ((e17 (set.intersection e16 e15)))
+(let ((e17 (set.inter e16 e15)))
 (let ((e18 (f1 v4 e15 v2)))
 (let ((e19 (ite (p1 e13) (set.singleton 1) (set.singleton 0))))
 (let ((e20 (set.member v0 e17)))
diff --git a/test/regress/regress1/sets/fuzz15201.smt2 b/test/regress/regress1/sets/fuzz15201.smt2
index 3094a8d84..bdcbe7d59 100644
--- a/test/regress/regress1/sets/fuzz15201.smt2
+++ b/test/regress/regress1/sets/fuzz15201.smt2
@@ -29,9 +29,9 @@
 (let ((e16 (set.minus v2 v1)))
 (let ((e17 (set.minus v1 v2)))
 (let ((e18 (set.union e17 e17)))
-(let ((e19 (set.intersection e17 v1)))
-(let ((e20 (set.intersection e17 e18)))
-(let ((e21 (set.intersection v1 e16)))
+(let ((e19 (set.inter e17 v1)))
+(let ((e20 (set.inter e17 e18)))
+(let ((e21 (set.inter v1 e16)))
 (let ((e22 (set.minus e20 e16)))
 (let ((e23 (ite (p1 v2 e18 e21) (set.singleton 1) (set.singleton 0))))
 (let ((e24 (set.minus e17 e23)))
diff --git a/test/regress/regress1/sets/fuzz31811.smt2 b/test/regress/regress1/sets/fuzz31811.smt2
index e86901f9a..ca028488a 100644
--- a/test/regress/regress1/sets/fuzz31811.smt2
+++ b/test/regress/regress1/sets/fuzz31811.smt2
@@ -28,19 +28,19 @@
 (let ((e10 (f0 v0 e8 e8)))
 (let ((e11 (ite (p1 v1) (set.singleton 1) (set.singleton 0))))
 (let ((e12 (set.union v3 v3)))
-(let ((e13 (set.intersection v3 v1)))
+(let ((e13 (set.inter v3 v1)))
 (let ((e14 (ite (p1 v3) (set.singleton 1) (set.singleton 0))))
-(let ((e15 (set.intersection v2 e14)))
+(let ((e15 (set.inter v2 e14)))
 (let ((e16 (ite (p1 e11) (set.singleton 1) (set.singleton 0))))
 (let ((e17 (ite (p1 v4) (set.singleton 1) (set.singleton 0))))
 (let ((e18 (set.union e15 v2)))
 (let ((e19 (ite (p1 e16) (set.singleton 1) (set.singleton 0))))
-(let ((e20 (set.intersection e18 v3)))
+(let ((e20 (set.inter e18 v3)))
 (let ((e21 (set.minus v4 e12)))
 (let ((e22 (set.union v3 v2)))
 (let ((e23 (set.minus e12 v4)))
 (let ((e24 (set.minus v3 e16)))
-(let ((e25 (set.intersection e19 e20)))
+(let ((e25 (set.inter e19 e20)))
 (let ((e26 (ite (p1 e15) (set.singleton 1) (set.singleton 0))))
 (let ((e27 (set.minus e17 e15)))
 (let ((e28 (f1 e23 e12)))
diff --git a/test/regress/regress1/sets/infinite-type/sets-card-array-int-1.smt2 b/test/regress/regress1/sets/infinite-type/sets-card-array-int-1.smt2
index f6d032f11..57f4344c6 100644
--- a/test/regress/regress1/sets/infinite-type/sets-card-array-int-1.smt2
+++ b/test/regress/regress1/sets/infinite-type/sets-card-array-int-1.smt2
@@ -7,6 +7,6 @@
 (assert (= (set.card universe) 3))
 (assert (= (set.card A) 2))
 (assert (= (set.card B) 2))
-(assert (= (set.intersection A B) (as set.empty (Set (Array Int Int)))))
+(assert (= (set.inter A B) (as set.empty (Set (Array Int Int)))))
 (assert (= universe (as set.universe (Set (Array Int Int)))))
 (check-sat)
diff --git a/test/regress/regress1/sets/infinite-type/sets-card-array-int-2.smt2 b/test/regress/regress1/sets/infinite-type/sets-card-array-int-2.smt2
index d7e6a758c..76828576e 100644
--- a/test/regress/regress1/sets/infinite-type/sets-card-array-int-2.smt2
+++ b/test/regress/regress1/sets/infinite-type/sets-card-array-int-2.smt2
@@ -7,6 +7,6 @@
 (assert (= (set.card universe) 3))
 (assert (= (set.card A) 1))
 (assert (= (set.card B) 2))
-(assert (= (set.intersection A B) (as set.empty (Set (Array Int Int)))))
+(assert (= (set.inter A B) (as set.empty (Set (Array Int Int)))))
 (assert (= universe (as set.universe (Set (Array Int Int)))))
 (check-sat)
diff --git a/test/regress/regress1/sets/infinite-type/sets-card-int-1.smt2 b/test/regress/regress1/sets/infinite-type/sets-card-int-1.smt2
index c649c9be2..2cf5e566d 100644
--- a/test/regress/regress1/sets/infinite-type/sets-card-int-1.smt2
+++ b/test/regress/regress1/sets/infinite-type/sets-card-int-1.smt2
@@ -7,6 +7,6 @@
 (declare-const B (Set Int))
 (assert (= (set.card A) 6))
 (assert (= (set.card B) 5))
-(assert (= (set.intersection A B) (as set.empty (Set Int))))
+(assert (= (set.inter A B) (as set.empty (Set Int))))
 (assert (= universe (as set.universe (Set Int))))
 (check-sat)
diff --git a/test/regress/regress1/sets/infinite-type/sets-card-int-2.smt2 b/test/regress/regress1/sets/infinite-type/sets-card-int-2.smt2
index b3958e79e..8668b9c27 100644
--- a/test/regress/regress1/sets/infinite-type/sets-card-int-2.smt2
+++ b/test/regress/regress1/sets/infinite-type/sets-card-int-2.smt2
@@ -7,6 +7,6 @@
 (declare-const B (Set Int))
 (assert (= (set.card A) 5))
 (assert (= (set.card B) 5))
-(assert (= (set.intersection A B) (as set.empty (Set Int))))
+(assert (= (set.inter A B) (as set.empty (Set Int))))
 (assert (= universe (as set.universe (Set Int))))
 (check-sat)
diff --git a/test/regress/regress1/sets/insert_invariant_37_2.smt2 b/test/regress/regress1/sets/insert_invariant_37_2.smt2
index cac805531..a8f117062 100644
--- a/test/regress/regress1/sets/insert_invariant_37_2.smt2
+++ b/test/regress/regress1/sets/insert_invariant_37_2.smt2
@@ -723,7 +723,7 @@
 (assert (! (not (set.member null$0 Alloc$0)) :named initial_footprint_of_insert_27_11_1))
 
 (assert (! (or (= prev_2$0 curr_2$0)
-       (set.member sk_?e_1$0 (set.intersection sk_?X_4$0 sk_?X_3$0))
+       (set.member sk_?e_1$0 (set.inter sk_?X_4$0 sk_?X_3$0))
        (and (set.member sk_?e_1$0 sk_FP$0) (not (set.member sk_?e_1$0 FP$0)))
        (and (set.member sk_?e$0 (set.union c1_2$0 c2_2$0)) (not (set.member sk_?e$0 content$0)))
        (and (set.member sk_?e$0 c1_2$0)
diff --git a/test/regress/regress1/sets/issue2904.smt2 b/test/regress/regress1/sets/issue2904.smt2
index c39ea09ba..d2ffdbd7c 100644
--- a/test/regress/regress1/sets/issue2904.smt2
+++ b/test/regress/regress1/sets/issue2904.smt2
@@ -21,6 +21,6 @@
 (assert (> n (+ (* 2 f) m)))
 
 
-(assert (>= (set.card (set.minus UNIVERALSET (set.intersection (set.minus UNIVERALSET b) (set.minus UNIVERALSET c)))) n))
+(assert (>= (set.card (set.minus UNIVERALSET (set.inter (set.minus UNIVERALSET b) (set.minus UNIVERALSET c)))) n))
 
 (check-sat)
diff --git a/test/regress/regress1/sets/issue4370-2-lemma-ee-iter.smt2 b/test/regress/regress1/sets/issue4370-2-lemma-ee-iter.smt2
index fd3bd62eb..f57837d05 100644
--- a/test/regress/regress1/sets/issue4370-2-lemma-ee-iter.smt2
+++ b/test/regress/regress1/sets/issue4370-2-lemma-ee-iter.smt2
@@ -2,6 +2,6 @@
 (set-info :status unsat)
 (declare-fun st1 () (Set Int))
 (declare-fun st7 () (Set Int))
-(assert (> 0 (set.card (set.intersection st1 (set.union st7 st1)))))
+(assert (> 0 (set.card (set.inter st1 (set.union st7 st1)))))
 (assert (set.subset st1 st7))
 (check-sat)
diff --git a/test/regress/regress1/sets/issue4370-4-lemma-ee-iter.smt2 b/test/regress/regress1/sets/issue4370-4-lemma-ee-iter.smt2
index bc2f103d2..55b4ac581 100644
--- a/test/regress/regress1/sets/issue4370-4-lemma-ee-iter.smt2
+++ b/test/regress/regress1/sets/issue4370-4-lemma-ee-iter.smt2
@@ -2,7 +2,7 @@
 (set-info :status unsat)
 (declare-fun st3 () (Set String))
 (declare-fun st9 () (Set String))
-(assert (set.is_singleton (set.intersection st3 st9)))
-(assert (< 1 (set.card (set.intersection st3 st9))))
+(assert (set.is_singleton (set.inter st3 st9)))
+(assert (< 1 (set.card (set.inter st3 st9))))
 (assert (set.is_singleton st9))
 (check-sat)
diff --git a/test/regress/regress1/sets/issue4391-card-lasso.smt2 b/test/regress/regress1/sets/issue4391-card-lasso.smt2
index f7a720436..76e27f5b0 100644
--- a/test/regress/regress1/sets/issue4391-card-lasso.smt2
+++ b/test/regress/regress1/sets/issue4391-card-lasso.smt2
@@ -11,6 +11,6 @@
 (assert (= (set.card b) d))
 (assert (= (set.card c) 0))
 (assert (= 0 (mod 0 d)))
-(assert (> (set.card (set.minus e (set.intersection (set.intersection e b) (set.minus e c)))) 1))
+(assert (> (set.card (set.minus e (set.inter (set.inter e b) (set.minus e c)))) 1))
 
 (check-sat)
diff --git a/test/regress/regress1/sets/lemmabug-ListElts317minimized.smt2 b/test/regress/regress1/sets/lemmabug-ListElts317minimized.smt2
index ae71a1edb..a5ee519f5 100644
--- a/test/regress/regress1/sets/lemmabug-ListElts317minimized.smt2
+++ b/test/regress/regress1/sets/lemmabug-ListElts317minimized.smt2
@@ -27,7 +27,7 @@
 (define-fun smt_set_mem ((x Elt) (s mySet)) Bool (set.member x s))
 (define-fun smt_set_add ((s mySet) (x Elt)) mySet (set.union s (set.singleton x)))
 (define-fun smt_set_cup ((s1 mySet) (s2 mySet)) mySet (set.union s1 s2))
-(define-fun smt_set_cap ((s1 mySet) (s2 mySet)) mySet (set.intersection s1 s2))
+(define-fun smt_set_cap ((s1 mySet) (s2 mySet)) mySet (set.inter s1 s2))
 ;(define-fun smt_set_com ((s mySet)) mySet ((_ map not) s))
 (define-fun smt_set_dif ((s1 mySet) (s2 mySet)) mySet (set.minus s1 s2))
 ;(define-fun smt_set_sub ((s1 mySet) (s2 mySet)) Bool (= smt_set_emp (smt_set_dif s1 s2)))
diff --git a/test/regress/regress1/sets/remove_check_free_31_6.smt2 b/test/regress/regress1/sets/remove_check_free_31_6.smt2
index c2ff1da23..9c2bc9be7 100644
--- a/test/regress/regress1/sets/remove_check_free_31_6.smt2
+++ b/test/regress/regress1/sets/remove_check_free_31_6.smt2
@@ -230,7 +230,7 @@
 (assert (! (= sk_?X_28$0 (lseg_domain$0 next$0 curr_3$0 null$0))
    :named invariant_18_4_69))
 
-(assert (! (= (as set.empty SetLoc) (set.intersection sk_?X_27$0 sk_?X_28$0))
+(assert (! (= (as set.empty SetLoc) (set.inter sk_?X_27$0 sk_?X_28$0))
    :named invariant_18_4_70))
 
 (assert (! (= Alloc$0 (set.union FP_Caller$0 Alloc$0))
@@ -246,7 +246,7 @@
 
 (assert (! (= FP_2$0
      (set.union (set.minus FP$0 FP_1$0)
-       (set.union (set.intersection Alloc$0 FP_1$0) (set.minus Alloc$0 Alloc$0))))
+       (set.union (set.inter Alloc$0 FP_1$0) (set.minus Alloc$0 Alloc$0))))
    :named framecondition_of_remove_loop_18_4_17))
 
 (assert (! (or (Btwn$0 next$0 lst$0 curr_2$0 curr_2$0)
@@ -311,7 +311,7 @@
 
 (assert (! (= sk_?X_30$0 FP_1$0) :named invariant_18_4_74))
 
-(assert (! (= (as set.empty SetLoc) (set.intersection sk_?X_32$0 sk_?X_31$0))
+(assert (! (= (as set.empty SetLoc) (set.inter sk_?X_32$0 sk_?X_31$0))
    :named invariant_18_4_75))
 
 (assert (! (not (= curr_3$0 null$0)) :named invariant_18_4_76))
@@ -320,7 +320,7 @@
    :named invariant_18_4_77))
 
 (assert (! (= sk_?X_29$0
-     (set.union (set.intersection Alloc$0 FP_1$0) (set.minus Alloc$0 Alloc$0)))
+     (set.union (set.inter Alloc$0 FP_1$0) (set.minus Alloc$0 Alloc$0)))
    :named invariant_18_4_78))
 
 (assert (! (= sk_?X_27$0 (lseg_domain$0 next$0 lst_1$0 curr_3$0))
diff --git a/test/regress/regress1/sym/sym5.smt2 b/test/regress/regress1/sym/sym5.smt2
index cf9cbe092..16b44d115 100644
--- a/test/regress/regress1/sym/sym5.smt2
+++ b/test/regress/regress1/sym/sym5.smt2
@@ -13,6 +13,6 @@
 (assert (set.subset A (set.insert g h i (set.singleton f))))
 (assert (= C (set.minus A B) ))
 (assert (set.subset B A))
-(assert (= C (set.intersection A B)))
+(assert (= C (set.inter A B)))
 (assert (set.member j C))
 (check-sat)
diff --git a/test/regress/regress1/trim.cvc.smt2 b/test/regress/regress1/trim.cvc.smt2
index f05e08572..d823e565d 100644
--- a/test/regress/regress1/trim.cvc.smt2
+++ b/test/regress/regress1/trim.cvc.smt2
@@ -18,9 +18,9 @@
 (declare-fun ic0_c () (Set myType))
 (assert (forall ((r myType)) (=> (set.member r ic0_i) (forall ((r2 myType)) (=> (set.member r2 (neg (select d r))) (set.member r2 ic0_c))))))
 (assert (set.subset (set.singleton A) ic0_i))
-(assert (or (exists ((e0 myType)) (=> (set.member e0 ic0_i) (set.subset (select l A) (select l e0)))) (set.subset (set.intersection ic0_i ic0_c) emptymyTypeSet)))
+(assert (or (exists ((e0 myType)) (=> (set.member e0 ic0_i) (set.subset (select l A) (select l e0)))) (set.subset (set.inter ic0_i ic0_c) emptymyTypeSet)))
 (declare-fun ic1_i () (Set myType))
 (declare-fun ic1_c () (Set myType))
 (assert (forall ((r myType)) (=> (set.member r (pos (select d B))) (set.member r ic1_i))))
-(assert (or (exists ((e1 myType)) (=> (set.member e1 ic1_i) (set.subset (select l B) (select l e1)))) (set.subset (set.intersection ic1_i ic1_c) emptymyTypeSet)))
+(assert (or (exists ((e1 myType)) (=> (set.member e1 ic1_i) (set.subset (select l B) (select l e1)))) (set.subset (set.inter ic1_i ic1_c) emptymyTypeSet)))
 (check-sat)