z3-4.8.15

[NikolajBjorner]

4.8.15 release

Changes:

• f1806d3 remove buggy code, close, fix [consolidated] Issues about invalid model #5825
• 1e8bae0 enable pypi in release pipeline
• b4873d2 fix (proof=true) invalid model issue  #5907
• f053daa fix Assertation voilation at ../src/util/symbol.h, Line: 97: !is_numerical()  #5906
• bbb2777 ensure that objects in callback are of sort Ast.
• 3439d24 Revert "doc: update readme (doc: update readme #5898)" (Revert "doc: update readme" #5905)
• 9061ca5 call it macOSBuild
• b5b9c85 call it UbuntuBuild
• dfa6544 fix name for artifact
• 964e513 re-add bv_eq_axioms, fix (smt.bv.eq_axioms=false) Solution soundness bug on QF_ABV formula undetected by model validator #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 Incorrect model #5903
• 41d1c34 remove else case
• 1fa373d old bug: unit of xor is false
• 4e0a2f5 Dispose of intermediate Z3Objects created in dotnet api. (Dispose of intermediate Z3Objects created in dotnet api. #5901)
• bdf7de1 Care for root index being undefine while calling Z3_algebraic_get_i() (Care for root index being undefine while calling Z3_algebraic_get_i() #5888) [ Algebraic numbers, index problem #5807 ]
• 6455ae4 Merge branch 'master' of https://github.com/z3prover/z3
• 0b230ee move some functions to using var pattern Disposing of Z3Objects in the dotnet API #5900
• 6c4780a Update cross-build.yml
• 3d87d86 github action: add riscv64/aarch64/powerpc64 cross compile (github action: add riscv64/aarch64/powerpc64 cross compile #5897)
• a151725 call dispose on sorts Disposing of Z3Objects in the dotnet API #5900, missing charSort
• cd5e114 call dispose on sorts Disposing of Z3Objects in the dotnet API #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 (doc: update readme #5898)
• 545341e fix Enable TRACE mode error #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 Assertion violation at src/math/lp/nla_core.cpp:1420 #5894
• f26c12a fix With fp.xform.inline_linear_branch z3 returns incorrect model  #5882. Use model true when inlining (fix #5882. Use model true when inlining #5892)
• 8e18a94 Update README with info about Smalltalk bindings (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 (Clean up build warnings #5884)
• e3568d5 Handle additional cases in rule_properties::check_accessor (Handle additional cases in rule_properties::check_accessor #5821)
• 882fc31 doc strings
• b0c0f4d fix Documentation is too strict: soft assert weight can be negative #5876
• 3e51b69 no fun!
• 2b71d8b doc macros
• 87e6f10 commenting
• 676ba78 fix else case: it is first argument of const array
• 35d26bc NativeModel: TryGetArrayValue (NativeModel: TryGetArrayValue #5881)
• 248a367 na
• e1e8d15 stub out array serialization
• cd324a4 na
• 8d1276f using directives
• 35fb956 Updated user-propagator example (Updated user-propagator example #5879)
• a08be49 NativeContext, NativeSolver, NativeModel - updates for Pex (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 Disabling fp.xform.inline_eager results in an incorrect model #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 Incorrect model #5869
• 302c0d1 fix Issues with tactics #5867
• 412b050 User-functions fix (User-functions fix #5868)
• 689e2d4 remove a bunch of unneeded memory allocations
• 7f149a3 refining model update rules for del_rule Incorrect model #5865 Incorrect model #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 (Fix OCaml Binding Builds on MSYS2 #5864)
• 6be0a66 fix Disabling fp.xform.inline_eager results in an incorrect model #5863
• 6af170b fix Potential refutational soundness issue on integer formula #5861
• c2f1bdc fix Incorrect model #5862
• 11030fc disable unsound mk_seq_butlast
• ea0876b add lambda definitions during ast translation [consolidated] invalid model issues on QF_ABV instances #5820
• d06c51d na
• 061e94d Incorrect model #5858
• e8d4804 Revert "use horn_subsume_model_converter in coi filter (Fix bug in coi filter #5844)" (Revert "Fix bug in coi filter" #5859)
• 456b8ee nightly
• c47e5af multi
• cfe9846 multi
• b843618 fix Solution soundness issue on QF_ALIA #5798
• 5c26249 Assertion violation at File: ../src/ast/ast.cpp, Line: 1846 on a BV instance #5849
• 1e46395 [Consolidated] Bugs in FP logic  #4889 avoid double internalize of bvle
• b38b6da add option to disable FPMATH
• f66b4f0 fir Bug in z3py LastIndexOf #5856
• 14ee021 nightly
• e800269 na
• d0d4ab7 [consolidated] invalid model issues on QF_ABV instances #5820
• ff5d210 na
• c25d710 try out arch arm64 on the mac
• 4d184fe skip expensive equality rewriting of Booleans
• 10b611b fix Unexpected code was reached in pb_solver.cpp #5850
• 91045d3 two words
• 9a1a728 Add str.<= and str.< to Java API
• 7091b1c add additional regex operators to API
• 2e00f2f Propagator (Propagator #5845) [ What do the arguments to the user propagator callbacks represent? #5818, Update propagator example (I) #5835, Assertion violation in PbEq with integer parameter #5829, Fixed bug in user-propagator "created" #5843 ]
• 2e15e2a Add access to builtin special relations (Context::mkLinearOrder and Context::mkPartialOrder ) to Java API (Add access to builtin special relations (Context::mkLinearOrder and Context::mkPartialOrder ) to Java API #5832)
• 9cf5076 fix compiler warnings under clang (Fix compiler warnings under clang #5839)
• 09da87d use horn_subsume_model_converter in coi filter (Fix bug in coi filter #5844)
• 5bbb8fb add bail [consolidated] Issues about invalid model #5825
• 33985eb update expected
• 6202cd5 fix (smt.bv.eq_axioms=false) Solution soundness bug on QF_ABV formula undetected by model validator #5842
• aa6ec41 move idiv test to after cuts/branch
• 9a4d6ce overhead with push-ite on shared terms
• 3d26b50 fix heap-use-after-free at src/ast/ast.h:502 #5827 (rewriter.expand_nested_stores) assertion violation at ../src/smt/smt_internalizer.cpp:378 #5828
• d745d03 switch to vs 2022
• 81e94b2 na
• 07d02ea fix Assertion violation in PbEq with integer parameter #5829
• 4f6fcf8 fix Z3 build scripts assume there's a single ocamlfind path location #5814
• 0059e88 fix Randomly incorrect result using only Booleans #5808
• 9958cab fix Randomly incorrect result using only Booleans #5808
• 3f3d058 extract also units from search state
• d4ea67a Fix a few typos in README (Fixed a few typos in README #5782)
• 03ff320 block recursive definitions with lambdas until they are properly supported Invalid unsat with recursive functions and arrays #5813
• 1c10ce4 z3 python not support Select with >=2 arguments  #5815 - surface multi-arity arrays over python API
• 8a84cac add tuple support for getitem z3 python not support Select with >=2 arguments  #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 invalid model on QF_ABV formula #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 invalid model on QF_ABV formulas  #5803
• a189ca8 truncation directive smt2lib log does not lead to a valid log #5805
• 773e829 stack-overflow at seq_util::str::is_empty #5804
• 913b90f fix Invalid model for bit-vector formula #5802
• 2551631 mul overflow invalid model on formulas with bvsmul_noovfl #5797
• 5e81c12 invalid model on formulas with bvsmul_noovfl #5797 probably still wrong wrt underflow.
• 9e5b6e0 [consolidated] issues for "tactic.default_tactic=smt sat.euf=true" #5778
• 4da930b Issues with bvsmul_noovfl #5794
• a621041 fix C++ API solver::solver(context&, solver const&, translate) does not check Z3_solver_translate() for error #5795
• 461e710 fix Invalid model for bit-vec formulas #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 Spacer CHC solver and pattern-matching #4869
• 3b8c0b7 fix Soundness: sat query is answered unsat #5791
• 20f9814 fix (rewriter.flat=false) invalid model on QF_BV #5789
• d02235f [consolidated] issues for "tactic.default_tactic=smt sat.euf=true" #5778
• 85f6456 Add missing constness (Add missing constness #5787)
• 9969809 [consolidated] issues for "tactic.default_tactic=smt sat.euf=true" #5778
• a1f7676 remove assertion - literals could be assigned but propagation incomplete
• 007af9c fix stack-overflow in seq_rewriter::max_length #5784
• 1728084 added comments to explain Question about get_assignment & mark_as_relevant #5781
• b1ff4bc no normalize
• 75a81af fix heap-use-after-free at src/math/polynomial/algebraic_numbers.cpp:128 #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 heap-use-after-free at ast.h:502 #5780
• 06feb71 fix bug in root setting exposed by incremental mode pb_solver
• 36cfb88 add preliminary stub to handle closure types
• d777306 [consolidated] issues for "tactic.default_tactic=smt sat.euf=true" #5778
• fcc9f37 [consolidated] issues for "tactic.default_tactic=smt sat.euf=true" #5778
• a15da8f [consolidated] issues for "tactic.default_tactic=smt sat.euf=true" #5778
• 637ddf9 fix [consolidated] issues for "tactic.default_tactic=smt sat.euf=true" #5777
• 0dd5a5e [consolidated] issues for "tactic.default_tactic=smt sat.euf=true" #5777
• a48d3fd [consolidated] issues for "tactic.default_tactic=smt sat.euf=true" #5777
• ea93345 [consolidated] issues for "tactic.default_tactic=smt sat.euf=true" #5777
• cd56d55 [consolidated] issues for "tactic.default_tactic=smt sat.euf=true" #5753
• bc9c6ad [consolidated] issues for "tactic.default_tactic=smt sat.euf=true" #5753
• 1b5f7cd na
• 17cfc1d [consolidated] issues for "tactic.default_tactic=smt sat.euf=true" #5753
• 74824ac [consolidated] issues for "tactic.default_tactic=smt sat.euf=true" #5753
• d09abdf fix Incorrect sat result on Isaplanner prop_05 #5771
• d5cc162 bug in bounds
• 2363bfc internalize arithmetic sub-terms [consolidated] issues for "tactic.default_tactic=smt sat.euf=true" #5753
• e816946 handling unsimplified input
• b259f46 dependencies
• 4b6679e [consolidated] issues for "tactic.default_tactic=smt sat.euf=true" #5753
• 366cd9b missing pb cases
• dfe2b27 Python API (seems to be) missing string to code conversions #5773
• 0720998 [consolidated] issues for "tactic.default_tactic=smt sat.euf=true" #5753
• 10dc8d7 [consolidated] issues for "tactic.default_tactic=smt sat.euf=true" #5753
• 56d3718 add simplification with qe-lite as an option unexpected unknown result with mbqi/array property fragment #5767
• 08294d6 separate dependencies for qe_lite
• 2bcc814 add macro to track closures declared in z3_api [ Add WebAssembly/TypeScript bindings #5762 ]
• e5eaea4 ensure m_true is assigned [consolidated] issues for "tactic.default_tactic=smt sat.euf=true" #5753
• dbd5512 ensure enode without recursion
• 0557324 ensure enode without recursion
• 571a74c counting function applications The “collect-statistics” tactic returns incorrect statistics #5766
• 4cd818b The “collect-statistics” tactic returns incorrect statistics #5766
• d3bc11d bvs have to be expressions
• 21feefe Add character access functions Regression from 4.8.11.0 on bitvec comparison #5764
• 2b934b6 Add WebAssembly/TypeScript bindings (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 [consolidated] issues for "tactic.default_tactic=smt sat.euf=true" #5753
• 010bccf Update wasm.yml
• bf3c213 [consolidated] issues for "tactic.default_tactic=smt sat.euf=true" #5753
• 90fd3d8 enable propagation
• 9f9543e Fix unused variable warnings. (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 stack-overflow in static_features::update_core #5758
• 2c44454 self -> env
• d6ce050 try separate x86
• 6013d5d Unable to solve string not equals utf-8 value via Java API #5755
• 0bc8518 na
• 199daea remove Z3_bool_opt Why do some APIs return Z3_bool_opt? #5757
• 7baa4f8 build failure
• 2be71cf [consolidated] issues for "tactic.default_tactic=smt sat.euf=true" #5753
• 6a3fe51 build
• 592b1d7 Assertion violation, File: ../src/util/obj_hashtable.h, Line: 168 #5752
• d14f00d with no last model
• dadda86 Optimization fails  #5751
• 130a0c4 resurrect infinitesimals from maximization function Regression in Optimization between Z3 version 4.8.10 and 4.8.11 #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.

---

This discussion was created from the release z3-4.8.15.