From 46ad5bddc9bc0e03ea702f29c56c22e917aeb06b Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Thu, 30 Sep 2021 10:38:44 -0500 Subject: Simplify the syntax and representation of the separation logic empty heap constraint (#7268) Since ~1 year ago, we insist that the location and data types of the separation logic heap are set upfront, analogous to the set-logic command. This means that the separation logic empty heap constraint does not need to be annotated with its types. This makes SEP_EMP a nullary Boolean operator instead of binary predicate (taking dummy arguments whose types specify the heap type). It changes the smt2 extended syntax from (_ emp T1 T2) to sep.emp. --- test/regress/regress1/sep/split-find-unsat-w-emp.smt2 | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'test/regress/regress1/sep/split-find-unsat-w-emp.smt2') diff --git a/test/regress/regress1/sep/split-find-unsat-w-emp.smt2 b/test/regress/regress1/sep/split-find-unsat-w-emp.smt2 index c6fa301f0..7935ccdc1 100644 --- a/test/regress/regress1/sep/split-find-unsat-w-emp.smt2 +++ b/test/regress/regress1/sep/split-find-unsat-w-emp.smt2 @@ -11,7 +11,7 @@ (declare-const c Int) (assert (and - (not (sep (not (pto x a)) (not (pto y b)) (not (sep (pto x a) (pto y b))) (not (_ emp Int Int)) )) + (not (sep (not (pto x a)) (not (pto y b)) (not (sep (pto x a) (pto y b))) (not sep.emp) )) (sep (pto x a) (pto y b)) ) ) -- cgit v1.2.3