0
# SMT Integration
1

2
Integration with external SMT solvers for formal verification through Solidity's SMTChecker with support for Z3, Eldarica, and cvc5.
3

4
## Capabilities
5

6
### SMT Callback Creation
7

8
Create callback functions for SMT solver integration during compilation.
9

10
```typescript { .api }
11
/**
12
 * Create SMT solver callback for compilation
13
 * @param solverFunction - Function that takes SMT queries and returns solutions
14
 * @param solver - Optional solver configuration object
15
 * @returns Callback function compatible with compile() method
16
 */
17
function smtCallback(
18
  solverFunction: (query: string, solver?: any) => string,
19
  solver?: any
20
): (query: string) => { contents: string } | { error: string };
21
```
22

23
**Usage Examples:**
24

25
```typescript
26
import solc from "solc";
27
import smtchecker from "solc/smtchecker";
28
import smtsolver from "solc/smtsolver";
29

30
const input = {
31
  language: 'Solidity',
32
  sources: {
33
    'test.sol': {
34
      content: 'contract C { function f(uint x) public { assert(x > 0); } }'
35
    }
36
  },
37
  settings: {
38
    modelChecker: {
39
      engine: "chc",
40
      solvers: ["smtlib2"]
41
    }
42
  }
43
};
44

45
// Create SMT callback
46
const callback = smtchecker.smtCallback(
47
  smtsolver.smtSolver,
48
  smtsolver.availableSolvers[0]
49
);
50

51
// Compile with SMT verification
52
const output = JSON.parse(
53
  solc.compile(JSON.stringify(input), { smtSolver: callback })
54
);
55
```
56

57
### SMT Query Handling
58

59
Process SMT queries from compiler output and provide solutions for re-compilation.
60

61
```typescript { .api }
62
/**
63
 * Handle SMT queries from compiler output
64
 * @param inputJSON - Original Standard JSON input object
65
 * @param outputJSON - Standard JSON output containing SMT queries
66
 * @param solverFunction - Function to solve individual SMT queries
67
 * @param solver - Optional solver configuration
68
 * @returns Modified input JSON with SMT responses, or null if no queries
69
 */
70
function handleSMTQueries(
71
  inputJSON: any,
72
  outputJSON: any,
73
  solverFunction: (query: string, solver?: any) => string,
74
  solver?: any
75
): any | null;
76
```
77

78
**Usage Examples:**
79

80
```typescript
81
import smtchecker from "solc/smtchecker";
82
import smtsolver from "solc/smtsolver";
83

84
// First compilation to get SMT queries
85
const input = { /* standard JSON input with modelChecker settings */ };
86
const firstOutput = JSON.parse(solc.compile(JSON.stringify(input)));
87

88
// Process SMT queries if present
89
const modifiedInput = smtchecker.handleSMTQueries(
90
  input,
91
  firstOutput,
92
  smtsolver.smtSolver,
93
  smtsolver.availableSolvers[0]
94
);
95

96
if (modifiedInput) {
97
  // Re-compile with SMT solutions
98
  const finalOutput = JSON.parse(solc.compile(JSON.stringify(modifiedInput)));
99
  console.log('SMT verification results:', finalOutput.errors);
100
} else {
101
  console.log('No SMT queries to process');
102
}
103
```
104

105
### SMT Solver Management
106

107
Direct SMT solver integration with support for multiple solver backends.
108

109
```typescript { .api }
110
/**
111
 * Solve an individual SMT query using available solvers
112
 * @param query - SMT-LIB2 formatted query string
113
 * @param solver - Optional solver configuration (uses first available if not specified)
114
 * @returns Solver output string (sat/unsat/unknown with optional model)
115
 */
116
function smtSolver(query: string, solver?: SolverConfig): string;
117

118
interface SolverConfig {
119
  name: string;
120
  command: string;
121
  params: string;
122
}
123

124
/** Array of locally available SMT solvers detected at runtime */
125
const availableSolvers: SolverConfig[];
126
```
127

128
**Available Solvers:**
129

130
The package supports three SMT solvers if they are installed locally:
131

132
- **Z3**: Microsoft Research SMT solver
133
  - Command: `z3`
134
  - Default parameters: `-smt2 rlimit=20000000 rewriter.pull_cheap_ite=true fp.spacer.q3.use_qgen=true fp.spacer.mbqi=false fp.spacer.ground_pobs=false`
135

136
- **Eldarica**: Horn clause solver  
137
  - Command: `eld`
138
  - Default parameters: `-horn -t:10` (10 second timeout)
139

140
- **cvc5**: SMT solver from Stanford
141
  - Command: `cvc5`
142
  - Default parameters: `--lang=smt2 --tlimit=10000`
143

144
**Usage Examples:**
145

