Generate an SMT-LIB query testing for satisfiability of this Boolean problem.
| (1) |
Generate an SMT-LIB query testing for finding a satisfying assignment to a randomly generated Boolean problem.
>
|
|
>
|
|
| (2) |
Generate an SMT-LIB query requesting a solution for the specified variables in this Diophantine problem over quantifier-free integer linear arithmetic.
>
|
|
| (3) |
Generate an SMT-LIB query requesting a proof of solvability for the preceding Diophantine problem example.
>
|
|
| (4) |
Generate an SMT-LIB query requesting an unsatisfiable core (that is, a proof of unsolvability) for the specified Boolean problem.
>
|
|
| (5) |
>
|
|
| (6) |
Generate an SMT-LIB query testing for satisfiability of this problem over quantifier-free real arithmetic, in which the types of each variable are specified explicitly (not inferred).
>
|
|
| (7) |