Z3Prover/z3 issues and pull requests

#7296 - new hashtable.h invariants

Pull Request - State: closed - Opened by ChuyueSun 2 months ago

#7295 - performance on bit vectors

Issue - State: open - Opened by Heaven2024 2 months ago

#7294 - New invariant for dlist

Pull Request - State: closed - Opened by ChuyueSun 2 months ago

#7294 - New invariant for dlist

Pull Request - State: closed - Opened by ChuyueSun 2 months ago

#7294 - New invariant for dlist

Pull Request - State: closed - Opened by ChuyueSun 2 months ago

#7294 - New invariant for dlist

Pull Request - State: closed - Opened by ChuyueSun 2 months ago

#7294 - New invariant for dlist

Pull Request - State: closed - Opened by ChuyueSun 2 months ago

#7294 - New invariant for dlist

Pull Request - State: closed - Opened by ChuyueSun 2 months ago

#7293 - unit tests for dlist.h

Pull Request - State: closed - Opened by ChuyueSun 2 months ago

#7293 - unit tests for dlist.h

Pull Request - State: closed - Opened by ChuyueSun 2 months ago

#7293 - unit tests for dlist.h

Pull Request - State: closed - Opened by ChuyueSun 2 months ago

#7293 - unit tests for dlist.h

Pull Request - State: closed - Opened by ChuyueSun 2 months ago

#7293 - unit tests for dlist.h

Pull Request - State: closed - Opened by ChuyueSun 2 months ago

#7293 - unit tests for dlist.h

Pull Request - State: closed - Opened by ChuyueSun 2 months ago

#7292 - Suspected bug due to copy-pasted code in mbp_basic_tg.cpp

Issue - State: open - Opened by ustchcs-bugfinder 3 months ago

#7292 - Suspected bug due to copy-pasted code in mbp_basic_tg.cpp

Issue - State: closed - Opened by ustchcs-bugfinder 3 months ago

#7292 - Suspected bug due to copy-pasted code in mbp_basic_tg.cpp

Issue - State: open - Opened by ustchcs-bugfinder 3 months ago

#7291 - arm64 linux versions in release are actually providing x86_64 binaries

Issue - State: closed - Opened by panda2134 3 months ago - 2 comments

#7291 - arm64 linux versions in release are actually providing x86_64 binaries

Issue - State: closed - Opened by panda2134 3 months ago - 2 comments

#7291 - arm64 linux versions in release are actually providing x86_64 binaries

Issue - State: closed - Opened by panda2134 3 months ago - 2 comments

#7291 - arm64 linux versions in release are actually providing x86_64 binaries

Issue - State: closed - Opened by panda2134 3 months ago - 2 comments

#7289 - Bump docker/build-push-action from 6.3.0 to 6.4.0

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

#7288 - add new ema invariant

Pull Request - State: closed - Opened by ChuyueSun 3 months ago

#7287 - Linux arm64 releases contain x86-64 binaries

Issue - State: open - Opened by tchajed 3 months ago - 1 comment

#7287 - Linux arm64 releases contain x86-64 binaries

Issue - State: closed - Opened by tchajed 3 months ago - 2 comments

#7286 - Possibly a bug - Int type

Issue - State: closed - Opened by DennisYurichev 3 months ago - 5 comments

#7285 - "mbp to_real" when using spacer with global guidance

Issue - State: open - Opened by mmsbrggr 3 months ago - 2 comments

#7284 - ASSERTION VIOLATION File: ../src/ast/ast.cpp Line: 388 UNEXPECTED CODE WAS REACHED. Z3 4.13.1.0

Issue - State: open - Opened by Sunshien-CC 3 months ago - 1 comment

#7284 - ASSERTION VIOLATION File: ../src/ast/ast.cpp Line: 388 UNEXPECTED CODE WAS REACHED. Z3 4.13.1.0

Issue - State: closed - Opened by Sunshien-CC 3 months ago - 1 comment

#7283 - Uncollected memory

Issue - State: open - Opened by Flians 3 months ago

#7283 - Uncollected memory

Issue - State: open - Opened by Flians 3 months ago

#7283 - Uncollected memory

Issue - State: closed - Opened by Flians 3 months ago - 2 comments

#7282 - Strategy for different types of SMT problems

Issue - State: closed - Opened by huhuhu777 3 months ago

#7281 - When using rlimit, z3 gives an output but keeps running for a long time

Issue - State: closed - Opened by hmijail 3 months ago - 5 comments

#7281 - When using rlimit, z3 gives an output but keeps running for a long time

Issue - State: open - Opened by hmijail 3 months ago

