6 files changed, 13 insertions, 13 deletions
diff --git a/test/regress/regress0/datatypes/data-nested-codata.smt2 b/test/regress/regress0/datatypes/data-nested-codata.smt2
index 159ae4ae9..6a5716123 100644
--- a/test/regress/regress0/datatypes/data-nested-codata.smt2
+++ b/test/regress/regress0/datatypes/data-nested-codata.smt2
@@ -8,14 +8,14 @@
 
 
 (declare-fun x () Stream)
-(assert (not (is-nil (shead x))))
-(assert (not (is-nil (tail (shead x)))))
+(assert (not ((_ is nil) (shead x))))
+(assert (not ((_ is nil) (tail (shead x)))))
 (declare-fun y () Stream)
-(assert (not (is-nil (shead y))))
-(assert (not (is-nil (tail (shead y)))))
+(assert (not ((_ is nil) (shead y))))
+(assert (not ((_ is nil) (tail (shead y)))))
 (declare-fun z () Stream)
-(assert (not (is-nil (shead z))))
-(assert (not (is-nil (tail (shead z)))))
+(assert (not ((_ is nil) (shead z))))
+(assert (not ((_ is nil) (tail (shead z)))))
 (assert (distinct x y z))
 
 (check-sat)
diff --git a/test/regress/regress0/datatypes/is_test.smt2 b/test/regress/regress0/datatypes/is_test.smt2
index f13a4f21f..c54a84859 100644
--- a/test/regress/regress0/datatypes/is_test.smt2
+++ b/test/regress/regress0/datatypes/is_test.smt2
@@ -2,5 +2,5 @@
 (set-info :status unsat)
 (declare-datatypes ((Unit 0)) (((u))))
 (declare-fun x () Unit)
-(assert (not (is-u x)))
+(assert (not ((_ is u) x)))
 (check-sat)
diff --git a/test/regress/regress0/quantifiers/simp-len.smt2 b/test/regress/regress0/quantifiers/simp-len.smt2
index 0a736d7b3..06ae23f8d 100644
--- a/test/regress/regress0/quantifiers/simp-len.smt2
+++ b/test/regress/regress0/quantifiers/simp-len.smt2
@@ -3,7 +3,7 @@
 
 (declare-datatypes ((Lst 0)) (((cons (head Int) (tail Lst)) (nil))))
 
-(define-fun-rec len ((x Lst)) Int (ite (is-cons x) (+ 1 (len (tail x))) 0))
+(define-fun-rec len ((x Lst)) Int (ite ((_ is cons) x) (+ 1 (len (tail x))) 0))
 
 (assert (= (len (cons 0 nil)) 0))
 (check-sat)
diff --git a/test/regress/regress0/smtlib/global-decls.smt2 b/test/regress/regress0/smtlib/global-decls.smt2
index a8b6c17b2..4b1c8a0ae 100644
--- a/test/regress/regress0/smtlib/global-decls.smt2
+++ b/test/regress/regress0/smtlib/global-decls.smt2
@@ -16,8 +16,8 @@
 (define-fun y () (Struct1 Bool) (mk-struct1 true))
 (declare-const z Unit)
 (assert (= u u))
-(assert (is-mk-struct1 y))
-(assert (is-u z))
+(assert ((_ is mk-struct1) y))
+(assert ((_ is u) z))
 
 (declare-fun size (Tree) Int)
 (assert (= (size nil) 0))
diff --git a/test/regress/regress1/push-pop/bug-fmf-fun-skolem.smt2 b/test/regress/regress1/push-pop/bug-fmf-fun-skolem.smt2
index 229a5e17a..01a274e8a 100644
--- a/test/regress/regress1/push-pop/bug-fmf-fun-skolem.smt2
+++ b/test/regress/regress1/push-pop/bug-fmf-fun-skolem.smt2
@@ -1,7 +1,7 @@
 ; COMMAND-LINE: --incremental --fmf-fun
 (set-logic ALL_SUPPORTED)
 (declare-datatypes ((Lst 0)) (((cons (head Int) (tail Lst)) (nil))))
-(define-fun-rec sum ((l Lst)) Int (ite (is-nil l) 0 (+ (head l) (sum (tail l)))))
+(define-fun-rec sum ((l Lst)) Int (ite ((_ is nil) l) 0 (+ (head l) (sum (tail l)))))
 
 (declare-fun input () Int)
 (declare-fun p () Bool)
diff --git a/test/regress/regress2/bug674.smt2 b/test/regress/regress2/bug674.smt2
index fccde862a..31eaa5aba 100644
--- a/test/regress/regress2/bug674.smt2
+++ b/test/regress/regress2/bug674.smt2
@@ -1,8 +1,8 @@
 ; COMMAND-LINE: --quant-ind --incremental --rewrite-divk
 (set-logic ALL_SUPPORTED)
 (declare-datatypes ((Lst 0)) (((cons (head Int) (tail Lst)) (nil))))
-(define-fun-rec app ((l1 Lst) (l2 Lst)) Lst (ite (is-nil l1) l2 (cons (head l1) (app (tail l1) l2))))
-(define-fun-rec rev ((l Lst)) Lst (ite (is-nil l) nil (app (rev (tail l)) (cons (head l) nil))))
+(define-fun-rec app ((l1 Lst) (l2 Lst)) Lst (ite ((_ is nil) l1) l2 (cons (head l1) (app (tail l1) l2))))
+(define-fun-rec rev ((l Lst)) Lst (ite ((_ is nil) l) nil (app (rev (tail l)) (cons (head l) nil))))
 ; EXPECT: unsat
 (push 1)
 (assert (not (=> true (and (forall (($l1$0 Lst) ($l2$0 Lst) ($l3$0 Lst)) (= (app $l1$0 (app $l2$0 $l3$0)) (app (app $l1$0 $l2$0) $l3$0)))))))