diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-09-30 10:38:44 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-09-30 15:38:44 +0000 |
| commit | 46ad5bddc9bc0e03ea702f29c56c22e917aeb06b (patch) | |
| tree | f5401a4a35643d25b6e3c43403018cf57ec5c0b4 /test/regress/regress1/sep/split-find-unsat-w-emp.smt2 | |
| parent | 0a15133a7de2289fdfb10ccf65e9b753f5064ba7 (diff) | |
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.
Diffstat (limited to 'test/regress/regress1/sep/split-find-unsat-w-emp.smt2')
| -rw-r--r-- | test/regress/regress1/sep/split-find-unsat-w-emp.smt2 | 2 |
1 files changed, 1 insertions, 1 deletions
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)) ) ) |