146
```typescript
147
import smtsolver from "solc/smtsolver";
148

149
// Check available solvers
150
console.log('Available solvers:', smtsolver.availableSolvers);
151

152
if (smtsolver.availableSolvers.length === 0) {
153
  console.log('No SMT solvers found. Install Z3, Eldarica, or cvc5.');
154
} else {
155
  // Use first available solver
156
  const query = `(set-logic QF_LIA)
157
(declare-fun x () Int)
158
(assert (> x 0))
159
(check-sat)
160
(get-model)`;
161

162
  try {
163
    const result = smtsolver.smtSolver(query);
164
    console.log('Solver result:', result); // "sat" or "unsat" etc.
165
  } catch (error) {
166
    console.error('Solver error:', error.message);
167
  }
168
}
169
```
170

171
### Model Checker Configuration
172

173
Configure the Solidity model checker for different verification approaches.
174

175
```typescript { .api }
176
interface ModelCheckerSettings {
177
  /** Verification engine to use */
178
  engine: "chc" | "bmc";
179
  /** SMT solvers to use (defaults to ["smtlib2"]) */
180
  solvers?: string[];
181
  /** Timeout in milliseconds */
182
  timeout?: number;
183
  /** Verification targets */
184
  targets?: ("assert" | "underflow" | "overflow" | "divByZero" | "constantCondition" | "popEmptyArray" | "outOfBounds")[];
185
}
186
```
187

188
**Usage Examples:**
189

190
```typescript
191
// Basic assertion checking
192
const basicConfig = {
193
  language: 'Solidity',
194
  sources: { /* ... */ },
195
  settings: {
196
    modelChecker: {
197
      engine: "chc",
198
      solvers: ["smtlib2"]
199
    }
200
  }
201
};
202

203
// Advanced configuration
204
const advancedConfig = {
205
  language: 'Solidity',
206
  sources: { /* ... */ },
207
  settings: {
208
    modelChecker: {
209
      engine: "bmc",
210
      solvers: ["smtlib2"],
211
      timeout: 30000,
212
      targets: ["assert", "overflow", "underflow"]
213
    }
214
  }
215
};
216
```
217

218
### Error Handling and Timeouts
219

220
SMT solvers may timeout or encounter errors. The integration handles these cases gracefully:
221

222
```typescript
223
import smtsolver from "solc/smtsolver";
224

225
try {
226
  const result = smtsolver.smtSolver(complexQuery);
227
  
228
  if (result.startsWith('sat')) {
229
    console.log('Query is satisfiable');
230
  } else if (result.startsWith('unsat')) {
231
    console.log('Query is unsatisfiable');
232
  } else if (result.startsWith('unknown')) {
233
    console.log('Solver could not determine satisfiability');
234
  }
235
} catch (error) {
236
  console.error('SMT solver failed:', error.message);
237
  // Continue without SMT verification
238
}
239
```
240

241
### Verification Workflow
242

243
Complete workflow for SMT-based formal verification:
244

245
```typescript
246
import solc from "solc";
247
import smtchecker from "solc/smtchecker";
248
import smtsolver from "solc/smtsolver";
249

250
async function verifyContract(sourceCode: string) {
251
  const input = {
252
    language: 'Solidity',
253
    sources: {
254
      'contract.sol': { content: sourceCode }
255
    },
256
    settings: {
257
      modelChecker: {
258
        engine: "chc",
259
        solvers: ["smtlib2"]
260
      },
261
      outputSelection: {
262
        '*': { '*': ['*'] }
263
      }
264
    }
265
  };
266

267
  try {
268
    // First compilation
269
    const output = JSON.parse(solc.compile(JSON.stringify(input)));
270
    
271
    if (smtsolver.availableSolvers.length === 0) {
272
      console.log('No SMT solvers available - skipping verification');
273
      return output;
274
    }
275

276
    // Handle SMT queries
277
    const modifiedInput = smtchecker.handleSMTQueries(
278
      input,
279
      output,
280
      smtsolver.smtSolver,
281
      smtsolver.availableSolvers[0]
282
    );
283

284
    if (modifiedInput) {
285
      console.log('Re-running compilation with SMT solutions...');
286
      const finalOutput = JSON.parse(solc.compile(JSON.stringify(modifiedInput)));
287
      return finalOutput;
288
    }
289

290
    return output;
291
    
292
  } catch (error) {
293
    console.error('Verification failed:', error);
294
    throw error;
295
  }
296
}
297

298
// Usage
299
const contractCode = `
300
contract SafeMath {
301
  function add(uint a, uint b) public pure returns (uint) {
302
    uint c = a + b;
303
    assert(c >= a); // This assertion will be verified
304
    return c;
305
  }
306
}`;
307

308
verifyContract(contractCode).then(result => {
309
  const errors = result.errors || [];
310
  const warnings = errors.filter(e => e.severity === 'warning');
311
  const errorMessages = errors.filter(e => e.severity === 'error');
312
  
313
  console.log(`Verification complete: ${errorMessages.length} errors, ${warnings.length} warnings`);
314
});
315
```