Ecosyste.ms: Issues

An open API service for providing issue and pull request metadata for open source projects.

GitHub / Z3Prover/z3 issues and pull requests

#6970 - refutation unsoundness issue on a QF_AFP instance

Issue - State: closed - Opened by zhendongsu about 1 year ago - 7 comments
Labels: Floats

#6968 - Assorted fixes for floats

Pull Request - State: closed - Opened by wintersteiger about 1 year ago - 1 comment

#6967 - Z3 Rust : About Arrray

Issue - State: closed - Opened by FoxMakarov about 1 year ago - 2 comments

#6966 - Fixed next_split call in pop

Pull Request - State: closed - Opened by CEisenhofer about 1 year ago

#6965 - Java API wrong behavior for MaxSMT

Issue - State: closed - Opened by victoriafomina about 1 year ago

#6964 - python regression

Issue - State: closed - Opened by tpaviot about 1 year ago - 3 comments

#6963 - docs: More intra-doc linking, bit of formatting.

Pull Request - State: closed - Opened by waywardmonkeys about 1 year ago - 2 comments

#6961 - Bump actions/setup-node from 3 to 4

Pull Request - State: closed - Opened by dependabot[bot] about 1 year ago
Labels: dependencies, github_actions

#6960 - Update README.md

Pull Request - State: closed - Opened by itehax about 1 year ago

#6959 - Is it possible to always get rational solutions for NRA?

Issue - State: closed - Opened by anirjoshi about 1 year ago - 2 comments

#6958 - Rust Z3. How can I convert Float to f32/f64?

Issue - State: closed - Opened by FoxMakarov about 1 year ago - 1 comment

#6957 - z3-solver Z3.String() is not a function angular implementation

Issue - State: open - Opened by MargeKh about 1 year ago - 2 comments

#6955 - Assertion Violation at ../src/qe/qsat.cpp:580

Issue - State: closed - Opened by brutalsavage about 1 year ago

#6954 - Bump @babel/traverse from 7.19.4 to 7.23.2 in /src/api/js

Pull Request - State: closed - Opened by dependabot[bot] about 1 year ago
Labels: dependencies, javascript

#6953 - Support constant rotating in bit-blast

Issue - State: closed - Opened by QinshiWang about 1 year ago - 2 comments

#6952 - Redundant checks in rpolynomial.cpp

Issue - State: closed - Opened by sashakir about 1 year ago

#6951 - Dead code in nla_basics_lemmas.cpp

Issue - State: closed - Opened by sashakir about 1 year ago - 1 comment

#6950 - ASSERTION VIOLATION, File: ../src/qe/mbp/mbp_basic_tg.cpp, Line: 139

Issue - State: closed - Opened by merlinsun about 1 year ago - 1 comment
Labels: qel

#6949 - Update script to use importlib_resources

Pull Request - State: closed - Opened by rsetaluri about 1 year ago - 3 comments

#6948 - attempt improve bounds with maximize_term

Pull Request - State: closed - Opened by levnach about 1 year ago

#6946 - Issue with tactic

Issue - State: open - Opened by merlinsun about 1 year ago - 1 comment
Labels: qe

#6944 - need help for formal verifiaction of picorv32

Issue - State: closed - Opened by Vinayakamk about 1 year ago

#6943 - kernel support?

Issue - State: closed - Opened by Nitr0-G about 1 year ago - 1 comment

#6942 - Segmentation fault when testing smt2 on linux

Issue - State: closed - Opened by zhoum929 about 1 year ago - 1 comment

#6941 - Optimization issue

Issue - State: closed - Opened by nnarek about 1 year ago - 1 comment

#6940 - bug fix #6934

Pull Request - State: closed - Opened by hgvk94 about 1 year ago - 5 comments

#6939 - unit propagate more intensively in nl

Pull Request - State: closed - Opened by levnach about 1 year ago

#6938 - fix a bug in unit nl prop

Pull Request - State: closed - Opened by levnach about 1 year ago

#6937 - invalid model on an incremental QF_UFLIA instance

Issue - State: closed - Opened by zhendongsu about 1 year ago - 1 comment

#6936 - heap-use-after-free at src/util/rlimit.cpp:90

Issue - State: closed - Opened by zhendongsu about 1 year ago

#6935 - Segfault on NIRA

Issue - State: closed - Opened by merlinsun about 1 year ago

#6934 - Issue with tactic

