2 Releases published by 1 person

• z3-4.13.4

  published Dec 17, 2024

• Nightly

  published Dec 18, 2024

1 Pull request merged by 1 person

• Optimize expr_safe_replace for quantifiers when all source patterns are vars

  #7481 merged Dec 19, 2024

2 Pull requests opened by 2 people

• Add 2 new API functions to get depth & groundness of exprs

  #7479 opened Dec 16, 2024

• Support BitVectors in the TypeScript Optimize API

  #7480 opened Dec 17, 2024

8 Issues closed by 2 people

• Java api: the call to com.microsoft.z3.Native.INTERNALdelContext(Native Method) never ends

  #7455 closed Dec 21, 2024

• Why Can't (V & 65535) >> 15 Be Simplified Further in Z3?

  #7460 closed Dec 21, 2024

• Unexpected `unknown constant in0` Parse Error When `parse_smt2_string` Contains No Reference to `in0`

  #7490 closed Dec 21, 2024

• z3 does not turn (<= (+ (ite foo1 1 0) ...) n) into at-most n

  #7483 closed Dec 21, 2024

• Segmentation fault with Z3 in Python on Cygwin (reprise)

  #7474 closed Dec 21, 2024

• TS/JS Bindings - Poor documentation, inconsistent API, ADTs?

  #7486 closed Dec 20, 2024

• Segfault with sat.smt=true, quantifiers and cardinality constraint

  #7485 closed Dec 20, 2024

• Equation ordering is sometimes swapped

  #7476 closed Dec 18, 2024

4 Issues opened by 4 people

• smt.relevancy=0 produces wrong result

  #7491 opened Dec 21, 2024

• Z3 returns incorrect 'unsat' in QF_NRA logic

  #7489 opened Dec 21, 2024

• z3 hangs on query involving maps and bitvectors

  #7484 opened Dec 18, 2024

• NuGet package does not include the API DLL

  #7482 opened Dec 17, 2024

2 Unresolved conversations

Sometimes conversations happen on old items that aren’t yet closed. Here is a list of all the Issues and Pull Requests with unresolved conversations.

• ASSERTION VIOLATION with z3 version 4.13.3.0

  #7478 commented on Dec 21, 2024 • 0 new comments

• Fatal Runtime Error when run java

  #7472 commented on Dec 21, 2024 • 0 new comments