z3-4.13.2

4.13.2 release

Changes:

• 9a8ff74 update version number and release notes
• 11bb19d make default tactic cases lazy
• 40b0210 fixes to lazy tactic uses
• 01cf042 fix #7404, relates to #7400.
• d047b86 pypi publish
• f4452a0 pypi publish
• 3df7299 update signature of operator==
• 649c36a align nightly and release yamls
• 8d831a1 set to macos latest
• b39bcd6 remove ubuntu20

See More

• ebdb037 fix indent
• c690279 skip pypi publish during dry run
• 77aa528 wasm: increase timeout in tests (#7401)
• 103c5ad wasm: attempt to GC in tests (#7400)
• 82eb186 remove ubuntu build 20 from nightly
• eb5d036 fix #7392
• 2655301 comment out simple proofs unit test
• 8b81bda Julia now used the C API. (#7388)
• 994056f C API now used by Julia. (#7387)
• 716a815 update lock file
• a831fe9 fix some build warnings
• afaa48d sample fix script
• fa1a2cd disable simple check in nlsat
• c34c847 Add .gitattributes for genaiscript and update git commit flow script. (#7396)
• ec14ef7 Update Ubuntu job name in Azure pipeline and add string variable creation in C API example
• 95d2e00 Update OCaml jobs to use Ubuntu-latest in Azure Pipelines configuration
• 0604d23 Check if model_converter is non-null before initializing values in sat_tactic
• 5a6dc18 Override convert_initialize_value method in bit_blaster_model_converter.cpp
• 5c58329 Remove unnecessary const qualifiers from comparison operator overloads in z3++.h
• ee34773 remove junk
• eb8c630 Refactor and fix uninitialized variables and improve function consistency across multiple modules
• 499ed5d remove unneeded iterator functions
• 737c220 delete more default constructors
• 4b4a282 Add const qualifiers to comparison operators and update iterator equality checks in various classes
• a62fede remove a few default constructors
• 22d9bfa fix warning with iterators due to non-const comparator
• 1121815 Standardize C++20 flag across different platforms in build script
• 1e580a7 update to c++20, remove debug output
• 96c1375 #7391
• a9f8ec1 updated handling of value initialization for bit-vectors
• ba5cec7 additional rewrites for bv2int
• fa7fc8e Refactor bv_rewriter functions using unified variable assignment and early break logic
• d66609e fix #7389
• 0c48a50 Add support for initializing variable values in solver and optimize contexts in Z3
• 342dccd correctly process cancellation in gomory cuts
• b99c4a4 Add override specifiers to methods in set_initial_value_cmd class for clarity and consistency
• 8349ee0 Add support for const array in all logics as per issue #7383
• 4896edf Add tracking of values size in scoped_state push method in opt_context
• a3f35b6 Add command to set initial value hints for solver in various components
• 1c163db remove output
• 0f89650 Add initial value setting API for solver and optimize contexts and update related function signatures
• 48712b4 Add initial value setting for variables in Z3 API, solver, and optimize modules
• 0ba306e y
• 99a9a4a fix #7372
• 1ace3d0 fix #7372
• 8061765 remove default destructors & some default constructors
• 0837e3b Fix nightly (#7365)
• 5237e7d Adjust memory reallocation to consider SIZE_T_ALIGN in memory_manager
• 6086a30 Add reference URL to GenAI script file for auto Git commit guide
• db4176a #6902
• ef58376 replace a few old-school constructors for a 0.5% reduction in code size
• a3eb2ff revert update to vector for testing #6902
• a1bcf13 fix build
• 01a4195 #7362
• 9a87bb1 #7362
• 46d602e update gitignore to prepare for genaiscript
• 84b2c21 Update nightly.yaml for Azure Pipelines
• dcdb7c4 wheelhouse
• 96417d4 Update nightly.yaml
• 59853d0 Update nightly.yaml
• c79477a update nightly
• ea93f07 Update azure-pipelines.yml
• cd89867 add back auditwheel
• ea417bb Update README.md
• 954dddb retain pip install build, remove audit
• 5360656 fix expected
• 0bf3eeb Bump docker/build-push-action from 6.6.1 to 6.7.0 (#7350)
• f6dbaee adding to nightly
• e1f1d67 New python packaging and tests (#7356)
• 349ebd0 #7344
• 84da614 make gcc linting happy
• b84b4e7 fix attribute order
• 49ba3bc address compiler warnings gcc-13
• cff1e92 Avoid broken stack at few places (#7353)
• 6a68cc5 #7353 - clear pointer when existing stack
• c1454dc Fix building with Windows SDK and Clang-CL (#7337)
• 0612a0b Bump docker/build-push-action from 6.5.0 to 6.6.1 (#7338)
• 6565455 fix #7343
• ed17de5 fix #7343
• 83f47bd wasm build problem
• bf34600 add release nodes and add the author reference in qfnra_tactic
• f2d35dd more cleanup
• 8999e1a use standard name conventions and add file headers
• 33f0256 cleanup
• 752c999 cleanup
• f81303f delete unused nlsat_symmetry_checker
• f7905a5 remove printouts
• 518a8b2 fix the build
• 4b3a06a port hybridSMT
• 1a5bddb port more from hybridSMT
• 209366b cleanup porting comments
• 839594a remove option look_for_0_witness
• 0306eff port look for 0 witness
• a09e412 cleaning up
• 6ce0fcd port sample cell projection
• 3e518b9 fix #7331
• 26b8d63 add max conflict throttle to SAT based QFNIA tactic #7329
• 52f8eb2 #7255 #7328
• bc8fa67 #7255 #7328
• d6040ee do not copy artifacts from CI pipeline
• 51fcb10 shave some overhead from fingerprint hash function #7281
• 7c30cbf add scoped_vector invariants and unit tests (#7327)
• d2fc085 update heap unit tests (#7324)
• fce4b36 add apply_permutation tests (#7322)
• ea9fa17 add static
• 23e7dc0 assert -> SASSERT
• fe59461 fix dlist tests (#7323)
• 6ba25b8 add permutation unit tests (#7300)
• e7382d6 Added "λ" pretty printing to python (#7320)
• 0c16d34 fix #7292 (#7316)
• 5fcc50f Revert "add scoped vector unit test (#7307)" (#7317)
• 2ae3d87 add scoped vector unit test (#7307)
• 2ce89e5 Gcc 15 two phase (#7313)
• 25e683e fix finalize method
• ac7014a expose public
• f94500c fix #7309
• 5f6bb3d fix #7311
• 1e6b137 Bump docker/build-push-action from 6.4.0 to 6.5.0 (#7304)
• b535509 remove crashing test
• 2013cd1 Update coverage.yml
• 966c9a3 Revert "new heap invariants (#7298)" (#7303)
• 3d014f8 add new hashtable unit tests (#7297)
• 49dc1bb add new permutation class invariant (#7299)
• 5003d41 Revert "New invariant for dlist (#7294)" (#7301)
• 80ac7b3 new heap invariants (#7298)
• bc636d7 new hashtable.h invariants (#7296)
• 08b6338 fix signature
• 458d8b0 remove wsp
• 9803e9e unit tests for dlist.h (#7293)
• cf4d0e7 New invariant for dlist (#7294)
• 9073da4 Bump docker/build-push-action from 6.3.0 to 6.4.0 (#7289)
• a2c3ce5 Bump docker/build-push-action from 6.2.0 to 6.3.0 (#7280)
• b006901 add new ema invariant (#7288)
• 374609b kludge to address #7232, probably superseeded by planned revision to setup/pypi
• af1f0e3 fix #7268
• 6e069c1 remove macro distinction #7270
• 18b6087 trigger the build with a comment change
• 1da1320 Fix a comment for Z3_solver_from_string (#7271)
• facc7d8 Bump docker/build-push-action from 6.1.0 to 6.2.0 (#7269)
• 8de2544 set clean shutdown for local search and re-enable local search when it parallelizes with PB solver
• b2b3bab Bump docker/build-push-action from 6.0.0 to 6.1.0 (#7265)
• 8e482df fix #7264
• c137ef7 disable publish and signing
• abea0b7 disable publish and signing
• b5c3a6a skip signing
• 4ca59c5 update to macOS-latest
• 2654d80 revert nightly to 2_28 manylinux
• 3bf2b3f fix #7260
• 223b65b Bump docker/build-push-action from 5.3.0 to 6.0.0 (#7257)
• 758d886 Bump braces from 3.0.2 to 3.0.3 in /src/api/js (#7261)
• bf3615d fix lemma logging in nlsat
• e4b3df2 remove unused column_info.h
• c0b4d02 update containers for Python, first steps to address #7232
• ef86f5f add partial evaluation cases for algebraic data-types for recursive functions.
• 81ebd52 #7207
• 972d352 reshuffle priorities on multiplication allow non-determinism.
• 01e47bf fix #7245
• a6b5027 fix #7252
• 35c1cac fix #7248
• b831a58 fixes to #7250
• 49610f5 fix #7246
• 770c51a add m_replay_qhead to the trail
• c0a7af4 fix bugs with tracking premises in user propagator in sat/smt
• 904a50f Fix compilation error in column_info (#7235)
• e454ae2 intblast: fix translation of sign_ext (#7230)
• 18a95d8 fix assertion failure when printing stats
• cb50dca fix #7229
• 552068a let the replayer stop when it encounters a C command with invalid args
• 8fe357f Nlsat simplify (#7227) [ #7219 ]
• e036a5b add parameter validation to ternary and 4-ary functions for API #7219
• efc8932 add abs function to API
• b120745 add C++ bindings for sequence operations
• c7529d0 expose fold as well
• fc6c4c9 initial warppers for seq-map/seq-fold
• f9176fb Update README.md
• 8f4ffc7 add logging for first conflict
• 2f02278 add virtual destructor to z3::object class
• 19eb722 add virtual destructor to z3::object class
• 231a985 add virtual destructor to z3::object class
• 04c55c3 fix unsoundness bug
• 869643a fix memory leak
• 1ef4354 fix build
• aa1a596 add doc-string
• 29e724f add gc to lemmas, convert bounds constraints to lemmas, add simplification pre-processing beyond equality extraction
• b0222cb temper warning messages from uninitalized pointers
• 4c070f9 add extra fields to nlsat-clause
• 39dc886 expose comparisons with polynomials, incremental way to extract variables
• bc577b9 refine precision before taking closest integral value.
• 2ad9f22 add logging
• bebcd94 enable logging nla lemmas
• 2a4f0e7 tidy
• cbef183 type check equality injectivity axiom
• e184a9a fix translation of bvudiv
• 0368b52 add missing expr
• 2682c2e sls updates
• 43dd6a5 include mutex
• c0bdc7c enable concurrent sls with new solver core
• 510534d cleanup
• 974ea7b maintain ownership of dependency
• 7b8980f fix regression introduced when testing
• 8d0e66b fix regression introduced when testing
• 9a681b1 reorg sls
• bab7ca2 fixes to bv-sls
• d7c0e17 fixes to tighten-range
• 2ce202d add special handling of lshr, ashr
• 918ac2b fix #7196: make the code C++23 compatible
• 84092cb add engine-init to control model transfer
• 51f1e26 updates to sls
• 111fcb9 Implement API to set exit action to exception (#7192)
• c18a42c change signed projection to include root object.
• 80642e5 Add check for libatomic requirement to Python build system (#7184)
• 648e057 #7178 copy build tool chains used for manylinux arm64 into ubuntu builds
• 6455de9 fix #7179
• 530c6fc fix ##7175 - don't add user macros/functions when smtlib2_compliant=true
• 27a9b8b fix project minor version
• f840d5d na
• 70d2263 cast, updated nlexplain
• 730f9ad Nikolaj's fix in add_zero_assumption
• a9054bc fix warning C4244 in util.h (#7171)
• 1a74371 Bump docker/build-push-action from 5.2.0 to 5.3.0 (#7170)
• 1836590 Update util.h (#7169)
• b8a6998 fix #7165
• 6450a7a Bump docker/build-push-action from 5.1.0 to 5.2.0 (#7159)
• 5704e8d fix intblast is_bounded (#7163)
• 0b3bbc2 #7158
• 7bbe3fb fix (get-proof) command to respect option pp.simplify_implies (#7157)
• 361e04a port fixes to intblast
• dcaacf5 add rewrite glue for instantiating equalities, #7154
• a4ecaf1 increment version number

This list of changes was auto generated.