solve
Execute Z3 Python code to solve SMT constraints and check satisfiability of logical formulas.
Instructions
Execute Z3 Python code to solve SMT constraints.
The code can use any Z3 Python API functions. Common imports (Solver, Int, Real, Bool, And, Or, Not, etc.) are pre-loaded.
Example:
x = Int('x')
y = Int('y')
solver = Solver()
solver.add(x + y == 10)
solver.add(x - y == 4)
if solver.check() == sat:
print(solver.model())Input Schema
TableJSON Schema
| Name | Required | Description | Default |
|---|---|---|---|
| code | Yes | Z3 Python code to execute | |
| timeout_ms | No | Timeout in milliseconds (default: 30000) |