run_smtchecker_deposit.js

const fs = require('fs');
const path = require('path');

const solc = require('./index.js');
const smtchecker = require('./smtchecker.js');
const smtsolver = require('./smtsolver.js');
          
const settings = { modelChecker: {
  engine: 'chc',
  targets: ['assert'],
  solvers: ['smtlib2']
} };

const sources =
{
  'deposit.sol':
  {
    'urls': [ './deposit.sol' ]
  }
};

const basePath = './';

function readFileCallback(path) {
  path = basePath + '/' + path;
  if (fs.existsSync(path)) {
    try {
      return { 'contents': fs.readFileSync(path).toString('utf8') }
    } catch (e) {
      return { error: 'Error reading ' + path + ': ' + e };
    }
  } else
    return { error: 'File not found at ' + path}
}

let eldarica = smtsolver.availableSolvers[1];
eldarica.params = '-horn -abstract:off -t:1000';

const output = JSON.parse(solc.compile(
  JSON.stringify({
    language: 'Solidity',
    sources: sources,
    settings: settings
  }),
  {
    'import': readFileCallback,
    smtSolver: smtchecker.smtCallback(smtsolver.smtSolver, eldarica)
  }
));

console.log(output);