z3-4.10.0

4.10.0 release

Changes:

• 9cd3b9c Merge branch 'master' of https://github.com/z3prover/z3
• adcb3e8 set version number
• 59d47e3 don't publish pypi yet
• efa74fe fix #6180
• cf5a8fd fix validation code for pb
• a66095b fix the path to ../build/z3-built
• dc95659 did I mess up wasm paths in jest - or not?
• 3700822 did I mess up wasm paths in jest?
• 32c0d1f fix #6168
• 7f983e7 fix #6174

See More

• 3261472 fix #6176
• 1b83a45 fix #6178
• 5b219aa add mutual recursive datatypes to c++ API #6179
• 2e13c0b add API and example for one dimensional algebraic datatype #6179
• 81cb575 simplify
• 2e52029 add command-line overwrite capability to setup.py
• 2c8df54 enable fresh for python wrapper for user-propagator
• 914cfca updated release notes
• 111d27c remove dependency on pragma
• dead0c9 reverting relative path
• afcfc80 the relative path seems out of sync with how it is set up in node.ts
• 7f1893d add missing MkSub to NativeContext
• 7ded856 script to test jsdoc
• 393c63f fix #6114
• 527914d update documentation to use latest conventions
• b5a89eb add missing generation of z3.z3 for pydoc and add some explanations to logging function declaration
• 95c3dd9 Added missing decide-callback for tactics (#6166)
• 6e5ced0 optimizations to api ctx ref counting
• eb2ee34 fix typo
• aefd336 set OCaml default behaivor to enable concurrent dec ref #6160
• 6c5747a guard against lemmas that are already true
• 4ecb61a neatify
• b743e21 give java dynamic lib a chance for extra flags for #5848
• 2696775 remove stale assertion
• 6688c1d prepare for #6160
• b29cdca integrate factorization to Grobner
• 7c17758 add propagators to grobner
• af80bd1 Flush the trace stream before displaying sat results (#6162)
• 2f5fef9 Cache param descrs when modifying solver params (#6156)
• 4a19285 add var_factors
• 981c82c fix initialization order
• 894fb83 fix build break (debug assertion) and isolate gomory functionality
• b253db2 redundant parenthesis
• dec87fe fix issue with set-logic for eval_smtlib2_string
• 1378e71 fix #6157
• a3eb9da fix #6158
• 8e23af3 fix build
• b81f70f split nla_grobner to separate file
• 7d0c789 propagate has-length over map/mapi
• 8900db5 add diagnostics for grobner
• ca80d99 fix #6153
• 43cf053 fix #6128
• faf6c02 remove --js from nightly and release doc builds as the npm run 'check-engine' fails
• d5779bf handle trivial equalities in simplify_leaf
• 4dc88f0 add --js to nightly and release scripts, nb @ritave
• 2e79704 remove space
• 316ed77 Tune Grobner equations
• f33c933 Add substitution routine to pdd
• 5c54d65 fix #6143
• 8b29f40 Fix build on Mac (#6146)
• 49b7e90 Merge branch 'master' of https://github.com/z3prover/z3
• 7ae1a33 parallel-tactic: fix deadlocking race between shutdown and get_task (#6152)
• 99212a2 Use int64 for ocaml api functions that require it (#6150)
• 1f23460 Fixed missing assignment for binary clauses (#6148)
• 9dd529b missing initialization of List for cmd interpreter
• b68af0c working on reconciling perf for arithmetic solvers
• 9d9414c inc version number
• 0c42d3b small format update

This list of changes was auto generated.