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

#6631 - Multiple assertions with inequalities and fix values take forever to check

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

#6630 - [Question] When model of sat bit-vector formula would be an empty list?

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

#6629 - Question about paralell SMT solving engines in Z3

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

#6628 - fix a tiny typo

Pull Request - State: closed - Opened by ffwangdo over 1 year ago

#6627 - use uintptr_t instead of size_t (tptr) for portability

Pull Request - State: closed - Opened by igcontreras over 1 year ago - 1 comment

#6626 - Make all methods show in java API

Pull Request - State: closed - Opened by BramVerb over 1 year ago - 7 comments

#6625 - fix unsound slice criteria

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

#6624 - Sequences/map: Decidability regression

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

#6623 - remove operation with doubles

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

#6621 - Constraint added is changing based on prior constraint

Issue - State: closed - Opened by BobChuckyJoe over 1 year ago - 1 comment

#6620 - (rewriter.hi_div0=false) Unsoundness on simple bitvector formula

Issue - State: closed - Opened by wintered over 1 year ago - 1 comment

#6619 - restore the previous state

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

#6618 - bug fix. Prevent resetting gg stats #6062

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

#6615 - Intermittent segfault

Issue - State: closed - Opened by aaronbembenek over 1 year ago

#6611 - Decidability of SMT problems

Issue - State: closed - Opened by GrafBlutwurst over 1 year ago

#6572 - Linux release builds of 4.12.x depend on very new distributions

Issue - State: closed - Opened by atomb almost 2 years ago - 7 comments

#6553 - Fuzz bugs for floats - unsoundness / Invalid model issue on default mode

Issue - State: closed - Opened by ffwangdo almost 2 years ago - 4 comments
Labels: Floats

#6537 - Z3 failed to runtests due to run test-z3.exe smt2print_parse under amd64 mode

Issue - State: closed - Opened by nnfdnkns almost 2 years ago - 4 comments
Labels: no-repro

#6534 - WiP: nightly versioning for distinct symbol archiving by version

Pull Request - State: open - Opened by jfleisher almost 2 years ago

#6523 - [consolidated] issues with new core

Issue - State: closed - Opened by NikolajBjorner almost 2 years ago - 42 comments

#6512 - NodeJs process won't stop after using 'solve' or 'solver.check()'

Issue - State: open - Opened by eliachiarucci almost 2 years ago - 1 comment
Labels: javascript

#6495 - Assertion violation at ../src/smt/tactic/ctx_solver_simplify_tactic.cpp:140

Issue - State: open - Opened by merlinsun almost 2 years ago - 1 comment
Labels: string

#6471 - Potential Horn soundness issue

Issue - State: open - Opened by leonardoalt almost 2 years ago - 4 comments
Labels: Horn

#6346 - invalid model issue on an incremental string formula

Issue - State: open - Opened by zhendongsu about 2 years ago - 11 comments
Labels: string

#6308 - Assertion violation at File: ../src/nlsat/nlsat_interval_set.cpp:94

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

#6280 - Publish Z3 symbols

Pull Request - State: closed - Opened by jfleisher over 2 years ago - 2 comments

#6278 - Update github service connection

Pull Request - State: closed - Opened by jfleisher over 2 years ago

#6277 - Fix errors from obsolete ubuntu VM

Pull Request - State: closed - Opened by jfleisher over 2 years ago

#6155 - Add --js to nightly and release doc builds

Issue - State: open - Opened by NikolajBjorner over 2 years ago - 2 comments
Labels: javascript

#6117 - [consolidated] issues in FP

Issue - State: closed - Opened by zhendongsu over 2 years ago - 12 comments
Labels: Floats

#6097 - Java API for custom User Propagators

Issue - State: closed - Opened by ThomasHaas over 2 years ago - 17 comments

#6079 - Invalid model issue on fp

Issue - State: closed - Opened by merlinsun over 2 years ago - 8 comments
Labels: Floats

#6062 - Z3 diverges on example from Bradley's IC3 paper

Issue - State: closed - Opened by Columpio over 2 years ago - 4 comments
Labels: Horn

#6015 - SIGBUS due to unaligned access

Issue - State: closed - Opened by arrowd over 2 years ago - 30 comments

#5925 - Assertion violation at /src/qe/mbp/mbp_arrays.cpp:477

Issue - State: closed - Opened by merlinsun over 2 years ago - 3 comments

#5785 - Assertation voilation at ../src/math/polynomial/algebraic_numbers.cpp, Line: 2449

Issue - State: closed - Opened by zhendongsu almost 3 years ago - 3 comments
Labels: nlsat

#5785 - Assertation voilation at ../src/math/polynomial/algebraic_numbers.cpp, Line: 2449

Issue - State: closed - Opened by zhendongsu almost 3 years ago - 3 comments
Labels: nlsat

