z3
z3 copied to clipboard
Z3Prover
The Z3 Theorem Prover
``` [659] % z3release model_validate=true small.smt2 sat sat sat sat sat sat sat sat sat sat sat sat sat (error "line 27 column 10: an invalid model was generated") (...
Following @agurfinkel 's recommendation, I tried latest master on the benchmarks I have where Eldarica performed better, specifically this directory: https://github.com/leonardoalt/chc_benchmarks_solidity/tree/main/unit_tests/abi . The results improved massively! z3 now outperforms Eldarica...
The --js option currently fails in the Azure pipelines for nightly doc builds. It is a hosted build (ubuntu-latest) and may need to be configured with a version of npm....
I'm using Z3 on a personal project, I am able to get the results form the solve function, however, the process won't stop unless I force it with 'process.exit()'. This...
There seems to be an issue with the async mechanism used in the Javascript/Typescript API (ref: https://www.npmjs.com/package/z3-solver). Specifically, the async process spawned never terminates (and the undocumented workaround in the...
Hello, Scenario: Cent OS 7 Z3 From Nugget 4.8.4 (I used 4.8.9 as well) C# Code. Exception ``` ---> (Inner Exception #32) System.DllNotFoundException: Unable to load shared library 'libz3' or...
Is there any plan to support finite sets with cardinality reasoning in Z3? This feature would be very useful for verifying concurrent and distributed systems.
I am not quite sure how to diagnose this bug myself. It doesn't seem to me that this input is too complicated (though I wasn't expecting z3 to be able...
Hi, While trying to validate the interpretations generated by Spacer for a number of [CHC-comp](https://github.com/chc-comp/chc-comp22-benchmarks) instances, I believe I found some examples in which invalid interpretations are generated. Below is...
Hi ! Before going into my problem, I wanted to first thank all the amazing contributors here for this fantastic open sourced repository. It's genuinely wonderful. Now straight to the...
