Z3Prover z3 issues - Githubissues

Z3Prover / z3

The Z3 Theorem Prover

Other

9.96k stars 1.46k forks source link

issues

Newest

Newest Most commented Recently updated Oldest Least commented Least recently updated

Questions about the combination of quantitative formulas

#7276 Heaven2024 opened 7 hours ago
0
Project Euler 142 and Google OR-tools

#7275 DennisYurichev opened 9 hours ago
1
unknown with bit-blast

#7274 Heaven2024 opened 9 hours ago
0
Optimize not respecting constraint that Solver respects

#7273 skeggse opened 1 day ago
0
Incorrect solution regarding data type conversion

#7272 Heaven2024 opened 2 days ago
0
Fix a comment for Z3_solver_from_string

#7271 ligurio closed 2 days ago
0
`z3` cannot understand the models it produces

#7270 yav opened 3 days ago
0
Bump docker/build-push-action from 6.1.0 to 6.2.0

#7269 dependabot[bot] closed 3 days ago
0
Incorrect definition order in `get-model`

#7268 yav opened 3 days ago
0
Timeout on Simple String Formula

#7267 levinwinter closed 4 days ago
2
Unexpected code reached

#7266 Lotan-Raz closed 1 week ago
1
Bump docker/build-push-action from 6.0.0 to 6.1.0

#7265 dependabot[bot] closed 1 week ago
0
Error when using `model.completion=true` with DT

#7264 nafur closed 1 week ago
0
Optimization in combination with custom data-types gives unexpected results

#7262 joukestoel-axini opened 2 weeks ago
0
Bump braces from 3.0.2 to 3.0.3 in /src/api/js

#7261 dependabot[bot] closed 2 weeks ago
0
`Z3_solver_reset` may not properly reset parser context

#7260 pclayton closed 2 weeks ago
0
ASSERTION VIOLATION, File: ../src/qe/qe_mbp.cpp Line: 404

#7259 merlinsun closed 2 weeks ago
1
Z3 does not recognize the QF_DTLIA logic

#7258 yoni206 closed 2 weeks ago
1
Bump docker/build-push-action from 5.3.0 to 6.0.0

#7257 dependabot[bot] closed 2 weeks ago
0
Possible regression between 4.12.1 and 4.13.0

#7255 blishko opened 2 weeks ago
1
WIP: Migrating OCaml binding to CMake

#7254 arbipher opened 2 weeks ago
1
conflicts with libgc

#7253 KuiWei004 closed 2 weeks ago
2
Segfault on a nested re.loop formula

#7252 muchang closed 2 weeks ago
0
Bump docker/build-push-action from 5.3.0 to 5.4.0

#7251 dependabot[bot] closed 2 weeks ago
1
Multiple Segmentation Faults When Producing Proofs with "sat.euf=true tactic.default_tactic=smt..."

#7250 SunHao-0 closed 3 weeks ago
2
Solving problems with formulas related to square roots

#7249 Heaven2024 closed 3 weeks ago
1
Performance on solve a logical problem about unexplained functions

#7248 Heaven2024 closed 3 weeks ago
1
rlimit fails to stop z3

#7247 hmijail closed 3 weeks ago
1
Segfault is triggered when push is before logic set

#7246 Heaven2024 closed 4 weeks ago
0
Non-deterministic correctness bug in QF_LIA optimization

#7245 mikand closed 2 weeks ago
0
Clear up inefficient code

#7244 CoolThi closed 1 month ago
1
is there an implementation available in the high level api for string variables/sorts in typescript?

#7242 uwesimm closed 1 month ago
0
Z3 proves `(= 0.0 (^ 0 (- 2))`

#7241 someplaceguy closed 1 month ago
1
Semantics of "box" for "opt.priority" optimization

#7240 mikand opened 1 month ago
2
Alternative solutions for z3-solver without using SharedArrayBuffer or COOP/COEP headers

#7238 MargeKh opened 1 month ago
0
reading string value from the output of z3 consequence API throws exception

#7237 chauhansantosh17 closed 2 weeks ago
1
Fix compilation error in column_info

#7235 waywardmonkeys closed 1 month ago
1
Timeout not working on z3 python in the second `s.check()` call

#7234 anirjoshi closed 2 weeks ago
1
aarch64 linux wheel is tagged `manylinux2014` despite actually being `manylinux_2_34`

#7232 burgholzer opened 1 month ago
0
Solver printing wrong model in C++ api

#7231 anirjoshi closed 1 month ago
1
intblast: fix translation of sign_ext

#7230 JakobR closed 1 month ago
0
Z3_solver_pop() does not clear ASTs

#7229 remysucre closed 1 month ago
1
Remaining deprecated `distutils` in Python scripts.

#7228 arbipher opened 1 month ago
0
Nlsat simplify

#7227 NikolajBjorner closed 1 month ago
0
Fix SLIBEXTRAFLAGS:Add LDFLAGS

#7226 shijy16 closed 1 month ago
4
Failed to build libz3.so because of missing `LDFLAGS` in `SLIBEXTRAFLAGS` when cross compiling z3

#7225 shijy16 closed 1 month ago
1
ASSERTION VIOLATION, File: ../src/sat/sat_drat.cpp

#7224 whangdo closed 1 month ago
2
Invalid model issue on String theory

#7223 whangdo opened 1 month ago
0
[Question]: z3 py in overflow checking for bit-vectors

#7221 hagozaebii closed 1 month ago
1
Empty universes

#7220 remysucre closed 1 month ago
1