rename subseteq to subset in smtlib, all kinds and smt operator names are now consistent

12 files changed, 13 insertions, 13 deletions

diff --git a/test/regress/regress0/sets/feb3/ListElts.hs.fqout.cvc4.317.smt2 b/test/regress/regress0/sets/feb3/ListElts.hs.fqout.cvc4.317.smt2
index 87cb9b73d..7b5294aec 100644
--- a/test/regress/regress0/sets/feb3/ListElts.hs.fqout.cvc4.317.smt2
+++ b/test/regress/regress0/sets/feb3/ListElts.hs.fqout.cvc4.317.smt2
@@ -11,7 +11,7 @@
 ;(define-fun smt_set_com ((s mySet)) mySet ((_ map not) s))
 (define-fun smt_set_dif ((s1 mySet) (s2 mySet)) mySet (setminus s1 s2))
 ;(define-fun smt_set_sub ((s1 mySet) (s2 mySet)) Bool (= smt_set_emp (smt_set_dif s1 s2)))
-(define-fun smt_set_sub ((s1 mySet) (s2 mySet)) Bool (subseteq s1 s2))
+(define-fun smt_set_sub ((s1 mySet) (s2 mySet)) Bool (subset s1 s2))
 (declare-fun z3v58 () Int)
 (declare-fun z3v59 () Int)
 (assert (distinct z3v58 z3v59))
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 bc919673d..71bb8a3e6 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
@@ -10,7 +10,7 @@
 
 (define-fun smt_set_dif ((s1 mySet) (s2 mySet)) mySet (setminus s1 s2))
 
-(define-fun smt_set_sub ((s1 mySet) (s2 mySet)) Bool (subseteq s1 s2))
+(define-fun smt_set_sub ((s1 mySet) (s2 mySet)) Bool (subset s1 s2))
 (declare-fun z3v58 () Int)
 (declare-fun z3v59 () Int)
 (assert (distinct z3v58 z3v59))
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 f055a8e1c..eb48b023a 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
@@ -10,7 +10,7 @@
 ;(define-fun smt_set_com ((s mySet)) mySet ((_ map not) s))
 (define-fun smt_set_dif ((s1 mySet) (s2 mySet)) mySet (setminus s1 s2))
 ;(define-fun smt_set_sub ((s1 mySet) (s2 mySet)) Bool (= smt_set_emp (smt_set_dif s1 s2)))
-(define-fun smt_set_sub ((s1 mySet) (s2 mySet)) Bool (subseteq s1 s2))
+(define-fun smt_set_sub ((s1 mySet) (s2 mySet)) Bool (subset s1 s2))
 (declare-fun z3v54 () Int)
 (declare-fun z3f55 (Int) Int)
 (declare-fun z3v56 () Int)
diff --git a/test/regress/regress0/sets/jan27/ListElem.hs.fqout.cvc4.38.smt2 b/test/regress/regress0/sets/jan27/ListElem.hs.fqout.cvc4.38.smt2
index 81b8794e5..3c0ef1dda 100644
--- a/test/regress/regress0/sets/jan27/ListElem.hs.fqout.cvc4.38.smt2
+++ b/test/regress/regress0/sets/jan27/ListElem.hs.fqout.cvc4.38.smt2
@@ -16,7 +16,7 @@
 ;(define-fun smt_set_com ((s mySet)) mySet ((_ map not) s))
 (define-fun smt_set_dif ((s1 mySet) (s2 mySet)) mySet (setminus s1 s2))
 ;(define-fun smt_set_sub ((s1 mySet) (s2 mySet)) Bool (= smt_set_emp (smt_set_dif s1 s2)))
-(define-fun smt_set_sub ((s1 mySet) (s2 mySet)) Bool (subseteq s1 s2))
+(define-fun smt_set_sub ((s1 mySet) (s2 mySet)) Bool (subset s1 s2))
 (declare-fun z3v56 () Int)
 (declare-fun z3v57 () Int)
 (assert (distinct z3v56 z3v57))
diff --git a/test/regress/regress0/sets/jan27/deepmeas0.hs.fqout.cvc4.41.smt2 b/test/regress/regress0/sets/jan27/deepmeas0.hs.fqout.cvc4.41.smt2
index 8b84c9153..83dfe41e5 100644
--- a/test/regress/regress0/sets/jan27/deepmeas0.hs.fqout.cvc4.41.smt2
+++ b/test/regress/regress0/sets/jan27/deepmeas0.hs.fqout.cvc4.41.smt2
@@ -11,7 +11,7 @@
 ;(define-fun smt_set_com ((s mySet)) mySet ((_ map not) s))
 (define-fun smt_set_dif ((s1 mySet) (s2 mySet)) mySet (setminus s1 s2))
 ;(define-fun smt_set_sub ((s1 mySet) (s2 mySet)) Bool (= smt_set_emp (smt_set_dif s1 s2)))
