Z3Prover/z3 issues and pull requests

#7262 - Optimization in combination with custom data-types gives unexpected results

Issue - State: closed - Opened by joukestoel-axini 5 months ago - 1 comment

#7262 - Optimization in combination with custom data-types gives unexpected results

Issue - State: open - Opened by joukestoel-axini 5 months ago

#7261 - Bump braces from 3.0.2 to 3.0.3 in /src/api/js

Pull Request - State: closed - Opened by dependabot[bot] 5 months ago
Labels: dependencies, javascript

#7261 - Bump braces from 3.0.2 to 3.0.3 in /src/api/js

Pull Request - State: closed - Opened by dependabot[bot] 5 months ago
Labels: dependencies, javascript

#7260 - `Z3_solver_reset` may not properly reset parser context

Issue - State: closed - Opened by pclayton 5 months ago

#7260 - `Z3_solver_reset` may not properly reset parser context

Issue - State: closed - Opened by pclayton 5 months ago

#7259 - ASSERTION VIOLATION, File: ../src/qe/qe_mbp.cpp Line: 404

Issue - State: closed - Opened by merlinsun 5 months ago - 1 comment
Labels: qel, qe

#7259 - ASSERTION VIOLATION, File: ../src/qe/qe_mbp.cpp Line: 404

Issue - State: closed - Opened by merlinsun 5 months ago - 1 comment
Labels: qel, qe

#7258 - Z3 does not recognize the QF_DTLIA logic

Issue - State: closed - Opened by yoni206 5 months ago - 1 comment

#7258 - Z3 does not recognize the QF_DTLIA logic

Issue - State: closed - Opened by yoni206 5 months ago - 1 comment

#7257 - Bump docker/build-push-action from 5.3.0 to 6.0.0

Pull Request - State: closed - Opened by dependabot[bot] 5 months ago
Labels: dependencies, github_actions

#7255 - Possible regression between 4.12.1 and 4.13.0

Issue - State: open - Opened by blishko 5 months ago - 5 comments
Labels: Horn

#7255 - Possible regression between 4.12.1 and 4.13.0

Issue - State: open - Opened by blishko 5 months ago - 1 comment
Labels: Horn

#7255 - Possible regression between 4.12.1 and 4.13.0

Issue - State: closed - Opened by blishko 5 months ago - 6 comments
Labels: Horn

#7254 - WIP: Migrating OCaml binding to CMake

Pull Request - State: open - Opened by arbipher 5 months ago - 3 comments

#7254 - WIP: Migrating OCaml binding to CMake

Pull Request - State: open - Opened by arbipher 5 months ago

#7253 - conflicts with libgc

Issue - State: closed - Opened by KuiWei004 5 months ago - 2 comments

#7253 - conflicts with libgc

Issue - State: closed - Opened by KuiWei004 5 months ago - 2 comments

#7252 - Segfault on a nested re.loop formula

Issue - State: closed - Opened by muchang 5 months ago

#7251 - Bump docker/build-push-action from 5.3.0 to 5.4.0

Pull Request - State: closed - Opened by dependabot[bot] 5 months ago - 1 comment
Labels: dependencies, github_actions

#7250 - Multiple Segmentation Faults When Producing Proofs with "sat.euf=true tactic.default_tactic=smt..."

Issue - State: closed - Opened by SunHao-0 5 months ago - 2 comments

#7249 - Solving problems with formulas related to square roots

Issue - State: closed - Opened by Heaven2024 5 months ago - 1 comment

#7248 - Performance on solve a logical problem about unexplained functions

Issue - State: closed - Opened by Heaven2024 5 months ago - 1 comment

#7247 - rlimit fails to stop z3

Issue - State: closed - Opened by hmijail 5 months ago - 1 comment

#7246 - Segfault is triggered when push is before logic set

Issue - State: closed - Opened by Heaven2024 6 months ago

#7245 - Non-deterministic correctness bug in QF_LIA optimization

Issue - State: closed - Opened by mikand 6 months ago

#7244 - Clear up inefficient code

Pull Request - State: closed - Opened by CoolThi 6 months ago - 1 comment

#7242 - is there an implementation available in the high level api for string variables/sorts in typescript?

Issue - State: closed - Opened by uwesimm 6 months ago

#7241 - Z3 proves `(= 0.0 (^ 0 (- 2))`

Issue - State: closed - Opened by someplaceguy 6 months ago - 1 comment

#7240 - Semantics of "box" for "opt.priority" optimization

Issue - State: open - Opened by mikand 6 months ago - 2 comments

#7238 - Alternative solutions for z3-solver without using SharedArrayBuffer or COOP/COEP headers

Issue - State: open - Opened by MargeKh 6 months ago

#7237 - reading string value from the output of z3 consequence API throws exception

Issue - State: closed - Opened by chauhansantosh17 6 months ago - 1 comment

#7235 - Fix compilation error in column_info

Pull Request - State: closed - Opened by waywardmonkeys 6 months ago - 1 comment

#7234 - Timeout not working on z3 python in the second `s.check()` call

Issue - State: closed - Opened by anirjoshi 6 months ago - 1 comment

#7232 - aarch64 linux wheel is tagged `manylinux2014` despite actually being `manylinux_2_34`

Issue - State: closed - Opened by burgholzer 6 months ago - 1 comment

#7231 - Solver printing wrong model in C++ api

Issue - State: closed - Opened by anirjoshi 6 months ago - 1 comment

#7230 - intblast: fix translation of sign_ext

Pull Request - State: closed - Opened by JakobR 6 months ago

#7229 - Z3_solver_pop() does not clear ASTs

Issue - State: closed - Opened by remysucre 6 months ago - 1 comment