ethereum/formal-methods

<anvacaru> @leonardoalt I've changed the Dockerfile-eldarica to use your suggested soljson file. When an assertion violation happens I get a large output which starts with

{
  auxiliaryInputRequested: {
    smtlib2queries: {
      '0x5e7df8f9c2da419124ac9c1918697f4d25bea8f5918512e44855c3ee108eb46f': '(set-logic HORN)\n' +
        '\n' +
        '(declare-datatypes ((|state_type| 0)) (((|state_type| (|balances| (Array Int Int))))))\n' +

.

I did not get any counter examples. Instead, I get a message at the end saying that there were no Horn solvers available.

    {
      component: 'general',
      errorCode: '3996',
      formattedMessage: 'Warning: CHC analysis was not possible. No Horn solver was available. None of the installed solvers was enabled.\n' +
        '\n',
      message: 'CHC analysis was not possible. No Horn solver was available. None of the installed solvers was enabled.',
      severity: 'warning',
      type: 'Warning'
    }
  ],