Merge branch 'master' into refactorEagerSolverrefactorEagerSolver

11 files changed, 14 insertions, 14 deletions

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)