z3-4.8.15

4.8.15 release

Changes:

• f1806d3 remove buggy code, close, fix #5825
• 1e8bae0 enable pypi in release pipeline
• b4873d2 fix #5907
• f053daa fix #5906
• bbb2777 ensure that objects in callback are of sort Ast.
• 3439d24 Revert "doc: update readme (#5898)" (#5905)
• 9061ca5 call it macOSBuild
• b5b9c85 call it UbuntuBuild
• dfa6544 fix name for artifact
• 964e513 re-add bv_eq_axioms, fix #5842

See More

• cfe02ed remove stale return
• fd1f5cd fix callback type declarations for propagators
• eaa2fb7 update release pipeline with x86 Nuget
• 86af723 remove left-over debug output
• 6d836e7 expose model update
• a9d7026 add note about transform
• 81a5e56 publish to github
• 39df8ee update win build
• 669a1d6 na
• 29e2883 pre-release pipeline
• 6010d75 fix #5903
• 41d1c34 remove else case
• 1fa373d old bug: unit of xor is false
• 4e0a2f5 Dispose of intermediate Z3Objects created in dotnet api. (#5901)
• bdf7de1 Care for root index being undefine while calling Z3_algebraic_get_i() (#5888) [ #5807 ]
• 6455ae4 Merge branch 'master' of https://github.com/z3prover/z3
• 0b230ee move some functions to using var pattern #5900
• 6c4780a Update cross-build.yml
• 3d87d86 github action: add riscv64/aarch64/powerpc64 cross compile (#5897)
• a151725 call dispose on sorts #5900, missing charSort
• cd5e114 call dispose on sorts #5900
• cb9dcb7 add regex power to API and for Java per request
• e1929ca add regex power to API and for Java per request
• 706d7ea native context uses legacy mk_context
• 313b87f doc: update readme (#5898)
• 545341e fix #5895
• c51ca86 add another constant folding case
• e839e18 minimal addition to rewrite bit-vector to character conversion using constant folding.
• 8f2ea90 Merge branch 'master' of https://github.com/Z3Prover/z3
• 081c62d allow range comparison for bit-vectors and int/real
• 580012e fix #5894
• f26c12a fix #5882. Use model true when inlining (#5892)
• 8e18a94 Update README with info about Smalltalk bindings (#5893)
• 43f7636 remove some copies/moves
• 1d224d1 na
• c6f8ee3 na
• 3293aeb na
• e7ded9c update to 2022
• 97c7ce6 Clean up build warnings (#5884)
• e3568d5 Handle additional cases in rule_properties::check_accessor (#5821)
• 882fc31 doc strings
• b0c0f4d fix #5876
• 3e51b69 no fun!
• 2b71d8b doc macros
• 87e6f10 commenting
• 676ba78 fix else case: it is first argument of const array
• 35d26bc NativeModel: TryGetArrayValue (#5881)
• 248a367 na
• e1e8d15 stub out array serialization
• cd324a4 na
• 8d1276f using directives
• 35fb956 Updated user-propagator example (#5879)
• a08be49 NativeContext, NativeSolver, NativeModel - updates for Pex (#5878)
• 811cd9d add example
• ee18c50 add stubs for injective function axioms, add some parameter functions
• 757cf76 sketch ArrayValue, add statistics
• 80506df sketch ArrayValue, add statistics
• bf14aeb stub out nativesolver
• bbadd17 fix #5874
• 5f79a97 use conventions from Context
• c812d1e update native func interp
• 61d2654 quantifier
• deeb5e9 finish NativeModel
• c0826d5 add stubs for native model and func interp
• deaad86 nit
• 2b6dadc fix #5869
• 302c0d1 fix #5867
• 412b050 User-functions fix (#5868)
• 689e2d4 remove a bunch of unneeded memory allocations
• 7f149a3 refining model update rules for del_rule #5865 #5866
• 30a2f2f initial stab at NativeContext
• f2e712b throttle is_compatible to check variables at most once
• 7b4f1ed missing initialization of m_user_propagator, disable unsound in-processing in pb_solver
• dc110f1 Update mk_util.py (#5864)
• 6be0a66 fix #5863
• 6af170b fix #5861
• c2f1bdc fix #5862
• 11030fc disable unsound mk_seq_butlast
• ea0876b add lambda definitions during ast translation #5820
• d06c51d na
• 061e94d #5858
• e8d4804 Revert "use horn_subsume_model_converter in coi filter (#5844)" (#5859)
• 456b8ee nightly
• c47e5af multi
• cfe9846 multi
• b843618 fix #5798
• 5c26249 #5849
• 1e46395 #4889 avoid double internalize of bvle
• b38b6da add option to disable FPMATH
• f66b4f0 fir #5856
• 14ee021 nightly
• e800269 na
• d0d4ab7 #5820
• ff5d210 na
• c25d710 try out arch arm64 on the mac
• 4d184fe skip expensive equality rewriting of Booleans
• 10b611b fix #5850
• 91045d3 two words
• 9a1a728 Add str.<= and str.< to Java API
• 7091b1c add additional regex operators to API
• 2e00f2f Propagator (#5845) [ #5818, #5835, #5829, #5843 ]
• 2e15e2a Add access to builtin special relations (Context::mkLinearOrder and Context::mkPartialOrder ) to Java API (#5832)
• 9cf5076 fix compiler warnings under clang (#5839)
• 09da87d use horn_subsume_model_converter in coi filter (#5844)
• 5bbb8fb add bail #5825
• 33985eb update expected
• 6202cd5 fix #5842
• aa6ec41 move idiv test to after cuts/branch
• 9a4d6ce overhead with push-ite on shared terms
• 3d26b50 fix #5827 #5828
• d745d03 switch to vs 2022
• 81e94b2 na
• 07d02ea fix #5829
• 4f6fcf8 fix #5814
• 0059e88 fix #5808
• 9958cab fix #5808
• 3f3d058 extract also units from search state
• d4ea67a Fix a few typos in README (#5782)
• 03ff320 block recursive definitions with lambdas until they are properly supported #5813
• 1c10ce4 #5815 - surface multi-arity arrays over python API
• 8a84cac add tuple support for getitem #5815
• e9dad84 update documentation comments
• 9d655cc track all unhandled operators instead of latest
• 4749495 Merge branch 'master' of https://github.com/z3prover/z3
• 05e28e4 fix #5812
• 6a412f7 allow to pass Booleans as arguments to arithmetic expressions
• 994c7ef format
• 1e0d495 call mux finder
• 4392b88 return negated literal when expression is "not"
• 7ddfc54 shortcut negation
• f3fc6a5 formatting
• 6422b78 fix mux extraction to check for top-level assertion
• 62bb234 expose extract roots as separate
• a326ad4 flag incomplete on lambdas #5803
• a189ca8 truncation directive #5805
• 773e829 #5804
• 913b90f fix #5802
• 2551631 mul overflow #5797
• 5e81c12 #5797 probably still wrong wrt underflow.
• 9e5b6e0 #5778
• 4da930b #5794
• a621041 fix #5795
• 461e710 fix #5792 again
• 53f72d9 updated mini
• c6539de fixing null check
• 435f79e tup
• 9294b2c created
• 3de9d37 fix overrides for created_eh
• bf6454d throw error if created-eh has not been registered
• ea68275 add missing callback to m_created_eh
• f639a7e add marker for top-level expression in rule.
• 61ab72b fix #4869
• 3b8c0b7 fix #5791
• 20f9814 fix #5789
• d02235f #5778
• 85f6456 Add missing constness (#5787)
• 9969809 #5778
• a1f7676 remove assertion - literals could be assigned but propagation incomplete
• 007af9c fix #5784
• 1728084 added comments to explain #5781
• b1ff4bc no normalize
• 75a81af fix #5786
• af9ae35 term
• c527fda term
• f1a302b term
• 7a8c969 ensure b_internalized
• a3d4e9a adding created to sat/smt
• c00591d finish is-fixed
• e5767bf na
• 0f03ef4 for Clemens: ensure fixed values are propagated after registration
• 5b03896 #5780
• 06feb71 fix bug in root setting exposed by incremental mode pb_solver
• 36cfb88 add preliminary stub to handle closure types
• d777306 #5778
• fcc9f37 #5778
• a15da8f #5778
• 637ddf9 fix #5777
• 0dd5a5e #5777
• a48d3fd #5777
• ea93345 #5777
• cd56d55 #5753
• bc9c6ad #5753
• 1b5f7cd na
• 17cfc1d #5753
• 74824ac #5753
• d09abdf fix #5771
• d5cc162 bug in bounds
• 2363bfc internalize arithmetic sub-terms #5753
• e816946 handling unsimplified input
• b259f46 dependencies
• 4b6679e #5753
• 366cd9b missing pb cases
• dfe2b27 #5773
• 0720998 #5753
• 10dc8d7 #5753
• 56d3718 add simplification with qe-lite as an option #5767
• 08294d6 separate dependencies for qe_lite
• 2bcc814 add macro to track closures declared in z3_api [ #5762 ]
• e5eaea4 ensure m_true is assigned #5753
• dbd5512 ensure enode without recursion
• 0557324 ensure enode without recursion
• 571a74c counting function applications #5766
• 4cd818b #5766
• d3bc11d bvs have to be expressions
• 21feefe Add character access functions #5764
• 2b934b6 Add WebAssembly/TypeScript bindings (#5762)
• 9ac57fc update version number for next release
• f1bf660 add case for abs (normally simplified, but not with default_tactic=smt).
• 671d071 #5753
• 010bccf Update wasm.yml
• bf3c213 #5753
• 90fd3d8 enable propagation
• 9f9543e Fix unused variable warnings. (#5760)
• 174889a id
• afbfea8 name the package
• 36ed1ff update name of artifact
• 40761eb bug in script
• c2aff52 os-info back to common
• d391043 only one arch at a time
• ef48107 make static features avoid stack #5758
• 2c44454 self -> env
• d6ce050 try separate x86
• 6013d5d #5755
• 0bc8518 na
• 199daea remove Z3_bool_opt #5757
• 7baa4f8 build failure
• 2be71cf #5753
• 6a3fe51 build
• 592b1d7 #5752
• d14f00d with no last model
• dadda86 #5751
• 130a0c4 resurrect infinitesimals from maximization function #5720
• d7c7fbb setting roots breaks relevancy propagation
• bd8de96 more fixes on relevancy
• 5ec7a66 change class name, add comment
• 964a5cd lump java together
• e943bee apply delcypher's todo
• ef3dd32 some cleanup
• d1fb831 relevancy overhaul
• 4a19750 cleanup

This list of changes was auto generated.