Crashing exploration

[hjorthjort]

Crashing backend on KontrolTest.testFailQuadratic, bug report TAR here: https://s3.bithex-topnym.startram.io/bucket/2023.10.13..12.22.01-FailQuadratic.tar

The test (in Solidity):

// SPDX-License-Identifier: UNLICENSED
pragma solidity >=0.6.2 <0.9.0;

import {Test} from "forge-std/Test.sol";
import "forge-std/Vm.sol";

contract KontrolTest is Test {

  function testFailOneRange(uint256 x) public {
    assertTrue(x > 1000);
    assertGt(5000, x);
  }

  function testFailLinear(uint256 x) public {
    Func f = new Func();
    uint256 res = f.linear(x);
    assertGt(res, 5000);
  }

  function testFailQuadratic(uint256 x) public {
    Func f = new Func();
    uint256 res = f.quadratic(x);
    assertGt(res, 5000);
  }

}

contract Func {

  function linear(uint256 x) public returns (uint256) {
    uint k = 3;
    uint k0 = 7;
    uint m = 99;
    unchecked { return 
      k*x/k0 + m;
    }
  }

  function quadratic(uint256 x) public returns (uint256) {
    uint a = 2;
    uint b = 5;
    uint c = 73;
    unchecked { return 
      a* x*x+ b * x + c;
    }
  }

}

[palinatolmach]

From previous conversations: even if the Haskell Backend/SMT solver fails, we should handle the error more gracefully and at least provide a clear error message. Related: https://github.com/runtimeverification/kontrol/issues/21