Comments (2)
r0qs
commented on June 22, 2024
Hi @alex1448, thank you for raising the issue. It appears that the smtAssert(false) is triggered when utilizing chc as the model checker engine option. Interestingly, this error does not manifest when using the bmc engine.
The kind of the generated Z3 expression seems to be interpreted as a Z3_OP_CONCAT, i.e. bit-vector concatenation, which, to the best of my knowledge, is currently unsupported by Z3Interface::fromZ3Expr. Perhaps @blishko has insights into this issue and suggestions for addressing it.
from solidity.
Related Issues (20)
- Enable function overloading resolution when importing specific libraries or free functions via `using for` HOT 3
- `StackCompressor` goes into infinite loop after `SSATransform` on inline assembly with very long chains of dependent assignments HOT 2
- Add blobhash inside the `tx` context: blobhash(uint index) --> tx.blobhash(uint index) HOT 4
- SMTChecker: Use SMT-LIB interface instead of solvers' APIs
- Lack of proper heuristics in the Function Specializer can lead to large contract sizes HOT 5
- build solidity error HOT 3
- When compiling with the `via-ir` option, calldata out-of-bounds causes the transaction to revert HOT 1
- Support for Compiling Solidity to LLVM IR to Facilitate zkVM Adoption?
- Switch default EVM version to Cancun
- Performance issues of `solc --abi --via-ir` HOT 6
- Verifying blobhash causes failure to obtain gasLimit HOT 2
- Security vulnerability: Why do % and MOD result in different outputs despite being technically the same function? HOT 2
- SMT logic error for a conditional with empty tuple types
- Code Deduplication Creates Wrong Source Mappings HOT 1
- `memory-safe` Assembly Worsens Optimizations HOT 2
- Reduce default font weight for readability HOT 2
- Providing an empty string to `--yul-optimizations` without enabling yul optimization triggers uncaught exception HOT 1
- Version the `list.json` file for build information
- Abnormal execution time of the SMTChecker HOT 2
Recommend Projects
-
React
A declarative, efficient, and flexible JavaScript library for building user interfaces.
-
Vue.js
🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
-
Typescript
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
-
TensorFlow
An Open Source Machine Learning Framework for Everyone
-
Django
The Web framework for perfectionists with deadlines.
-
Laravel
A PHP framework for web artisans
-
D3
Bring data to life with SVG, Canvas and HTML. 📊📈🎉
-
Recommend Topics
-
javascript
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
-
web
Some thing interesting about web. New door for the world.
-
server
A server is a program made to process requests and deliver data to clients.
-
Machine learning
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
-
Visualization
Some thing interesting about visualization, use data art
-
Game
Some thing interesting about game, make everyone happy.
Recommend Org
-
Facebook
We are working to build community through open source technology. NB: members must have two-factor auth.
-
Microsoft
Open source projects and samples from Microsoft.
-
Google
Google ❤️ Open Source for everyone.
-
Alibaba
Alibaba Open Source for everyone
-
D3
Data-Driven Documents codes.
-
Tencent
China tencent open source team.
from solidity.