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 #561 8000 2
- 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.