Online Help

The session:-Assert(m) command asserts the truth of expression expr within the SMTLIB session session.

Assertions made at a given stack level will be deleted when the stack is popped with SMTLIB[Session][Pop] .

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

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

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

$\mathrm{session}:-\mathrm{Assert}\left(4<x\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}$

The SMTLIB[Session][Assert] command was introduced in Maple 2022.

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