Sumit Lahiri

### Summary of the problem ### Manticore version Latest version from Manticore GitHub repo. ### Python version 3.8.10 ### OS / Environment Distributor ID: Ubuntu Description: Ubuntu 20.04.3 LTS Release:...

Docker image of Manticore from Docker Hub fails to run `examples/evm/umd_example.sol` example

1

### Summary of the problem Docker image of Manticore from Docker Hub fails to run `examples/evm/umd_example.sol` example. The example fails with the following error. ``` m.c.worker:ERROR: Exception in state 1:...

- Migrating from `Tensorflow 1` to `Tensorflow 2`. - Changes the way `projector `is imported.

Sample Interpretation.

1

Thanks for the sampler tool. I had one query regarding the sample produced. How do I interpret the sample? I wanted to know the value of each bit vector entry...

CHC mode with `pf` timeout but BMC gives `sat` result. Why are they giving different results?

13

**Describe the bug** SeaHorn produces SAT result in the BMC mode but leads to timeout in CHC mode (using no bmc flags). We are trying to catch a bug, using...

Not able to emit loop invariant for a program.

1

**Describe the bug** When using the `--show-invars` flags while invoking the program with `sea pf`, tool does not emit loop invariant. Please guide me here. Is this the correct output?...

How does loops work? How does Gigahorse translate loops?

3

I am not able to understand the translation of a loop function to the IR generated by Gigahorse. I have a solidity function that looks like the example shown below....

Query regarding SeaHorn BPF mode with CHC Solver.

5

**Describe the bug** SeaHorn seems to produce an incorrect result when running in `bpf` mode solving. **To Reproduce** I have the following program where the `sassert()` call should fail when...

No counterexample but Seahorn gives SAT answer.

5

**Describe the bug** No counterexample but Seahorn gives SAT answer. Example Program ```c #include "seahorn/seahorn.h" #include #define int int int l1( int i1, int i2, int bnd ) { int...

Input Program ``` #include "seahorn/seahorn.h" #include #define int int int l1(int i1, int i2, int bnd) { int _out; int _out_s17 = ((i2) == (i1) ? 1 : 0); _out...