Sumit Lahiri

I noticed that the example `examples/evm/umd_example.sol` runs fine, if the `view` modifier from function in the smart contract is removed.

@step-xiaoyu-ka @mstad Facing the same issue. The bug exists in the docker image as well. ``` root@79678e02a3f8:/manticore# manticore examples/evm/umd_example.sol 2022-01-07 08:52:25,626: [17] m.main:INFO: Registered plugins: IntrospectionAPIPlugin, , 2022-01-07 08:52:25,626: [17]...

I noticed that the example `examples/evm/umd_example.sol` runs fine, if the `view` modifier from function in the smart contract is removed.

2yrs now. I am still facing this issue

Logs Mode-1 (sea with pf, no bpf) ``` /home/usea/seahorn/bin/seapp -o /tmp/sea-4y3wd57m/IntegerOverflowMultiTxMultiFuncFeasible.pp.bc --simplifycfg-sink-common=false --strip-extern=false --promote-assumptions=false --kill-vaarg=true --ignore-def-verifier-fn=false --horn-keep-arith-overflow=false --promote-nondet-undef=true --horn-replace-loops-with-nd-funcs=false IntegerOverflowMultiTxMultiFuncFeasible.ll /home/usea/seahorn/bin/seapp --simplifycfg-sink-common=false -o /tmp/sea-4y3wd57m/IntegerOverflowMultiTxMultiFuncFeasible.pp.ms.bc --horn-mixed-sem --ms-reduce-main /tmp/sea-4y3wd57m/IntegerOverflowMultiTxMultiFuncFeasible.pp.bc /home/usea/seahorn/bin/seaopt -f --simplifycfg-sink-common=false...

@agurfinkel How do I share the code here, it's a bit long. Will a drive link work?

Thanks for the clarification. Should I run the CHC mode with bpf enabled and with a higher timeout? I guess not supplying the BMC flag with bpf is still CHC...

I see. Does `bpf` activate the `bmc` mode? What if I try with `sea bpf --bmc=none ...`?

When I run my example now with SeaHorn enabling `bpf` mode with `sea bpf ...` without the `bmc` mode, I get a UNSAT result with an invariant (`--show-invars`). However, when...

Logs and the example are here. https://drive.google.com/drive/folders/1nWla3lFMn2_5hxC-sxRoqXB4ki5aPl3F?usp=sharing