-(define-fun smt_set_sub ((s1 mySet) (s2 mySet)) Bool (subseteq s1 s2))
+(define-fun smt_set_sub ((s1 mySet) (s2 mySet)) Bool (subset s1 s2))
 (declare-fun z3v58 () Int)
 (declare-fun z3v59 () Int)
 (assert (distinct z3v58 z3v59))
diff --git a/test/regress/regress0/sets/jan28/TalkingAboutSets.hs.fqout.cvc4.3577.smt2 b/test/regress/regress0/sets/jan28/TalkingAboutSets.hs.fqout.cvc4.3577.smt2
index ac5fdf48d..282325f14 100644
--- a/test/regress/regress0/sets/jan28/TalkingAboutSets.hs.fqout.cvc4.3577.smt2
+++ b/test/regress/regress0/sets/jan28/TalkingAboutSets.hs.fqout.cvc4.3577.smt2
@@ -11,7 +11,7 @@
 ;(define-fun smt_set_com ((s mySet)) mySet ((_ map not) s))
 (define-fun smt_set_dif ((s1 mySet) (s2 mySet)) mySet (setminus s1 s2))
 ;(define-fun smt_set_sub ((s1 mySet) (s2 mySet)) Bool (= smt_set_emp (smt_set_dif s1 s2)))
-(define-fun smt_set_sub ((s1 mySet) (s2 mySet)) Bool (subseteq s1 s2))
+(define-fun smt_set_sub ((s1 mySet) (s2 mySet)) Bool (subset s1 s2))
 (declare-fun z3v60 () Int)
 (declare-fun z3v61 () Int)
 (assert (distinct z3v60 z3v61))
diff --git a/test/regress/regress0/sets/jan30/UniqueZipper.hs.fqout.cvc4.10.smt2 b/test/regress/regress0/sets/jan30/UniqueZipper.hs.fqout.cvc4.10.smt2
index e17911327..10ed4be7c 100644
--- a/test/regress/regress0/sets/jan30/UniqueZipper.hs.fqout.cvc4.10.smt2
+++ b/test/regress/regress0/sets/jan30/UniqueZipper.hs.fqout.cvc4.10.smt2
@@ -8,7 +8,7 @@
 (define-fun smt_set_cup ((s1 mySet) (s2 mySet)) mySet (union s1 s2))
 (define-fun smt_set_cap ((s1 mySet) (s2 mySet)) mySet (intersection s1 s2))
 (define-fun smt_set_dif ((s1 mySet) (s2 mySet)) mySet (setminus s1 s2))
-(define-fun smt_set_sub ((s1 mySet) (s2 mySet)) Bool (subseteq s1 s2))
+(define-fun smt_set_sub ((s1 mySet) (s2 mySet)) Bool (subset s1 s2))
 (declare-fun z3v66 () Int)
 (declare-fun z3v67 () Int)
 (assert (distinct z3v66 z3v67))
diff --git a/test/regress/regress0/sets/jan30/UniqueZipper.hs.fqout.cvc4.1832.smt2 b/test/regress/regress0/sets/jan30/UniqueZipper.hs.fqout.cvc4.1832.smt2
index bea016683..6165b98de 100644
--- a/test/regress/regress0/sets/jan30/UniqueZipper.hs.fqout.cvc4.1832.smt2
+++ b/test/regress/regress0/sets/jan30/UniqueZipper.hs.fqout.cvc4.1832.smt2
@@ -10,7 +10,7 @@
 ;(define-fun smt_set_com ((s mySet)) mySet ((_ map not) s))
 (define-fun smt_set_dif ((s1 mySet) (s2 mySet)) mySet (setminus s1 s2))
 ;(define-fun smt_set_sub ((s1 mySet) (s2 mySet)) Bool (= smt_set_emp (smt_set_dif s1 s2)))
-(define-fun smt_set_sub ((s1 mySet) (s2 mySet)) Bool (subseteq s1 s2))
+(define-fun smt_set_sub ((s1 mySet) (s2 mySet)) Bool (subset s1 s2))
 (declare-fun z3v66 () Int)
 (declare-fun z3v67 () Int)
 (assert (distinct z3v66 z3v67))
