The session:-Depth() command returns the current depth of the stack associated with the SMTLIB session session. The depth of the stack of a fresh session is 0.

The session:-Pop(m) command pops m levels off of the stack associated with the SMTLIB session session. The default value of m is 1.

The session:-Push() command pushes a new level onto the stack associated with the SMTLIB session session.

The session:-Reset() command clears all assertions in the SMTLIB session session and resets the stack depth to zero.

Popping the stack will delete all assertions made at the current stack level.

$\mathrm{with}\left(\mathrm{SMTLIB}\right)\:$

$\mathrm{session}≔\mathrm{Session}\left(\right)$

$\mathrm{session}≔\left[\begin{array}{c}\mathrm{SMTLIB\; Session}\\ 13904568\\ \mathrm{Variables:\; 0}\\ \mathrm{Stack\; Depth:\; 0}\end{array}\right]$

$\mathrm{session}:-\mathrm{Assert}\left(7<2x\right)::\mathrm{integer}$

$::\mathbb{Z}$

$\mathrm{session}:-\mathrm{Satisfiable}\left(\right)$

$\mathrm{true}$

$\mathrm{session}:-\mathrm{Push}\left(\right)\&colon;$

$\mathrm{session}:-\mathrm{Assert}\left(x<0\right)::\mathrm{integer}$

$::\mathbb{Z}$

$\mathrm{session}:-\mathrm{Satisfiable}\left(\right)$

$\mathrm{false}$

$\mathrm{session}:-\mathrm{Pop}\left(\right)\&colon;$

$\mathrm{session}:-\mathrm{Satisfiable}\left(\right)$

$\mathrm{true}$

The SMTLIB[Session][Depth], SMTLIB[Session][Pop], SMTLIB[Session][Push] and SMTLIB[Session][Reset] commands were introduced in Maple 2022.

For more information on Maple 2022 changes, see Updates in Maple 2022.