Issue - State: closed - Opened by merlinsun about 1 year ago - 5 comments

#6933 - Make bug

Issue - State: closed - Opened by xebelleDerrel about 1 year ago - 4 comments
Labels: external

#6932 - Add RCF functions to OCaml API

Pull Request - State: closed - Opened by wintersteiger about 1 year ago - 1 comment

#6931 - increase wasm stack size

Pull Request - State: closed - Opened by LufyCZ about 1 year ago - 2 comments

#6930 - Performance issue with bitvectors combined with datatypes

Issue - State: open - Opened by talsewell about 1 year ago - 5 comments

#6929 - Fix UP registration in final callback

Pull Request - State: closed - Opened by CEisenhofer about 1 year ago

#6926 - `symbol lookup error` when trying to run `cpp_example`

Issue - State: closed - Opened by anirjoshi about 1 year ago - 3 comments

#6923 - Segmentation Fault with pb2bv tactic

Issue - State: closed - Opened by DiegoMyGit about 1 year ago - 5 comments

#6922 - 4.12.2 intermittent crash on M1 macbook with python API

Issue - State: open - Opened by mmosko about 1 year ago - 3 comments

#6921 - Z3PY hangs on formula containing Int and Bool variables

Issue - State: closed - Opened by aric-fowler about 1 year ago - 2 comments

#6920 - invalid model issue on an incremental QF_NIA instance

Issue - State: closed - Opened by zhendongsu about 1 year ago - 1 comment

#6919 - How to turn off generating ".z3-trace" file

Issue - State: closed - Opened by foreverkenan about 1 year ago - 1 comment

#6916 - Inconsistent Results from consequences Interface Based on Constant Names

Issue - State: closed - Opened by ptr1120 about 1 year ago - 1 comment

#6915 - [Question]: How to calculate upper and lower bound of floating points?

Issue - State: closed - Opened by hagozaebii about 1 year ago - 1 comment

#6914 - heap-use-after-free at src/ast/ast.h:507:36

Issue - State: closed - Opened by merlinsun about 1 year ago

#6913 - ASSERTION VIOLATION, File: ../src/qe/qe_mbp.cpp, Line: 403

Issue - State: closed - Opened by merlinsun about 1 year ago - 1 comment

#6912 - Z3Config.cmake & z3-config.cmake not found

Issue - State: closed - Opened by cctv130 about 1 year ago

#6911 - Bump docker/login-action from 2 to 3

Pull Request - State: closed - Opened by dependabot[bot] about 1 year ago
Labels: dependencies, github_actions

#6910 - Bump docker/metadata-action from 4 to 5

Pull Request - State: closed - Opened by dependabot[bot] about 1 year ago
Labels: dependencies, github_actions

#6909 - Bump docker/build-push-action from 4.2.1 to 5.0.0

Pull Request - State: closed - Opened by dependabot[bot] about 1 year ago
Labels: dependencies, github_actions

#6907 - invalid model issue on a string (QF_SNIA) instance

Issue - State: closed - Opened by zhendongsu about 1 year ago
Labels: no-repro, string

#6906 - Add c++ flags for vulcan assembly compliance

Pull Request - State: closed - Opened by jfleisher about 1 year ago

#6905 - Unit propagation on monomials

Pull Request - State: closed - Opened by levnach about 1 year ago

#6902 - Segfault on OpenBSD

Issue - State: closed - Opened by bentley about 1 year ago - 46 comments

#6901 - Running Z3 C++ in macOS Ventura

Issue - State: closed - Opened by anirjoshi about 1 year ago

#6900 - Running Z3 using c++ in Ubuntu 20.04

Issue - State: closed - Opened by anirjoshi about 1 year ago - 3 comments

#6899 - Undefined symbols for architecture arm64

Issue - State: closed - Opened by aliesh1996 about 1 year ago

#6898 - [Performance] redundant copies in the C++ source

Issue - State: closed - Opened by sdingcn about 1 year ago - 1 comment

#6897 - Provide static version of prebuilt z3 library in GitHub Release

Issue - State: closed - Opened by TheVeryDarkness about 1 year ago - 1 comment

#6896 - Bump docker/build-push-action from 4.1.1 to 4.2.1

Pull Request - State: closed - Opened by dependabot[bot] about 1 year ago
Labels: dependencies, github_actions

#6895 - Clear up Z3_LIBRARY_PATH error message