#7281 - When using rlimit, z3 gives an output but keeps running for a long time

Issue - State: open - Opened by hmijail 3 months ago

#7280 - Bump docker/build-push-action from 6.2.0 to 6.3.0

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

#7280 - Bump docker/build-push-action from 6.2.0 to 6.3.0

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

#7280 - Bump docker/build-push-action from 6.2.0 to 6.3.0

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

#7280 - Bump docker/build-push-action from 6.2.0 to 6.3.0

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

#7277 - Wrong solution of quantitative formula

Issue - State: open - Opened by Heaven2024 3 months ago - 1 comment

#7277 - Wrong solution of quantitative formula

Issue - State: closed - Opened by Heaven2024 3 months ago - 3 comments

#7276 - Questions about the combination of quantitative formulas

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

#7276 - Questions about the combination of quantitative formulas

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

#7275 - Project Euler 142 and Google OR-tools

Issue - State: open - Opened by DennisYurichev 3 months ago - 1 comment

#7275 - Project Euler 142 and Google OR-tools

Issue - State: closed - Opened by DennisYurichev 3 months ago - 1 comment

#7275 - Project Euler 142 and Google OR-tools

Issue - State: closed - Opened by DennisYurichev 3 months ago - 1 comment

#7274 - unknown with bit-blast

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

#7274 - unknown with bit-blast

Issue - State: open - Opened by Heaven2024 3 months ago

#7274 - unknown with bit-blast

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

#7273 - Optimize not respecting constraint that Solver respects

Issue - State: closed - Opened by skeggse 3 months ago - 2 comments

#7272 - Incorrect solution regarding data type conversion

Issue - State: closed - Opened by Heaven2024 3 months ago - 2 comments

#7271 - Fix a comment for Z3_solver_from_string

Pull Request - State: closed - Opened by ligurio 3 months ago

#7270 - `z3` cannot understand the models it produces

Issue - State: closed - Opened by yav 3 months ago

#7269 - Bump docker/build-push-action from 6.1.0 to 6.2.0

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

#7268 - Incorrect definition order in `get-model`

Issue - State: closed - Opened by yav 3 months ago

#7267 - Timeout on Simple String Formula

Issue - State: closed - Opened by levinwinter 3 months ago - 3 comments

#7266 - Unexpected code reached

Issue - State: closed - Opened by Lotan-Raz 3 months ago - 1 comment

#7265 - Bump docker/build-push-action from 6.0.0 to 6.1.0

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

#7264 - Error when using `model.completion=true` with DT

Issue - State: closed - Opened by nafur 3 months ago

#7264 - Error when using `model.completion=true` with DT

Issue - State: closed - Opened by nafur 3 months ago

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

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

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

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

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

Pull Request - State: closed - Opened by dependabot[bot] 3 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] 3 months ago
Labels: dependencies, javascript

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

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

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

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

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

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

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

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

#7258 - Z3 does not recognize the QF_DTLIA logic

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

#7258 - Z3 does not recognize the QF_DTLIA logic

Issue - State: closed - Opened by yoni206 3 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] 3 months ago
Labels: dependencies, github_actions

#7255 - Possible regression between 4.12.1 and 4.13.0

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

#7255 - Possible regression between 4.12.1 and 4.13.0

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

#7255 - Possible regression between 4.12.1 and 4.13.0

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

#7254 - WIP: Migrating OCaml binding to CMake

Pull Request - State: open - Opened by arbipher 4 months ago - 1 comment

#7254 - WIP: Migrating OCaml binding to CMake

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

#7253 - conflicts with libgc

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

#7253 - conflicts with libgc

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

#7252 - Segfault on a nested re.loop formula

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

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

Pull Request - State: closed - Opened by dependabot[bot] 4 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 4 months ago - 2 comments

#7249 - Solving problems with formulas related to square roots

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

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

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

#7247 - rlimit fails to stop z3

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

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

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

#7245 - Non-deterministic correctness bug in QF_LIA optimization

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

#7244 - Clear up inefficient code

Pull Request - State: closed - Opened by CoolThi 4 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 4 months ago

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

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

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

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

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

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

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

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

#7235 - Fix compilation error in column_info

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

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

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

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

Issue - State: open - Opened by burgholzer 4 months ago

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

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

#7230 - intblast: fix translation of sign_ext

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

#7229 - Z3_solver_pop() does not clear ASTs

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

#7228 - Remaining deprecated `distutils` in Python scripts.

Issue - State: open - Opened by arbipher 5 months ago

GitHub / Z3Prover/z3 issues and pull requests