z3-4.8.13

4.8.13 release

Changes:

• feadfbf enable publish
• 41a5b93 update release notes
• 5351640 Fix stray semicolon in examples (#5669)
• 5194aa1 nightly
• 1752055 update nightly
• c826b64 prepare release
• b6f7dea fix #5663
• 3c16edc check for v1 == v2
• 63ac2ee #5614 turn on / off options to get better performance.
• b28a801 #5653

See More

• b5deba8 add EFSMT solving example (#5654)
• 3a9656b fixing issues with user propagator from python
• f2fcbc7 capture values not reference
• af2cc46 #5646
• dd1e0fc #5643
• 091079e Added user propagator example (#5625)
• 87d4ce2 working on #5614
• a94e2e6 build warnings
• 036b38a ubuntu 16 is no more
• a11ca1a Update wasm.yml
• 8e59b34 Update README.md
• 933bb4f Update wasm.yml
• dfba177 Update wasm.yml
• f61e6ab Update wasm.yml
• f83226d Update wasm.yml
• fe0e1cc Update wasm.yml
• e7a54db Use emscripten to create a wasm build (#5634)
• d1fbf01 Update azure-pipelines.yml
• 96671cf Add and fix a few general compiler warnings. (#5628)
• 1d45a33 fix one typo and two misunderstandings for doxygen (#5633)
• d1592c6 fix misspelled \brief for doxygen (#5632)
• 780761a Create wasm.yml
• 4dad414 fix performance regression after adding user declared functions to model
• f5f35f8 fix grouping for latest doxygen (#5626)
• 723b755 Fix the command of install_name_tool -id. (#5622)
• eb8c8da ex handler
• 125eae0 #4869 load datatype parsing for HORN logic
• 61eb8d1 add ref for regression
• aa5b4b8 strengthen contract for log_axiom_instantiation #5621
• bdecc25 strengthen contract for log_axiom_instantiation #5621
• efcad5f fixed nullability bug in the if-then-else info (#5620)
• 4cfc737 update build
• 075769c try get_string contents again
• 45681b4 update API type annotation to make it OCaml friendly
• 3036b88 support threading for TRACE mode
• 4b7c08d Update azure-pipelines.yml for Azure Pipelines
• 09bda6f Update azure-pipelines.yml for Azure Pipelines
• cd4481b Update azure-pipelines.yml for Azure Pipelines
• ec9498e Fix ocaml link and load (#5618) [ #4840 ]
• 0660765 Add post-install testing for ocaml binding. (#5617) [ #4840 ]
• 3a3cef8 #5615 - update documentation and use non-encoded versions for ASCII characters in get_lstring
• 7f41d61 use some suggestions from #5615
• 0516163 remove deprecated escape string from Julia bindings
• cd8d8bb Fix runtime search path for shared-lib and add '-static' to the name of static-lib. (#5616)
• f05ac8a updated C++ API for escaped and unescaped strings #5615
• 05e7ed9 add API to access unescaped strings, update documentation of Z3_get_lstring, #5615
• 6eed885 print bounded terms for better efficiency
• 13da6a0 add handling of quantifiers #5612
• 839a085 Merge branch 'master' of https://github.com/z3prover/z3
• 86147d0 #5605
• f9dde2e #5605
• 3557e0b Added eq/fixed/final functions in C++ user propagator as methods (#5607)
• fc3a701 push-pop
• d5e5dcf add nff and auto-relevant
• bc2020a #5604
• 115203e fixes to sat.euf ematching #5573
• f78546c fixed bug of computing butlast of a sequence (#5602)
• fb9fa1b updated printer
• cb120c9 Regex range bug fix (#5601)
• 6302b86 tweak GC in OCaml bindings (#5600)
• f60ed2c #5591
• 7b34131 #5593
• fd77f0c fix #5594
• 96e117d Update smt_context.cpp
• c15968a fix #4901
• 9a76bf0 #5591
• 58fd4fc Merge pull request #5550 from wintersteiger/cwinter_fpa_fixes
• 52032b9 #5467
• b471ebd Revert "Fix off-by-one in fp.div bit-blasting. Inspired by #4841 but doesn't quite fix it."
• 738783a Fix off-by-one in fp.div bit-blasting. Inspired by #4841 but doesn't quite fix it.
• c24f438 Fix for mk_to_fp_float; pertains to #4841
• 00e8ea7 Make terms that are internalized on the fly relevant
• 8e69f76 Add additional equality in theory_fpa
• f1acc4b Make fpa2bv debug symbol names optional
• 515a2a7 Whitespace
• e8d6d97 Refine fpa_decl_plugin::is_unique_value
• 12c3266 Fix error messsages
• c3549ec na
• 73102cf fix #5589
• 75702c3 na
• f7a2d08 Update README.md
• 88c3119 Create android-build.yml (#5588)
• 0fc9f1d fix max/min length to handle concatenation
• f1b8376 Rename 'user' to 'user_solver' #5586 (#5587)
• bfa960c fix internalize regression
• 6f55971 Newderiv (#5585)
• 146f462 Updated regex derivative engine (#5567)
• c0c3e68 disable all propagation until ematch incompleteness is fixed
• 94cc4ea remove arith_lhs simplification from preamble tactic
• 33f4e65 redo bindings/fingerprints
• 281fb67 unit propagate with fingerprints
• 8a85cfd fix #5579 -
• cbe7dd4 missing continue fixes unsound sat result from #5573
• ff723f1 Update z3++.h
• 62fd22f disable macro finder tactic if there are recursive functions fix #5574
• 137e5c5 fix tmp_eq
• 67ae75b fix tmp_eq
• da124e4 tune q-eval and q-ematch
• 92c1b60 tuning eval
• 2e176a0 count lazy bindings
• 3abecc3 add extra commands to API parser
• 6c71baf lifting iff to binary
• 1dcbd2d Correct capitalization of package (#5569)
• d174f87 #5532
• 18d1b36 #5532
• cabd5b1 #5532
• de20bff import goodies from ps
• 708602d fix #5560 - add a throttle on maximal size of bignums created for propagate-value lemmas
• 2e96557 fix #5560 - add a throttle on maximal size of bignums created for propagate-value lemmas
• 2c266a9 #5545
• 1352aa0 #5532
• 0170f1f #5532
• fd79908 fix build
• 6f31d83 fix #5541
• 4263063 CNF conversion refactoring (#5547)
• 91fb646 Fix Z3Config.cmake.in when generating a static library (#5555)
• d36c3fa #4880 add interpreted versions of to_bv functions for MBQI quantifier models
• 1fc7b63 ...
• cef964f fixes for model converter default case
• fe3f139 na
• c3c5c14 prepare for min/max i
• 50375df enforce idempotency
• c58b2f4 Added character functions to API (#5549)
• 9aad331 #5546
• f13ccf8 bv2char and char2bv with Clemens
• 34f878f make it easier to debug parallel
• 3e6ff76 fix regression bug in mam reported by Aseem
• 47fdd6c Added 16 bit string-encoding (#5540)
• e70f501 handle potential extra nodes from q_solver
• c4d0ded #5532
• 8c406c1 #5532 add blocking condition for recursion.
• 9341574 left over bugs #5532
• be4df46 #5532 remove unsound rewrite rule that was recently added
• 72f6271 #5532
• 3764eb1 #5532
• 3021da8 #5532
• 9c91698 #5532
• 976c0a3 revisit as-array evaluation
• 38b82fa const rewriting revisited
• 051ede6 #5532
• 3de9162 handle null more gracefully
• 9c5ef79 #5532
• 18e4546 modernize parameter defaults
• cdcfbeb #5532
• 0ddbbe9 #5532
• 5633af7 #5532
• a566c73 #5532
• 87f5b92 #5532
• c4158eb #5532
• 20a259c throw less #5519
• af5c6e4 #5528
• 55285b2 make it easier to iterate over arguments of an application
• e9a4a9a merge
• edb26e7 Merge branch 'master' of https://github.com/z3prover/z3
• 02acc38 add extra checks that user-supplied assumptions are asserted
• e05ef8e account for updating scoped state by goal2sat #5528
• f4abe3d #5528
• 9e306e3 more useful diagnostics
• 968717a follow on fix from #5528
• 6907d30 #5528
• a74c01c #5528
• cf9e55f #5516
• ba68fba build
• 0c53c13 add to_string method to make it easier to use without <<
• 7ce4be8 #5528
• a7bc471 fix #5526
• 8bdc8d0 Update solver_subsumption_tactic.h
• a3ba4e1 #5528
• f91c3d9 round-tripping escapes, again #5519
• 90f98d5 fix part of #5519
• 7c782a7 #5518
• 1426390 #5518
• ab2baa7 #5518
• 34c8f59 #5518
• 07bbd02 #5518
• 0b063f7 #5518
• 535f442 #5518
• cd2701d fix the use of ctx in Q() (#5521) [ #4956 ]
• 148cb83 #5482 fix default case for model construction
• 9b5ec6d logging cleanup
• 1f4a7c5 logging: don't call the returned function twice (one for log, one for return)
• 9a17293 fix logging in Z3_fpa_get_[es]bits
• b1bc890 fix #5515
• e7fcbd9 bail on first model validation failure
• 4f064ee simplify based on comment from Jamie Sharp #5512
• e5a2f08 fix logging of Z3_mk_lambda and Z3_mk_lambda_const
• e3a83dd Integrate fixes from #5512
• 992daa6 #5482
• e9a3038 remove wtm and booth
• cd7a826 bit_blaster unit tests for adder and multiplier (#5514)
• 8f306c6 handle constants
• 09696e9 add missing lambda defs per #5509
• 9790a8a #5507
• 828fc72 types
• d684817 re-add API for creating propagator from a context for "fresh"
• f7c1ed8 missing this
• 4d39af3 #5507 missing init
• 07c2620 regressions from previous push
• 2daf569 update Bool rewriter to pull negations up
• e6264a8 extend macro detection to negated equivalences #5496
• f03d756 missing rewrite exposed by #5498
• 17663ac #5482 other relevancy tracking
• e75b5e9 don't copy "true"
• 037c93b #5482
• 7bae297 #5482
• 26db68b #5482
• e5b6cd3 use datatype name instead of instantiation for cycle detection #5482
• e90ec45 #5482
• 5fa1b0b update project description #5503
• 23b995d #5499
• dd91cfb #5482
• 592c53e char sort
• 170ef1d add character sort to Python API and allchar function to API for ease. #5500
• 4b3b4b9 missing
• 2a682e4 #5482
• 9c7d9f0 #5497
• 1975e48 finally expose some easier to use basics could be used in cases such as #5496
• aa05298 fix #5491
• 15e3e81 remove likely culprit for #5493
• d0e2108 #5454 again
• 9122ec9 comment out for now
• 93c3fc2 try without semi-colon
• adcdd11 #5454 again
• 2492278 Update test for java
• 1db9f9a try vscode from github integration
• 810b9d0 move examples to python based build
• d980ee0 fix regression in FPNumRef sign
• b3db9a1 #5488
• 5c9f4dc #5486 - improve type elaboration by epsilon to make common cases parse without type annotation
• 7f88cfe build
• 1884ad5 expose method for updating python model for constants
• 34fc027 Update array_axioms.cpp
• 749d1ab remove dependencies on stale component
• 3516c52 Update coverage github action (#5483)
• c8a8374 #5484
• 904c6e2 modify #5454
• 429e5ed #5454
• 3d13c03 #5454
• 6a3ba64 #5454
• fe4c48e reorder fields

This list of changes was auto generated.