Create a a SMTLIB session object for solving over quantifier-free integer linear arithmetic.
>
|
|
| (1) |
Assert this Diophantine problem.
>
|
|
Push the stack and add a side assumption. The problem becomes unsatisfiable.
Pop the stack and verify the problem is once again satisfiable.