Skip to content

Commit abb4d8a

Browse files
author
Leonardo
authored
Merge pull request #396 from ethereum/cvc4_timeout
Add timeout for SMT solvers
2 parents b238a52 + a8e6c3c commit abb4d8a

File tree

1 file changed

+4
-2
lines changed

1 file changed

+4
-2
lines changed

smtsolver.js

Lines changed: 4 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -3,14 +3,16 @@ var execSync = require('child_process').execSync;
33
var fs = require('fs');
44
var tmp = require('tmp');
55

6+
const timeout = 10000;
7+
68
var potentialSolvers = [
79
{
810
name: 'z3',
9-
params: '-smt2'
11+
params: '-smt2 -t:' + timeout
1012
},
1113
{
1214
name: 'cvc4',
13-
params: '--lang=smt2'
15+
params: '--lang=smt2 --tlimit=' + timeout
1416
}
1517
];
1618
var solvers = potentialSolvers.filter(solver => commandExistsSync(solver.name));

0 commit comments

Comments
 (0)