Inconsistent test results in a simple contract (2)

[ggrieco-tob]

In this simple contract:

contract A {}

contract B {
  function f() {
    return;
  }
}
 
contract TEST {

  A[] private xs;
  B b = new B(); 
 
  function g() public {
    return;
  }

  //function add() {
  //  xs.push(new A());
  //}

  function echidna_true() returns (bool) {
    b.f();
    return true;
  }
}

the echidna_true test cannot fail and Echida works as expected. However it reports a failed test when you uncomment the add() function. For instance:

$ echidna-test test.sol test.sol:TEST
━━━ test.sol ━━━
  ✗ "echidna_true" failed after 2 tests.
  
    │ Call sequence: add();
  
  ✗ 1 failed.

[blperez01]

Weird aspect of this bug, the following function fails:

  function echidna_true() returns (bool) {
    xs.push(new A());
    b.f();
    return true;
  }

But switching the order of the push and call to f() works

  function echidna_true() returns (bool) {
    b.f();
    xs.push(new A());
    return true;
  }

(this is all assuming the add function is commented out)

[ggrieco-tob]

A simplified version of this example:

contract B {
  int x;
  function f() returns (int) {
    return x;
  }
}

contract TEST {

  B b = new B();

  function g() public {
    return;
  }

  function echidna_true() returns (bool) {
    var x = b.f();
    return true;
  }
}

[ggrieco-tob]

Using the last release of hevm (available in branch updated-hevm) solves this issue!

[ggrieco-tob]

@andremarianiello created PR #141 to migrate to hevm-0.21 using stack. It should solve this issue.

[ggrieco-tob]

Not longer failing in master, since we are using hevm-0.21.