diff --git a/test/regress/regress0/sets/mar2014/UniqueZipper.hs.1030minimized.cvc4.smt2 b/test/regress/regress0/sets/mar2014/UniqueZipper.hs.1030minimized.cvc4.smt2
index 9175a8723..38477c46a 100644
--- a/test/regress/regress0/sets/mar2014/UniqueZipper.hs.1030minimized.cvc4.smt2
+++ b/test/regress/regress0/sets/mar2014/UniqueZipper.hs.1030minimized.cvc4.smt2
@@ -8,7 +8,7 @@
 (define-fun smt_set_cup ((s1 mySet) (s2 mySet)) mySet (union s1 s2))
 (define-fun smt_set_cap ((s1 mySet) (s2 mySet)) mySet (intersection s1 s2))
 (define-fun smt_set_dif ((s1 mySet) (s2 mySet)) mySet (setminus s1 s2))
-(define-fun smt_set_sub ((s1 mySet) (s2 mySet)) Bool (subseteq s1 s2))
+(define-fun smt_set_sub ((s1 mySet) (s2 mySet)) Bool (subset s1 s2))
 
 (declare-fun z3v66 () Int)
 (declare-fun z3v67 () Int)
diff --git a/test/regress/regress0/sets/mar2014/UniqueZipper.hs.1030minimized2.cvc4.smt2 b/test/regress/regress0/sets/mar2014/UniqueZipper.hs.1030minimized2.cvc4.smt2
index 81117134c..e282e446e 100644
--- a/test/regress/regress0/sets/mar2014/UniqueZipper.hs.1030minimized2.cvc4.smt2
+++ b/test/regress/regress0/sets/mar2014/UniqueZipper.hs.1030minimized2.cvc4.smt2
@@ -8,7 +8,7 @@
 (define-fun smt_set_cup ((s1 mySet) (s2 mySet)) mySet (union s1 s2))
 (define-fun smt_set_cap ((s1 mySet) (s2 mySet)) mySet (intersection s1 s2))
 (define-fun smt_set_dif ((s1 mySet) (s2 mySet)) mySet (setminus s1 s2))
-(define-fun smt_set_sub ((s1 mySet) (s2 mySet)) Bool (subseteq s1 s2))
+(define-fun smt_set_sub ((s1 mySet) (s2 mySet)) Bool (subset s1 s2))
 
 (declare-fun z3f70 (Int) mySet)
 (declare-fun z3f72 (Int) mySet)
@@ -177,7 +177,7 @@
                         (z3f70 z3v270))))
 (assert (= z3v242 (z3f77 z3v271 z3v270)))
 (assert (= z3v242 z3v243))
-(assert (subseteq (z3f70 z3v242)
+(assert (subset (z3f70 z3v242)
                   (z3f70 z3v244)))
 (assert (= (z3f72 z3v243) smt_set_emp))
 (assert (= (z3f72 z3v244)
diff --git a/test/regress/regress0/sets/mar2014/lemmabug-ListElts317minimized.smt2 b/test/regress/regress0/sets/mar2014/lemmabug-ListElts317minimized.smt2
index 1e848695d..0fc8ca067 100644
--- a/test/regress/regress0/sets/mar2014/lemmabug-ListElts317minimized.smt2
+++ b/test/regress/regress0/sets/mar2014/lemmabug-ListElts317minimized.smt2
@@ -31,7 +31,7 @@
 ;(define-fun smt_set_com ((s mySet)) mySet ((_ map not) s))
 (define-fun smt_set_dif ((s1 mySet) (s2 mySet)) mySet (setminus s1 s2))
 ;(define-fun smt_set_sub ((s1 mySet) (s2 mySet)) Bool (= smt_set_emp (smt_set_dif s1 s2)))
-(define-fun smt_set_sub ((s1 mySet) (s2 mySet)) Bool (subseteq s1 s2))
+(define-fun smt_set_sub ((s1 mySet) (s2 mySet)) Bool (subset s1 s2))
 
 (declare-fun z3v58 () Int)
 (declare-fun z3v59 () Int)
diff --git a/test/regress/regress0/sets/sets-sample.smt2 b/test/regress/regress0/sets/sets-sample.smt2
index 4838c6cf2..a040b0bec 100644
--- a/test/regress/regress0/sets/sets-sample.smt2
+++ b/test/regress/regress0/sets/sets-sample.smt2
@@ -16,7 +16,7 @@
 (assert (= c (union a b) ))
 (assert (not (= c (intersection a b) )))
 (assert (= c (setminus a b) ))
-(assert (subseteq a b))
+(assert (subset a b))
 (assert (member e c))
 (assert (member e a))
 (assert (member e (intersection a b)))