Pull Request - State: closed - Opened by SijmenHuizenga about 1 year ago

#6894 - Refutational Soundness issue on QF_BV

Issue - State: closed - Opened by fwangdo about 1 year ago

#6893 - [Question] How to use `rotate_right` in z3py?

Issue - State: closed - Opened by hagozaebii about 1 year ago - 4 comments

#6891 - Z3 solver BitVec URem performace

Issue - State: closed - Opened by antonper about 1 year ago - 7 comments

#6890 - ThirdParty Memory Allocators still causes crash

Issue - State: closed - Opened by Naville about 1 year ago - 13 comments

#6889 - ASSERTION VIOLATION, File: ../src/qe/qe_mbp.cpp, Line: 572

Issue - State: closed - Opened by merlinsun about 1 year ago - 4 comments
Labels: qel

#6888 - Bump actions/checkout from 3 to 4

Pull Request - State: closed - Opened by dependabot[bot] about 1 year ago
Labels: dependencies, github_actions

#6887 - missing rewriter_tpl instances

Pull Request - State: closed - Opened by xantares about 1 year ago - 1 comment

#6885 - The z3py polynomial solver returned incorrect results

Issue - State: closed - Opened by frankeyjin about 1 year ago - 1 comment

#6884 - add the option :pi.enabled to disable pattern inference for quantifiers

Pull Request - State: closed - Opened by utaal about 1 year ago

#6883 - [draft] Use half SipHash-1-3 for AST hashing

Pull Request - State: closed - Opened by nunoplopes about 1 year ago - 7 comments

#6881 - Outermost existential quantifier prevents solution from being found

Issue - State: closed - Opened by pclayton about 1 year ago - 1 comment

#6880 - Configure a quantifier so it cannot be instantiated by e-matching

Issue - State: closed - Opened by utaal about 1 year ago - 4 comments

#6879 - local updates

Pull Request - State: closed - Opened by NikolajBjorner about 1 year ago

#6879 - local updates

Pull Request - State: closed - Opened by NikolajBjorner about 1 year ago

#6878 - print deq in lits2pure. fix #6877

Pull Request - State: closed - Opened by hgvk94 about 1 year ago

#6877 - segmentation fault with get-interpolant

Issue - State: closed - Opened by LeventErkok about 1 year ago

#6876 - Segmentation fault using recursive function

Issue - State: closed - Opened by pcarbonn about 1 year ago

#6875 - Explain max term

Pull Request - State: closed - Opened by levnach about 1 year ago

#6871 - ASSERTION VIOLATION, File: ../src/math/polynomial/algebraic_numbers.cpp, Line: 2462

Issue - State: open - Opened by zhendongsu about 1 year ago - 2 comments
Labels: nlsat

#6870 - broken links in API documentation

Issue - State: open - Opened by polgreen about 1 year ago - 1 comment

#6870 - broken links in API documentation

Issue - State: open - Opened by polgreen about 1 year ago - 1 comment

#6870 - broken links in API documentation

Issue - State: closed - Opened by polgreen about 1 year ago - 2 comments

#6867 - support or, and, implies, distinct in mbp_basic. fix #6865 #6866

Pull Request - State: closed - Opened by hgvk94 about 1 year ago

#6867 - support or, and, implies, distinct in mbp_basic. fix #6865 #6866

Pull Request - State: closed - Opened by hgvk94 about 1 year ago

#6867 - support or, and, implies, distinct in mbp_basic. fix #6865 #6866

Pull Request - State: closed - Opened by hgvk94 about 1 year ago

#6866 - ASSERTION VIOLATION, File: ../src/qe/mbp/mbp_arrays_tg.cpp, Line: 281

Issue - State: closed - Opened by merlinsun about 1 year ago - 2 comments

#6866 - ASSERTION VIOLATION, File: ../src/qe/mbp/mbp_arrays_tg.cpp, Line: 281

Issue - State: closed - Opened by merlinsun about 1 year ago - 2 comments

#6866 - ASSERTION VIOLATION, File: ../src/qe/mbp/mbp_arrays_tg.cpp, Line: 281

Issue - State: closed - Opened by merlinsun about 1 year ago - 2 comments

#6865 - ASSERTION VIOLATION, File: ../src/qe/mbp/mbp_basic_tg.cpp, Line: 60

Issue - State: closed - Opened by zhendongsu over 1 year ago - 2 comments