Z3Prover/z3

Issues

• Correctness issue regarding `abs` in multi-objective optimization

  #7578 opened 3 days ago by merlinsun
  0

• Correctness issue on multi-objective optimization

  #7569 opened 3 days ago by merlinsun
  0

• Cannot get parameter of func decl of floating-point numeral expression

  #7522 opened 2 months ago by pclayton
  3

• Segmentation Fault (Heap-Use-After-Free) in Z3 when Parsing Invalid SMT2 Rule

  #7574 opened 3 days ago by chinggg
  0

• SMTLib 2.7 compliance: Bit-vector to/from Int conversions

  #7572 opened 3 days ago by LeventErkok
  0

• License of DLLs in Windows Wheels

  #7575 opened 3 days ago by hyandell
  1

• unsupported logic UFDTLIRA

  #7571 opened 5 days ago by huhuhu777
  1

• user_propagate_function not exposed in Python API

  #7570 opened 8 days ago by linusheck
  1

• z3 cannot simplify (v << 3) + 1 - (v << 3)

  #7546 opened 8 days ago by fkil
  2

• ASSERTION VIOLATION, File: ../src/smt/theory_lra.cpp Line: 3569

  #7567 opened 10 days ago by merlinsun
  1

• ASSERTION VIOLATION, File: ../src/util/vector.h Line: 912

  #7550 opened 11 days ago by merlinsun
  0

• z3 browser init can't work as directed

  #7556 opened 22 days ago by dberlin
  9

• Spacer: New bug after previous fix?

  #7566 opened 14 days ago by jena-kling
  1

• z3/spacer returning UNSAT for sat-instance

  #7505 opened 18 days ago by jena-kling
  9

• An error occurred while executing the following Python program. OSError: exception: access violation reading 0x0000000000000000

  #7564 opened 18 days ago by GEMINI1999
  1

• Z3 throws a segmentation fault when getting the model of a formula with algebraic datatypes

  #7563 opened 19 days ago by muchang
  0

• Stray lines left in commit

  #7560 opened 19 days ago by LeventErkok
  2

• Convergence regression

  #7561 opened 19 days ago by LeventErkok
  0

• Invalid model issue related to options

  #7549 opened 20 days ago by r0ayane
  0

• Compilation warnings

  #7559 opened 20 days ago by LeventErkok
  0

• Wrong result "unsat" for Spacer

  #7554 opened 20 days ago by jena-kling
  3

• Combination of (Quantified) Strings and Bools leads to unexpected unknown

  #7558 opened 20 days ago by neta-elad
  1

• Vandalized Link on Wiki

  #7552 opened a month ago by toolCHAINZ
  1

• segmentation fault when processing incorrect input

  #7541 opened a month ago by mikulas-patocka
  3

• Performance regression on stratified EPR formula

  #7515 opened a month ago by kenmcmil
  7

• Z3 hangs when checking large polynomial formula

  #7539 opened a month ago by houseofwealth
  3

• Wrong solution for subset and Bool Set

  #7544 opened a month ago by leuschel
  1

• The runtime of z3 is too long

  #7542 opened a month ago by frankeyjin
  0

• Incorrect result in optimization problem

  #7493 opened a month ago by merlinsun
  3

• regression with arith.solver=6

  #7502 opened 2 months ago by mtzguido
  4

• Nondeterministic behavior observed despite seed set

  #7525 opened a month ago by Eladkay
  9

• Slow unsat multiplication overflow solving

  #7526 opened 2 months ago by alph6
  1

• Z3 hangs when adding polynomial formula

  #7536 opened a month ago by houseofwealth
  1

• `produce-unsat-cores` affects convergence

  #7538 opened a month ago by mtzguido
  0

• Assertion violation in sat_integrity_checker.cpp:110

  #7532 opened a month ago by r0ayane
  0

• Spacer: Wrong sat-result due to name clash?

  #7521 opened a month ago by jena-kling
  1

• Z3 ignores errors

  #7528 opened a month ago by Timmmm
  1

• Head Broken - Unable To Compile src/ast/sls/sls_arith_lookahead.h - Missing `::sqrt`

  #7527 opened a month ago by ErrWare
  1

• Func decls for floating-point operators `+oo`, `-oo`, `+zero`, `-zero` and `nan` have no parameters

  #7524 opened 2 months ago by pclayton
  4

• `Z3_get_numeral_string` may produce sexpr format for floating-point numerals

  #7523 opened 2 months ago by pclayton
  0

• compiler error trying to build from source

  #7520 opened 2 months ago by houseofwealth
  1

• Probleam in Rust version "mul" and "mul_towards_zero" function

  #7513 opened 2 months ago by FoxMakarov
  2

• Z3Exception: b'mbp to-real'

  #7517 opened 2 months ago by houseofwealth
  1

• python: load libz3 with soversion

  #7518 opened 2 months ago by sertonix
  0

• Named annotations appear in model generated by `get-model`

  #7499 opened 2 months ago by edwardcwang
  0

• Setting `smt.mbqi.id` causes result to switch from `unsat` to `sat`

  #7510 opened 2 months ago by ole-thoeb
  0

• Parallel in z3 to speed up?

  #7511 opened 2 months ago by XiangyuG
  1

• SAT check on an `ite` returning an unexpected `unknown`

  #7507 opened 2 months ago by PetarMax
  6

• Alpha-renaming causes convergence issues

  #7494 opened 2 months ago by LeventErkok
  1

• Equality test between a Bool and a Real throws an exception

  #7501 opened 2 months ago by houseofwealth
  2