8 files changed, 10 insertions, 10 deletions
diff --git a/test/regress/regress0/sep/dispose-1.smt2 b/test/regress/regress0/sep/dispose-1.smt2
index 45dd29459..5191ecd5b 100644
--- a/test/regress/regress0/sep/dispose-1.smt2
+++ b/test/regress/regress0/sep/dispose-1.smt2
@@ -13,7 +13,7 @@
 ;-----------------
 
 (assert (pto w (as sep.nil Int)))
-(assert (not (and (sep (and (_ emp Int Int) (= w2 (as sep.nil Int))) (pto w w1)) (sep (pto w w2) true))))
+(assert (not (and (sep (and sep.emp (= w2 (as sep.nil Int))) (pto w w1)) (sep (pto w w2) true))))
 
 (check-sat)
 ;(get-model)
diff --git a/test/regress/regress0/sep/dup-nemp.smt2 b/test/regress/regress0/sep/dup-nemp.smt2
index 5682a0a02..3f792a4fb 100644
--- a/test/regress/regress0/sep/dup-nemp.smt2
+++ b/test/regress/regress0/sep/dup-nemp.smt2
@@ -3,6 +3,6 @@
 (declare-sort Loc 0)
 (declare-const l Loc)
 (declare-heap (Loc Loc))
-(assert (sep (not (_ emp Loc Loc)) (not (_ emp Loc Loc))))
+(assert (sep (not sep.emp) (not sep.emp)))
 (assert (pto l l))
 (check-sat)
diff --git a/test/regress/regress0/sep/issue3720-check-model.smt2 b/test/regress/regress0/sep/issue3720-check-model.smt2
index 7e9c73cb8..488c558b0 100644
--- a/test/regress/regress0/sep/issue3720-check-model.smt2
+++ b/test/regress/regress0/sep/issue3720-check-model.smt2
@@ -1,6 +1,6 @@
-; COMMAND-LINE: --quiet
+; COMMAND-LINE: --no-check-models
 ; EXPECT: sat
 (set-logic ALL)
 (declare-heap (Int Int))
-(assert (_ emp Int Int))
+(assert sep.emp)
 (check-sat)
diff --git a/test/regress/regress0/sep/nemp.smt2 b/test/regress/regress0/sep/nemp.smt2
index 583457e48..2d35a43d8 100644
--- a/test/regress/regress0/sep/nemp.smt2
+++ b/test/regress/regress0/sep/nemp.smt2
@@ -2,5 +2,5 @@
 ; EXPECT: sat
 (set-logic QF_SEP_LIA)
 (declare-heap (Int Int))
-(assert (not (_ emp Int Int)))
+(assert (not sep.emp))
 (check-sat)
diff --git a/test/regress/regress0/sep/sep-simp-unsat-emp.smt2 b/test/regress/regress0/sep/sep-simp-unsat-emp.smt2
index 312c97542..c83e98b66 100644
--- a/test/regress/regress0/sep/sep-simp-unsat-emp.smt2
+++ b/test/regress/regress0/sep/sep-simp-unsat-emp.smt2
@@ -8,6 +8,6 @@
 (declare-fun a () U)
 (declare-fun b () U)
 
-(assert (_ emp U U))
+(assert sep.emp)
 (assert (sep (pto x a) (pto y b)))
 (check-sat)
diff --git a/test/regress/regress0/sep/skolem_emp.smt2 b/test/regress/regress0/sep/skolem_emp.smt2
index 2a836bef9..1c690cc75 100644
--- a/test/regress/regress0/sep/skolem_emp.smt2
+++ b/test/regress/regress0/sep/skolem_emp.smt2
@@ -2,5 +2,5 @@
 ; EXPECT: sat
 (set-logic QF_ALL)
 (declare-heap (Int Int))
-(assert (not (_ emp Int Int)))
+(assert (not sep.emp))
 (check-sat)
diff --git a/test/regress/regress0/sep/trees-1.smt2 b/test/regress/regress0/sep/trees-1.smt2
index 2c742c60f..31c85d62d 100644
--- a/test/regress/regress0/sep/trees-1.smt2
+++ b/test/regress/regress0/sep/trees-1.smt2
@@ -18,7 +18,7 @@
 (declare-const r Loc)
 
 (define-fun ten-tree0 ((x Loc) (d Int)) Bool 
-(or (and (_ emp Loc Node) (= x (as sep.nil Loc))) (and (sep (pto x (node d l r)) (and (_ emp Loc Node) (= l (as sep.nil Loc))) (and (_ emp Loc Node) (= r (as sep.nil Loc)))) (= dl (- d 10)) (= dr (+ d 10)))))
+(or (and sep.emp (= x (as sep.nil Loc))) (and (sep (pto x (node d l r)) (and sep.emp (= l (as sep.nil Loc))) (and sep.emp (= r (as sep.nil Loc)))) (= dl (- d 10)) (= dr (+ d 10)))))
 
 (declare-const dy Int)
 (declare-const y Loc)
@@ -26,7 +26,7 @@
 (declare-const z Loc)
 
 (define-fun ord-tree0 ((x Loc) (d Int)) Bool 
-(or (and (_ emp Loc Node) (= x (as sep.nil Loc))) (and (sep (pto x (node d y z)) (and (_ emp Loc Node) (= y (as sep.nil Loc))) (and (_ emp Loc Node) (= z (as sep.nil Loc)))) (<= dy d) (<= d dz))))
+(or (and sep.emp (= x (as sep.nil Loc))) (and (sep (pto x (node d y z)) (and sep.emp (= y (as sep.nil Loc))) (and sep.emp (= z (as sep.nil Loc)))) (<= dy d) (<= d dz))))
 
 ;------- f -------
 (assert (= y (as sep.nil Loc)))
diff --git a/test/regress/regress0/sep/wand-crash.smt2 b/test/regress/regress0/sep/wand-crash.smt2
index 02511bbae..d84d900f3 100644
--- a/test/regress/regress0/sep/wand-crash.smt2
+++ b/test/regress/regress0/sep/wand-crash.smt2
@@ -2,5 +2,5 @@
 ; EXPECT: sat
 (set-logic QF_ALL)
 (declare-heap (Int Int))
-(assert (wand (_ emp Int Int) (_ emp Int Int)))
+(assert (wand sep.emp sep.emp))
 (check-sat)