Loading ToolBench
MCP server for Z3/SMT solver - enables constraint solving and logical reasoning
The Z3/SMT MCP server has 11 tools with consistent schema structure and reasonable descriptions. However, there are significant gaps in parameter documentation, missing output schema specifications, and weak error handling guidance. Tool naming is reasonably clear (solve, solve_smtlib, check_sat, prove, simplify, solve_logic_program, session_*), following verb-noun patterns. Descriptions range from 50-200 characters, mostly adequate but some lack depth about when to use each tool vs. alternatives. Input schemas are present for all tools with type definitions and required fields declared, but parameter descriptions are often terse (10-30 chars), falling below the 72-char baseline for production tools. No output schemas are documented anywhere in the source code, critical for agents to understand what fields to extract. Error handling descriptions are absent; the code mentions Z3SolverError but provides no guidance to LLMs on recovery steps.
Check satisfiability of a list of constraints. Provide constraints as Z3 Python expressions. Variables will be auto-declared based on usage. Example constraints: - "x + y == 10" - "x > 0" - "And(x < 100, y < 100)"
Attempt to prove a theorem by showing its negation is unsatisfiable. Provide the theorem as a Z3 expression. If the negation is unsatisfiable, the theorem is proven. Example: prove "ForAll([x], x + 0 == x)" for integer x
Add a constraint to the current solver session. The constraint should be a valid Z3 expression using previously declared variables.
Add a variable to the current solver session. Supported types: int, real, bool, bitvec (with bits parameter)
Check satisfiability of current session constraints and get the model if satisfiable.
Pop a context from the solver stack (backtrack).
No output schemas documented for any tool. LLMs cannot infer what fields to expect in responses, forcing them to guess at downstream field names and risk malformed requests to chained tools.
Session tools (session_add_variable, session_add_constraint, session_check, session_push, session_pop) have extremely sparse descriptions (40-50 chars). Agents cannot determine the purpose of pushing/popping, what state management looks like, or when to use sessions vs. stateless tools.
| Scored | Grade | Overall | Spec posture | Rubric |
|---|---|---|---|---|
| 2026-09-23 | D | 50 | 2026-07-28+ | v2 |
Push a new context onto the solver stack (for backtracking).
Simplify a Z3 expression. Returns the simplified form of the given expression. Example: simplify "And(x > 0, x > 0)" -> "x > 0"
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: ```python 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()) ```
Solve a structured logic program (Logic-LLM format). The program should have sections: # Declarations - EnumSort, IntSort, Function declarations # Constraints - Logical constraints Example: ``` # Declarations Color = EnumSort([red, green, blue]) assign = Function(Object -> Color) # Constraints assign(obj1) != assign(obj2) ```
Solve an SMT problem in SMT-LIB 2.0 format. Example: ``` (declare-const x Int) (declare-const y Int) (assert (= (+ x y) 10)) (assert (= (- x y) 4)) (check-sat) (get-model) ```
Parameter descriptions are consistently terse (10-30 chars). The 'variables' parameter in check_sat, prove, and simplify lacks clear documentation of the format 'int', 'real', 'bool', 'bitvec:N'. Agents may pass invalid variable declarations.
No error handling guidance. Code references Z3SolverError but provides no recovery hints. When a constraint is unsatisfiable or a timeout occurs, the agent has no guidance on what to try next (simplify? add bounds? retry with longer timeout?).
The 'variables' parameter in check_sat, prove, simplify, and session_add_variable is documented as a free-form object with no enum or format constraint. Agents may pass malformed type declarations like 'var_type: int64' or 'var_type: unsigned' that Z3 does not support.
The 'var_type' enum in session_add_variable is well-constrained (int, real, bool, bitvec), but the 'bits' parameter for bitvec has no minimum/maximum bounds. Agents may request unreasonably large bitvectors (bits: 10000) causing memory exhaustion.
Tool composition gap: no batch variants. If an agent needs to add 50 constraints, it must make 50 session_add_constraint calls sequentially, wasting tokens and latency. A single add_constraints (plural) with array input would be more efficient.
Stateful session management (via global _sessions dict) is at odds with typical MCP usage. Agents expect tools to be independent and composable. No guidance on session lifecycle, cleanup, or isolation between agents.