#5659 - Wrong includedir returned by pkg-config on Fedora

Issue - State: closed - Opened by torokati44 about 3 years ago - 5 comments

#5648 - Regex performance cliff when using `InRe`

Issue - State: open - Opened by ahelwer about 3 years ago - 17 comments
Labels: string

#5555 - Fix Z3Config.cmake.in when generating a static library

Pull Request - State: closed - Opened by mrexodia about 3 years ago

#5555 - Fix Z3Config.cmake.in when generating a static library

Pull Request - State: closed - Opened by mrexodia about 3 years ago

#5555 - Fix Z3Config.cmake.in when generating a static library

Pull Request - State: closed - Opened by mrexodia about 3 years ago

#5555 - Fix Z3Config.cmake.in when generating a static library

Pull Request - State: closed - Opened by mrexodia about 3 years ago

#5073 - Internal variables in proofs

Issue - State: closed - Opened by m-fleury over 3 years ago - 5 comments

#4841 - Invalid model for QF_FP formula

Issue - State: closed - Opened by rainoftime almost 4 years ago - 3 comments
Labels: Floats

#4804 - Refutation unsoundness on NRA formula with =>

Issue - State: closed - Opened by muchang almost 4 years ago - 7 comments
Labels: nlsat

#4802 - (rewriter.flat=false) Solution soundness issue on QF_NRA formula

Issue - State: closed - Opened by muchang almost 4 years ago
Labels: no-repro, nlsat

#4780 - Unable to load shared library 'libz3'

Issue - State: open - Opened by EdilsonGalvao about 4 years ago - 8 comments
Labels: API usability / compile

#4772 - Error in Spacer

Issue - State: closed - Opened by blishko about 4 years ago - 1 comment
Labels: Horn

#4670 - integer optimization bug in python

Issue - State: open - Opened by amchiclet about 4 years ago - 6 comments

#4670 - integer optimization bug in python

Issue - State: open - Opened by amchiclet about 4 years ago - 6 comments

#4670 - integer optimization bug in python

Issue - State: open - Opened by amchiclet about 4 years ago - 6 comments

#3595 - Incorrect objective values with real optimization

Issue - State: closed - Opened by LeventErkok over 4 years ago - 4 comments

#3117 - Rs

Pull Request - State: open - Opened by NikolajBjorner over 4 years ago - 4 comments

#2867 - Assertion violation at ../src/nlsat/nlsat_interval_set.cpp line 84

Issue - State: closed - Opened by muchang almost 5 years ago - 4 comments
Labels: bug, no-repro, nlsat

#2690 - macOS Catalina error: z3 cannot be opened because the developer cannot be verified

Issue - State: open - Opened by pietrobraione about 5 years ago - 3 comments
Labels: API usability / compile

#2690 - macOS Catalina error: z3 cannot be opened because the developer cannot be verified

Issue - State: open - Opened by pietrobraione about 5 years ago - 3 comments
Labels: API usability / compile

#2650 - Incorrect result in NRA formula 2

Issue - State: open - Opened by muchang about 5 years ago - 34 comments
Labels: bug, nlsat

#2650 - Incorrect result in NRA formula 2

Issue - State: open - Opened by muchang about 5 years ago - 35 comments
Labels: bug, nlsat

#2650 - Incorrect result in NRA formula 2

Issue - State: open - Opened by muchang about 5 years ago - 35 comments
Labels: bug, nlsat

#2608 - Incorrect result on NRA formula

Issue - State: closed - Opened by muchang about 5 years ago - 2 comments
Labels: bug, no-repro

#2176 - Save and Restore solver state

Issue - State: closed - Opened by MarianAldenhoevel over 5 years ago - 5 comments

#1793 - Parser error for large numbers

Issue - State: closed - Opened by layderv over 6 years ago - 2 comments

#1793 - Parser error for large numbers

Issue - State: closed - Opened by layderv over 6 years ago - 2 comments

#1770 - z3 (python) issues misleading error when import libz3.so

Issue - State: closed - Opened by typon over 6 years ago - 4 comments

#1757 - SMTLib compliance: divisible predicate is missing

Issue - State: closed - Opened by LeventErkok over 6 years ago - 6 comments

#1139 - Instable Java API in comparison to commandline-tool

Issue - State: open - Opened by facferreira over 7 years ago - 5 comments
Labels: performance

#868 - Enabling proofs per solver instance

Issue - State: closed - Opened by PhilippWendler almost 8 years ago - 6 comments

#446 - Fix gcc build failure on ARM caused by including <emmintrin.h>

Pull Request - State: closed - Opened by msullivan almost 9 years ago - 4 comments

#294 - Z3 Java API fails to detect libz3.dylib

Issue - State: closed - Opened by Eipifi about 9 years ago - 22 comments