Use the same z3 options as Solidity does

ethereum · Aug 17, 2020 · 972e5f6 · 972e5f6
1 parent 0cf4948
commit 972e5f6
Showing 1 changed file with 2 additions and 2 deletions.
diff --git a/smtsolver.js b/smtsolver.js
@@ -8,7 +8,7 @@ const timeout = 10000;
 var potentialSolvers = [
   {
     name: 'z3',
-    params: '-smt2 -t:' + timeout
+    params: '-smt2 rlimit=20000000 rewriter.pull_cheap_ite=true fp.spacer.q3.use_qgen=true fp.spacer.mbqi=false fp.spacer.ground_pobs=false'
   },
   {
     name: 'cvc4',
@@ -33,7 +33,7 @@ function solve (query) {
   try {
     solverOutput = execSync(
       solvers[0].name + ' ' + solvers[0].params + ' ' + tmpFile.name, {
-        timeout: 10000
+        stdio: 'pipe'
       }
     ).toString();
   } catch (e) {